The Ambient Category

We work in an ambient distributive category. This file contains some helper definitions that will be used throughout the development.

module Category.Ambient where
  record Ambient (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where
    field
      C : Category o ℓ e
      distributive : Distributive C

    open Distributive distributive public
    open import Categories.Category.Distributive.Properties distributive public
    open Category C renaming (id to idC) public
    open Cocartesian cocartesian renaming (+-unique to []-unique) public
    open Cartesian cartesian public

    -- some helpers
    cartesianCategory : CartesianCategory o ℓ e
    cartesianCategory = record { U = C ; cartesian = cartesian }

    monoidal : Monoidal C
    monoidal = CartesianMonoidal.monoidal cartesian

    symmetric : Symmetric monoidal
    symmetric = symm C cartesian

    braided : Braided monoidal
    braided = Symmetric.braided symmetric

    open BinaryProducts products renaming (η to ⁂-η; g-η to ⁂-g-η; unique to ⟨⟩-unique; unique′ to ⟨⟩-unique′) public
    open CartesianMonoidal cartesian using (⊤×A≅A; A×⊤≅A) public

    module M = M'
    module MR = MR'
    module MP = MP'

Some helper Lemmas:

    open M C
    open MR C
    open HomReasoning
    open Equiv

    distribute₄ : ∀ {A B C D} → (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ {A + B} {C} {D} ≈ [ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹
    distribute₄ = Iso⇒Epi C (IsIso.iso isIsoʳ) ((distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹) ([ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) (begin 
      (((distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹) ∘ distributeʳ)                                                                                                ≈⟨ ∘[] ⟩ 
      [ (((distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹) ∘ (i₁ ⁂ idC)) , (((distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹) ∘ (i₂ ⁂ idC)) ]                         ≈⟨ []-cong₂ (pullʳ ((refl⟩∘⟨ (⁂-cong₂ refl (sym ([]-unique id-comm-sym id-comm-sym)))) ○ sym (distributeˡ⁻¹-natural i₁ idC idC))) (pullʳ (((refl⟩∘⟨ (⁂-cong₂ refl (sym ([]-unique id-comm-sym id-comm-sym)))) ○ sym (distributeˡ⁻¹-natural i₂ idC idC)))) ⟩ 
      [ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ ((i₁ ⁂ idC) +₁ (i₁ ⁂ idC)) ∘ distributeˡ⁻¹ , (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ ((i₂ ⁂ idC) +₁ (i₂ ⁂ idC)) ∘ distributeˡ⁻¹ ] ≈⟨ []-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ distributeʳ⁻¹-i₁ distributeʳ⁻¹-i₁)) (pullˡ (+₁∘+₁ ○ +₁-cong₂ distributeʳ⁻¹-i₂ distributeʳ⁻¹-i₂)) ⟩
      [ (i₁ +₁ i₁) ∘ distributeˡ⁻¹ , (i₂ +₁ i₂) ∘ distributeˡ⁻¹ ]                                                                                                       ≈˘⟨ []∘+₁ ⟩ 
      ([ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹))                                                                                                      ≈˘⟨ pullʳ (cancelʳ (IsIso.isoˡ isIsoʳ)) ⟩ 
      (([ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ distributeʳ)                                                                      ∎)


    distributeˡ⁻¹-assoc : ∀ {A B C D : Obj} → distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ _≅_.to ×-assoc ≈ (_≅_.to ×-assoc +₁ _≅_.to ×-assoc) ∘ distributeˡ⁻¹ {A × B} {C} {D}
    distributeˡ⁻¹-assoc {A} {B} {U} {D} = Iso⇒Epi C (IsIso.iso isIsoˡ) (distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ _≅_.to ×-assoc) ((_≅_.to ×-assoc +₁ _≅_.to ×-assoc) ∘ distributeˡ⁻¹) (begin 
      (distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ _≅_.to ×-assoc) ∘ [ idC ⁂ i₁ , idC ⁂ i₂ ]                                                                                                                          ≈⟨ ∘[] ⟩ 
      [ (distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ _≅_.to ×-assoc) ∘ (idC ⁂ i₁) , (distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ _≅_.to ×-assoc) ∘ (idC ⁂ i₂) ]                                                           ≈⟨ []-cong₂ (pullʳ (pullʳ ⟨⟩∘)) (pullʳ (pullʳ ⟨⟩∘)) ⟩ 
      [ distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ (π₁ ∘ π₁) ∘ (idC ⁂ i₁) , ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (idC ⁂ i₁) ⟩ , distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ (π₁ ∘ π₁) ∘ (idC ⁂ i₂) , ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (idC ⁂ i₂) ⟩ ] ≈⟨ []-cong₂ (refl⟩∘⟨ ⁂∘⟨⟩) (refl⟩∘⟨ ⁂∘⟨⟩) ⟩ 
      [ distributeˡ⁻¹ ∘ ⟨ idC ∘ (π₁ ∘ π₁) ∘ (idC ⁂ i₁) , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (idC ⁂ i₁) ⟩ , distributeˡ⁻¹ ∘ ⟨ idC ∘ (π₁ ∘ π₁) ∘ (idC ⁂ i₂) , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (idC ⁂ i₂) ⟩ ]     ≈⟨ []-cong₂ (refl⟩∘⟨ (⟨⟩-cong₂ identityˡ refl)) (refl⟩∘⟨ (⟨⟩-cong₂ identityˡ refl)) ⟩ 
      [ distributeˡ⁻¹ ∘ ⟨ (π₁ ∘ π₁) ∘ (idC ⁂ i₁) , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (idC ⁂ i₁) ⟩ , distributeˡ⁻¹ ∘ ⟨ (π₁ ∘ π₁) ∘ (idC ⁂ i₂) , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (idC ⁂ i₂) ⟩ ]                 ≈⟨ []-cong₂ (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) (refl⟩∘⟨ ⟨⟩∘))) (refl⟩∘⟨ ⟨⟩-cong₂ (pullʳ π₁∘⁂) (refl⟩∘⟨ ⟨⟩∘)) ⟩ 
      [ distributeˡ⁻¹ ∘ ⟨ π₁ ∘ idC ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ (π₂ ∘ π₁) ∘ (idC ⁂ i₁) , π₂ ∘ (idC ⁂ i₁) ⟩ ⟩ , distributeˡ⁻¹ ∘ ⟨ π₁ ∘ idC ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ (π₂ ∘ π₁) ∘ (idC ⁂ i₂) , π₂ ∘ (idC ⁂ i₂) ⟩ ⟩ ]     ≈⟨ []-cong₂ (refl⟩∘⟨ (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂)))) (refl⟩∘⟨ (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂)))) ⟩ 
      [ distributeˡ⁻¹ ∘ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ idC ∘ π₁ , i₁ ∘ π₂ ⟩ ⟩ , distributeˡ⁻¹ ∘ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ idC ∘ π₁ , i₂ ∘ π₂ ⟩ ⟩ ]                                                   ≈⟨ []-cong₂ (refl⟩∘⟨ ⟨⟩-cong₂ refl (refl⟩∘⟨ ⟨⟩-cong₂ ((refl⟩∘⟨ identityˡ) ○ sym identityˡ) refl)) (refl⟩∘⟨ ⟨⟩-cong₂ refl (refl⟩∘⟨ ⟨⟩-cong₂ ((refl⟩∘⟨ identityˡ) ○ sym identityˡ) refl)) ⟩ 
      [ distributeˡ⁻¹ ∘ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ idC ∘ π₂ ∘ π₁ , i₁ ∘ π₂ ⟩ ⟩ , distributeˡ⁻¹ ∘ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ idC ∘ π₂ ∘ π₁ , i₂ ∘ π₂ ⟩ ⟩ ]                                                   ≈˘⟨ []-cong₂ (refl⟩∘⟨ (⟨⟩-cong₂ refl (refl⟩∘⟨ ⁂∘⟨⟩))) (refl⟩∘⟨ (⟨⟩-cong₂ refl (refl⟩∘⟨ ⁂∘⟨⟩))) ⟩  
      [ distributeˡ⁻¹ ∘ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ (idC ⁂ i₁) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , distributeˡ⁻¹ ∘ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ (idC ⁂ i₂) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ]                                               ≈⟨ []-cong₂ (refl⟩∘⟨ (⟨⟩-cong₂ (sym identityˡ) (pullˡ distributeˡ⁻¹-i₁))) (refl⟩∘⟨ (⟨⟩-cong₂ (sym identityˡ) (pullˡ distributeˡ⁻¹-i₂))) ⟩ 
      [ distributeˡ⁻¹ ∘ ⟨ idC ∘ π₁ ∘ π₁ , i₁ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , distributeˡ⁻¹ ∘ ⟨ idC ∘ π₁ ∘ π₁ , i₂ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ]                                                                                   ≈˘⟨ []-cong₂ (refl⟩∘⟨ ⁂∘⟨⟩) (refl⟩∘⟨ ⁂∘⟨⟩) ⟩ 
      [ distributeˡ⁻¹ ∘ (idC ⁂ i₁) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , distributeˡ⁻¹ ∘ (idC ⁂ i₂) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ]                                                                               ≈⟨ []-cong₂ (pullˡ distributeˡ⁻¹-i₁) (pullˡ distributeˡ⁻¹-i₂) ⟩ 
      (_≅_.to ×-assoc +₁ _≅_.to ×-assoc)                                                                                                                                                                          ≈˘⟨ cancelʳ (IsIso.isoˡ isIsoˡ) ⟩ 
      ((_≅_.to ×-assoc +₁ _≅_.to ×-assoc) ∘ distributeˡ⁻¹) ∘ distributeˡ                                                                                                                                          ∎)

    Kleisli⇒Monad⇒Kleisli : ∀ (K : KleisliTriple C) {X Y} (f : X ⇒ RMonad.F₀ K Y) → RMonad.extend (Monad⇒Kleisli C (Kleisli⇒Monad C K)) f ≈ RMonad.extend K f
    Kleisli⇒Monad⇒Kleisli K f = begin 
      extend idC ∘ extend (unit ∘ f) ≈⟨ sym kleisli.assoc ⟩ 
      extend (extend idC ∘ unit ∘ f) ≈⟨ extend-≈ (pullˡ kleisli.identityʳ) ⟩
      extend (idC ∘ f)               ≈⟨ extend-≈ (identityˡ) ⟩
      extend f                       ∎
      where 
        module kleisli = RMonad K 
        open kleisli using (unit; extend; extend-≈)

    Monad⇒Kleisli⇒Monad : ∀ (M : Monad C) {X Y} (f : X ⇒ Monad.F.₀ M Y) → Monad.F.₁ (Kleisli⇒Monad C (Monad⇒Kleisli C M)) f ≈ Monad.F.₁ M f
    Monad⇒Kleisli⇒Monad M f = begin 
      μ.η _ ∘ F.₁ (η.η _ ∘ f) ≈⟨ refl⟩∘⟨ F.homomorphism ⟩ 
      μ.η _ ∘ F.₁ (η.η _) ∘ F.₁ f ≈⟨ cancelˡ monad.identityˡ ⟩ 
      F.₁ f ∎
      where
        module monad = Monad M
        open monad using (F; η; μ)

    F₁⇒extend : ∀ (M : Monad C) {X Y} (f : X ⇒ Y) → RMonad.extend (Monad⇒Kleisli C M) (RMonad.unit (Monad⇒Kleisli C M) ∘ f) ≈ Monad.F.₁ M f
    F₁⇒extend M f = begin 
      μ.η _ ∘ F.₁ (η.η _ ∘ f) ≈⟨ refl⟩∘⟨ F.homomorphism ⟩ 
      μ.η _ ∘ F.₁ (η.η _) ∘ F.₁ f ≈⟨ cancelˡ m-identityˡ ⟩ 
      F.₁ f ∎
      where open Monad M using (F; η; μ) renaming (identityˡ to m-identityˡ)

    extend∘F₁ : ∀ (M : Monad C) {X Y Z} (f : Y ⇒ Monad.F.₀ M Z) (g : X ⇒ Y) → RMonad.extend (Monad⇒Kleisli C M) f ∘ Monad.F.₁ M g ≈ RMonad.extend (Monad⇒Kleisli C M) (f ∘ g)
    extend∘F₁ M f g = begin 
      extend f ∘ F.₁ g ≈⟨ (refl⟩∘⟨ sym (F₁⇒extend M g)) ⟩ 
      extend f ∘ extend (unit ∘ g) ≈⟨ k-sym-assoc ⟩ 
      extend (extend f ∘ unit ∘ g) ≈⟨ extend-≈ (pullˡ k-identityʳ) ⟩ 
      extend (f ∘ g) ∎
      where 
        open Monad M using (F)
        open RMonad (Monad⇒Kleisli C M) using (extend; unit; extend-≈) renaming (sym-assoc to k-sym-assoc; identityʳ to k-identityʳ)

    -- the codiagonal
    ∇ : ∀ {X} → X + X ⇒ X
    ∇ = [ idC , idC ]

    [⟨⟩]≈⟨[]⟩ : ∀ {A B C D} (f : A ⇒ B) (g : A ⇒ C) (h : D ⇒ B) (i : D ⇒ C) → [ ⟨ f , g ⟩ , ⟨ h , i ⟩ ] ≈ ⟨ [ f , h ] , [ g , i ] ⟩
    [⟨⟩]≈⟨[]⟩ f g h i = []-unique (⟨⟩∘ ○ ⟨⟩-cong₂ inject₁ inject₁) (⟨⟩∘ ○ ⟨⟩-cong₂ inject₂ inject₂)