diff --git a/docs/Cubical.Categories.Adjoint.html b/docs/Cubical.Categories.Adjoint.html
index fd4d26a..b4abb0b 100644
--- a/docs/Cubical.Categories.Adjoint.html
+++ b/docs/Cubical.Categories.Adjoint.html
@@ -11,7 +11,7 @@
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
-open Functor
+open Functor
open Iso
open Category
@@ -42,70 +42,76 @@
definition.
-}
-module UnitCounit where
-
-
- record _⊣_ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (F : Functor C D) (G : Functor D C)
- : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
- field
-
- η : 𝟙⟨ C ⟩ ⇒ (funcComp G F)
-
- ε : (funcComp F G) ⇒ 𝟙⟨ D ⟩
-
- Δ₁ : ∀ c → F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε ⟦ F ⟅ c ⟆ ⟧ ≡ D .id
- Δ₂ : ∀ d → η ⟦ G ⟅ d ⟆ ⟧ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫ ≡ C .id
-
-module NaturalBijection where
-
- record _⊣_ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (F : Functor C D) (G : Functor D C) : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
- field
- adjIso : ∀ {c d} → Iso (D [ F ⟅ c ⟆ , d ]) (C [ c , G ⟅ d ⟆ ])
-
- infix 40 _♭
- infix 40 _♯
- _♭ : ∀ {c d} → (D [ F ⟅ c ⟆ , d ]) → (C [ c , G ⟅ d ⟆ ])
- (_♭) {_} {_} = adjIso .fun
-
- _♯ : ∀ {c d} → (C [ c , G ⟅ d ⟆ ]) → (D [ F ⟅ c ⟆ , d ])
- (_♯) {_} {_} = adjIso .inv
-
- field
- adjNatInD : ∀ {c : C .ob} {d d'} (f : D [ F ⟅ c ⟆ , d ]) (k : D [ d , d' ])
- → (f ⋆⟨ D ⟩ k) ♭ ≡ f ♭ ⋆⟨ C ⟩ G ⟪ k ⟫
-
- adjNatInC : ∀ {c' c d} (g : C [ c , G ⟅ d ⟆ ]) (h : C [ c' , c ])
- → (h ⋆⟨ C ⟩ g) ♯ ≡ F ⟪ h ⟫ ⋆⟨ D ⟩ g ♯
-
- adjNatInD' : ∀ {c : C .ob} {d d'} (g : C [ c , G ⟅ d ⟆ ]) (k : D [ d , d' ])
- → g ♯ ⋆⟨ D ⟩ k ≡ (g ⋆⟨ C ⟩ G ⟪ k ⟫) ♯
- adjNatInD' {c} {d} {d'} g k =
- g ♯ ⋆⟨ D ⟩ k
- ≡⟨ sym (adjIso .leftInv (g ♯ ⋆⟨ D ⟩ k)) ⟩
- ((g ♯ ⋆⟨ D ⟩ k) ♭) ♯
- ≡⟨ cong _♯ (adjNatInD (g ♯) k) ⟩
- ((g ♯) ♭ ⋆⟨ C ⟩ G ⟪ k ⟫) ♯
- ≡⟨ cong _♯ (cong (λ g' → seq' C g' (G ⟪ k ⟫)) (adjIso .rightInv g)) ⟩
- (g ⋆⟨ C ⟩ G ⟪ k ⟫) ♯ ∎
-
- adjNatInC' : ∀ {c' c d} (f : D [ F ⟅ c ⟆ , d ]) (h : C [ c' , c ])
- → h ⋆⟨ C ⟩ (f ♭) ≡ (F ⟪ h ⟫ ⋆⟨ D ⟩ f) ♭
- adjNatInC' {c'} {c} {d} f h =
- h ⋆⟨ C ⟩ (f ♭)
- ≡⟨ sym (adjIso .rightInv (h ⋆⟨ C ⟩ (f ♭))) ⟩
- ((h ⋆⟨ C ⟩ (f ♭)) ♯) ♭
- ≡⟨ cong _♭ (adjNatInC (f ♭) h) ⟩
- ((F ⟪ h ⟫ ⋆⟨ D ⟩ (f ♭) ♯) ♭)
- ≡⟨ cong _♭ (cong (λ f' → seq' D (F ⟪ h ⟫) f') (adjIso .leftInv f)) ⟩
- (F ⟪ h ⟫ ⋆⟨ D ⟩ f) ♭ ∎
-
- isLeftAdjoint : {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (F : Functor C D) → Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD'))
- isLeftAdjoint {C = C}{D} F = Σ[ G ∈ Functor D C ] F ⊣ G
-
- isRightAdjoint : {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (G : Functor D C) → Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD'))
- isRightAdjoint {C = C}{D} G = Σ[ F ∈ Functor C D ] F ⊣ G
-
-module UnitCounit {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (F : Functor C D) (G : Functor D C) where
+ record TriangleIdentities
+ (η : 𝟙⟨ C ⟩ ⇒ (funcComp G F))
+ (ε : (funcComp F G) ⇒ 𝟙⟨ D ⟩)
+ : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD'))
+ where
+ field
+ Δ₁ : ∀ c → F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε ⟦ F ⟅ c ⟆ ⟧ ≡ D .id
+ Δ₂ : ∀ d → η ⟦ G ⟅ d ⟆ ⟧ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫ ≡ C .id
+
+
+ record _⊣_ : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
+ field
+
+ η : 𝟙⟨ C ⟩ ⇒ (funcComp G F)
+
+ ε : (funcComp F G) ⇒ 𝟙⟨ D ⟩
+ triangleIdentities : TriangleIdentities η ε
+ open TriangleIdentities triangleIdentities public
+
+module NaturalBijection where
+
+ record _⊣_ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (F : Functor C D) (G : Functor D C) : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
+ field
+ adjIso : ∀ {c d} → Iso (D [ F ⟅ c ⟆ , d ]) (C [ c , G ⟅ d ⟆ ])
+
+ infix 40 _♭
+ infix 40 _♯
+ _♭ : ∀ {c d} → (D [ F ⟅ c ⟆ , d ]) → (C [ c , G ⟅ d ⟆ ])
+ (_♭) {_} {_} = adjIso .fun
+
+ _♯ : ∀ {c d} → (C [ c , G ⟅ d ⟆ ]) → (D [ F ⟅ c ⟆ , d ])
+ (_♯) {_} {_} = adjIso .inv
+
+ field
+ adjNatInD : ∀ {c : C .ob} {d d'} (f : D [ F ⟅ c ⟆ , d ]) (k : D [ d , d' ])
+ → (f ⋆⟨ D ⟩ k) ♭ ≡ f ♭ ⋆⟨ C ⟩ G ⟪ k ⟫
+
+ adjNatInC : ∀ {c' c d} (g : C [ c , G ⟅ d ⟆ ]) (h : C [ c' , c ])
+ → (h ⋆⟨ C ⟩ g) ♯ ≡ F ⟪ h ⟫ ⋆⟨ D ⟩ g ♯
+
+ adjNatInD' : ∀ {c : C .ob} {d d'} (g : C [ c , G ⟅ d ⟆ ]) (k : D [ d , d' ])
+ → g ♯ ⋆⟨ D ⟩ k ≡ (g ⋆⟨ C ⟩ G ⟪ k ⟫) ♯
+ adjNatInD' {c} {d} {d'} g k =
+ g ♯ ⋆⟨ D ⟩ k
+ ≡⟨ sym (adjIso .leftInv (g ♯ ⋆⟨ D ⟩ k)) ⟩
+ ((g ♯ ⋆⟨ D ⟩ k) ♭) ♯
+ ≡⟨ cong _♯ (adjNatInD (g ♯) k) ⟩
+ ((g ♯) ♭ ⋆⟨ C ⟩ G ⟪ k ⟫) ♯
+ ≡⟨ cong _♯ (cong (λ g' → seq' C g' (G ⟪ k ⟫)) (adjIso .rightInv g)) ⟩
+ (g ⋆⟨ C ⟩ G ⟪ k ⟫) ♯ ∎
+
+ adjNatInC' : ∀ {c' c d} (f : D [ F ⟅ c ⟆ , d ]) (h : C [ c' , c ])
+ → h ⋆⟨ C ⟩ (f ♭) ≡ (F ⟪ h ⟫ ⋆⟨ D ⟩ f) ♭
+ adjNatInC' {c'} {c} {d} f h =
+ h ⋆⟨ C ⟩ (f ♭)
+ ≡⟨ sym (adjIso .rightInv (h ⋆⟨ C ⟩ (f ♭))) ⟩
+ ((h ⋆⟨ C ⟩ (f ♭)) ♯) ♭
+ ≡⟨ cong _♭ (adjNatInC (f ♭) h) ⟩
+ ((F ⟪ h ⟫ ⋆⟨ D ⟩ (f ♭) ♯) ♭)
+ ≡⟨ cong _♭ (cong (λ f' → seq' D (F ⟪ h ⟫) f') (adjIso .leftInv f)) ⟩
+ (F ⟪ h ⟫ ⋆⟨ D ⟩ f) ♭ ∎
+
+ isLeftAdjoint : {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (F : Functor C D) → Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD'))
+ isLeftAdjoint {C = C}{D} F = Σ[ G ∈ Functor D C ] F ⊣ G
+
+ isRightAdjoint : {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (G : Functor D C) → Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD'))
+ isRightAdjoint {C = C}{D} G = Σ[ F ∈ Functor C D ] F ⊣ G
+
+
-module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (F : Functor C D) (G : Functor D C) where
- open UnitCounit
- open NaturalBijection renaming (_⊣_ to _⊣²_)
- module _ (adj : F ⊣² G) where
- open _⊣²_ adj
- open _⊣_
-
-
-
-
- adjNat' : ∀ {c c' d d'} {f : D [ F ⟅ c ⟆ , d ]} {k : D [ d , d' ]}
- → {h : C [ c , c' ]} {g : C [ c' , G ⟅ d' ⟆ ]}
-
- → ((f ⋆⟨ D ⟩ k ≡ F ⟪ h ⟫ ⋆⟨ D ⟩ g ♯) → (f ♭ ⋆⟨ C ⟩ G ⟪ k ⟫ ≡ h ⋆⟨ C ⟩ g))
- × ((f ♭ ⋆⟨ C ⟩ G ⟪ k ⟫ ≡ h ⋆⟨ C ⟩ g) → (f ⋆⟨ D ⟩ k ≡ F ⟪ h ⟫ ⋆⟨ D ⟩ g ♯))
- adjNat' {c} {c'} {d} {d'} {f} {k} {h} {g} = D→C , C→D
- where
- D→C : (f ⋆⟨ D ⟩ k ≡ F ⟪ h ⟫ ⋆⟨ D ⟩ g ♯) → (f ♭ ⋆⟨ C ⟩ G ⟪ k ⟫ ≡ h ⋆⟨ C ⟩ g)
- D→C eq = f ♭ ⋆⟨ C ⟩ G ⟪ k ⟫
- ≡⟨ sym (adjNatInD _ _) ⟩
- ((f ⋆⟨ D ⟩ k) ♭)
- ≡⟨ cong _♭ eq ⟩
- (F ⟪ h ⟫ ⋆⟨ D ⟩ g ♯) ♭
- ≡⟨ sym (cong _♭ (adjNatInC _ _)) ⟩
- (h ⋆⟨ C ⟩ g) ♯ ♭
- ≡⟨ adjIso .rightInv _ ⟩
- h ⋆⟨ C ⟩ g
- ∎
- C→D : (f ♭ ⋆⟨ C ⟩ G ⟪ k ⟫ ≡ h ⋆⟨ C ⟩ g) → (f ⋆⟨ D ⟩ k ≡ F ⟪ h ⟫ ⋆⟨ D ⟩ g ♯)
- C→D eq = f ⋆⟨ D ⟩ k
- ≡⟨ sym (adjIso .leftInv _) ⟩
- (f ⋆⟨ D ⟩ k) ♭ ♯
- ≡⟨ cong _♯ (adjNatInD _ _) ⟩
- (f ♭ ⋆⟨ C ⟩ G ⟪ k ⟫) ♯
- ≡⟨ cong _♯ eq ⟩
- (h ⋆⟨ C ⟩ g) ♯
- ≡⟨ adjNatInC _ _ ⟩
- F ⟪ h ⟫ ⋆⟨ D ⟩ g ♯
- ∎
-
- open NatTrans
-
-
-
- adj'→adj : F ⊣ G
- adj'→adj = record
- { η = η'
- ; ε = ε'
- ; Δ₁ = Δ₁'
- ; Δ₂ = Δ₂' }
-
- where
-
-
-
- commInD : ∀ {x y} (f : C [ x , y ]) → D .id ⋆⟨ D ⟩ F ⟪ f ⟫ ≡ F ⟪ f ⟫ ⋆⟨ D ⟩ D .id
- commInD f = (D .⋆IdL _) ∙ sym (D .⋆IdR _)
-
- sharpen1 : ∀ {x y} (f : C [ x , y ]) → F ⟪ f ⟫ ⋆⟨ D ⟩ D .id ≡ F ⟪ f ⟫ ⋆⟨ D ⟩ D .id ♭ ♯
- sharpen1 f = cong (λ v → F ⟪ f ⟫ ⋆⟨ D ⟩ v) (sym (adjIso .leftInv _))
-
- η' : 𝟙⟨ C ⟩ ⇒ G ∘F F
- η' .N-ob x = D .id ♭
- η' .N-hom f = sym (fst (adjNat') (commInD f ∙ sharpen1 f))
-
-
-
-
- commInC : ∀ {x y} (g : D [ x , y ]) → C .id ⋆⟨ C ⟩ G ⟪ g ⟫ ≡ G ⟪ g ⟫ ⋆⟨ C ⟩ C .id
- commInC g = (C .⋆IdL _) ∙ sym (C .⋆IdR _)
-
- sharpen2 : ∀ {x y} (g : D [ x , y ]) → C .id ♯ ♭ ⋆⟨ C ⟩ G ⟪ g ⟫ ≡ C .id ⋆⟨ C ⟩ G ⟪ g ⟫
- sharpen2 g = cong (λ v → v ⋆⟨ C ⟩ G ⟪ g ⟫) (adjIso .rightInv _)
-
- ε' : F ∘F G ⇒ 𝟙⟨ D ⟩
- ε' .N-ob x = C .id ♯
- ε' .N-hom g = sym (snd adjNat' (sharpen2 g ∙ commInC g))
-
-
-
- Δ₁' : ∀ c → F ⟪ η' ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε' ⟦ F ⟅ c ⟆ ⟧ ≡ D .id
- Δ₁' c =
- F ⟪ η' ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε' ⟦ F ⟅ c ⟆ ⟧
- ≡⟨ sym (snd adjNat' (cong (λ v → (η' ⟦ c ⟧) ⋆⟨ C ⟩ v) (G .F-id))) ⟩
- D .id ⋆⟨ D ⟩ D .id
- ≡⟨ D .⋆IdL _ ⟩
- D .id
- ∎
-
-
-
- Δ₂' : ∀ d → η' ⟦ G ⟅ d ⟆ ⟧ ⋆⟨ C ⟩ G ⟪ ε' ⟦ d ⟧ ⟫ ≡ C .id
- Δ₂' d =
- (η' ⟦ G ⟅ d ⟆ ⟧) ⋆⟨ C ⟩ (G ⟪ ε' ⟦ d ⟧ ⟫)
- ≡⟨ fst adjNat' (cong (λ v → v ⋆⟨ D ⟩ (ε' ⟦ d ⟧)) (sym (F .F-id))) ⟩
- C .id ⋆⟨ C ⟩ C .id
- ≡⟨ C .⋆IdL _ ⟩
- C .id
- ∎
-
-
- module _ (adj : F ⊣ G) where
- open _⊣_ adj
- open _⊣²_
- open NatTrans
-
- adj→adj' : F ⊣² G
-
-
- adj→adj' .adjIso {c = c} .fun f = η ⟦ c ⟧ ⋆⟨ C ⟩ G ⟪ f ⟫
-
- adj→adj' .adjIso {d = d} .inv g = F ⟪ g ⟫ ⋆⟨ D ⟩ ε ⟦ d ⟧
-
- adj→adj' .adjIso {c = c} {d} .rightInv g
- = η ⟦ c ⟧ ⋆⟨ C ⟩ G ⟪ F ⟪ g ⟫ ⋆⟨ D ⟩ ε ⟦ d ⟧ ⟫
- ≡⟨ cong (λ v → η ⟦ c ⟧ ⋆⟨ C ⟩ v) (G .F-seq _ _) ⟩
- η ⟦ c ⟧ ⋆⟨ C ⟩ (G ⟪ F ⟪ g ⟫ ⟫ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫)
- ≡⟨ sym (C .⋆Assoc _ _ _) ⟩
- η ⟦ c ⟧ ⋆⟨ C ⟩ G ⟪ F ⟪ g ⟫ ⟫ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫
-
- ≡⟨ rCatWhisker {C = C} _ _ _ natu ⟩
- (g ⋆⟨ C ⟩ η ⟦ G ⟅ d ⟆ ⟧) ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫
- ≡⟨ C .⋆Assoc _ _ _ ⟩
- g ⋆⟨ C ⟩ (η ⟦ G ⟅ d ⟆ ⟧ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫)
- ≡⟨ lCatWhisker {C = C} _ _ _ (Δ₂ d) ⟩
- g ⋆⟨ C ⟩ C .id
- ≡⟨ C .⋆IdR _ ⟩
- g
- ∎
- where
- natu : η ⟦ c ⟧ ⋆⟨ C ⟩ G ⟪ F ⟪ g ⟫ ⟫ ≡ g ⋆⟨ C ⟩ η ⟦ G ⟅ d ⟆ ⟧
- natu = sym (η .N-hom _)
- adj→adj' .adjIso {c = c} {d} .leftInv f
- = F ⟪ η ⟦ c ⟧ ⋆⟨ C ⟩ G ⟪ f ⟫ ⟫ ⋆⟨ D ⟩ ε ⟦ d ⟧
- ≡⟨ cong (λ v → v ⋆⟨ D ⟩ ε ⟦ d ⟧) (F .F-seq _ _) ⟩
- F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ F ⟪ G ⟪ f ⟫ ⟫ ⋆⟨ D ⟩ ε ⟦ d ⟧
- ≡⟨ D .⋆Assoc _ _ _ ⟩
- F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ (F ⟪ G ⟪ f ⟫ ⟫ ⋆⟨ D ⟩ ε ⟦ d ⟧)
-
- ≡⟨ lCatWhisker {C = D} _ _ _ natu ⟩
- F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ (ε ⟦ F ⟅ c ⟆ ⟧ ⋆⟨ D ⟩ f)
- ≡⟨ sym (D .⋆Assoc _ _ _) ⟩
- F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε ⟦ F ⟅ c ⟆ ⟧ ⋆⟨ D ⟩ f
-
- ≡⟨ rCatWhisker {C = D} _ _ _ (Δ₁ c) ⟩
- D .id ⋆⟨ D ⟩ f
- ≡⟨ D .⋆IdL _ ⟩
- f
- ∎
- where
- natu : F ⟪ G ⟪ f ⟫ ⟫ ⋆⟨ D ⟩ ε ⟦ d ⟧ ≡ ε ⟦ F ⟅ c ⟆ ⟧ ⋆⟨ D ⟩ f
- natu = ε .N-hom _
-
- adj→adj' .adjNatInD {c = c} f k = cong (λ v → η ⟦ c ⟧ ⋆⟨ C ⟩ v) (G .F-seq _ _) ∙ (sym (C .⋆Assoc _ _ _))
- adj→adj' .adjNatInC {d = d} g h = cong (λ v → v ⋆⟨ D ⟩ ε ⟦ d ⟧) (F .F-seq _ _) ∙ D .⋆Assoc _ _ _
+module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (F : Functor C D) (G : Functor D C) where
+ open UnitCounit
+ open NaturalBijection renaming (_⊣_ to _⊣²_)
+ module _ (adj : F ⊣² G) where
+ open _⊣²_ adj
+ open _⊣_
+
+
+
+
+ adjNat' : ∀ {c c' d d'} {f : D [ F ⟅ c ⟆ , d ]} {k : D [ d , d' ]}
+ → {h : C [ c , c' ]} {g : C [ c' , G ⟅ d' ⟆ ]}
+
+ → ((f ⋆⟨ D ⟩ k ≡ F ⟪ h ⟫ ⋆⟨ D ⟩ g ♯) → (f ♭ ⋆⟨ C ⟩ G ⟪ k ⟫ ≡ h ⋆⟨ C ⟩ g))
+ × ((f ♭ ⋆⟨ C ⟩ G ⟪ k ⟫ ≡ h ⋆⟨ C ⟩ g) → (f ⋆⟨ D ⟩ k ≡ F ⟪ h ⟫ ⋆⟨ D ⟩ g ♯))
+ adjNat' {c} {c'} {d} {d'} {f} {k} {h} {g} = D→C , C→D
+ where
+ D→C : (f ⋆⟨ D ⟩ k ≡ F ⟪ h ⟫ ⋆⟨ D ⟩ g ♯) → (f ♭ ⋆⟨ C ⟩ G ⟪ k ⟫ ≡ h ⋆⟨ C ⟩ g)
+ D→C eq = f ♭ ⋆⟨ C ⟩ G ⟪ k ⟫
+ ≡⟨ sym (adjNatInD _ _) ⟩
+ ((f ⋆⟨ D ⟩ k) ♭)
+ ≡⟨ cong _♭ eq ⟩
+ (F ⟪ h ⟫ ⋆⟨ D ⟩ g ♯) ♭
+ ≡⟨ sym (cong _♭ (adjNatInC _ _)) ⟩
+ (h ⋆⟨ C ⟩ g) ♯ ♭
+ ≡⟨ adjIso .rightInv _ ⟩
+ h ⋆⟨ C ⟩ g
+ ∎
+ C→D : (f ♭ ⋆⟨ C ⟩ G ⟪ k ⟫ ≡ h ⋆⟨ C ⟩ g) → (f ⋆⟨ D ⟩ k ≡ F ⟪ h ⟫ ⋆⟨ D ⟩ g ♯)
+ C→D eq = f ⋆⟨ D ⟩ k
+ ≡⟨ sym (adjIso .leftInv _) ⟩
+ (f ⋆⟨ D ⟩ k) ♭ ♯
+ ≡⟨ cong _♯ (adjNatInD _ _) ⟩
+ (f ♭ ⋆⟨ C ⟩ G ⟪ k ⟫) ♯
+ ≡⟨ cong _♯ eq ⟩
+ (h ⋆⟨ C ⟩ g) ♯
+ ≡⟨ adjNatInC _ _ ⟩
+ F ⟪ h ⟫ ⋆⟨ D ⟩ g ♯
+ ∎
+
+ open NatTrans
+
+
+
+ adj'→adj : F ⊣ G
+ adj'→adj = record
+ { η = η'
+ ; ε = ε'
+ ; triangleIdentities = record
+ {Δ₁ = Δ₁'
+ ; Δ₂ = Δ₂' }}
+
+ where
+
+
+
+ commInD : ∀ {x y} (f : C [ x , y ]) → D .id ⋆⟨ D ⟩ F ⟪ f ⟫ ≡ F ⟪ f ⟫ ⋆⟨ D ⟩ D .id
+ commInD f = (D .⋆IdL _) ∙ sym (D .⋆IdR _)
+
+ sharpen1 : ∀ {x y} (f : C [ x , y ]) → F ⟪ f ⟫ ⋆⟨ D ⟩ D .id ≡ F ⟪ f ⟫ ⋆⟨ D ⟩ D .id ♭ ♯
+ sharpen1 f = cong (λ v → F ⟪ f ⟫ ⋆⟨ D ⟩ v) (sym (adjIso .leftInv _))
+
+ η' : 𝟙⟨ C ⟩ ⇒ G ∘F F
+ η' .N-ob x = D .id ♭
+ η' .N-hom f = sym (fst (adjNat') (commInD f ∙ sharpen1 f))
+
+
+
+
+ commInC : ∀ {x y} (g : D [ x , y ]) → C .id ⋆⟨ C ⟩ G ⟪ g ⟫ ≡ G ⟪ g ⟫ ⋆⟨ C ⟩ C .id
+ commInC g = (C .⋆IdL _) ∙ sym (C .⋆IdR _)
+
+ sharpen2 : ∀ {x y} (g : D [ x , y ]) → C .id ♯ ♭ ⋆⟨ C ⟩ G ⟪ g ⟫ ≡ C .id ⋆⟨ C ⟩ G ⟪ g ⟫
+ sharpen2 g = cong (λ v → v ⋆⟨ C ⟩ G ⟪ g ⟫) (adjIso .rightInv _)
+
+ ε' : F ∘F G ⇒ 𝟙⟨ D ⟩
+ ε' .N-ob x = C .id ♯
+ ε' .N-hom g = sym (snd adjNat' (sharpen2 g ∙ commInC g))
+
+
+
+ Δ₁' : ∀ c → F ⟪ η' ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε' ⟦ F ⟅ c ⟆ ⟧ ≡ D .id
+ Δ₁' c =
+ F ⟪ η' ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε' ⟦ F ⟅ c ⟆ ⟧
+ ≡⟨ sym (snd adjNat' (cong (λ v → (η' ⟦ c ⟧) ⋆⟨ C ⟩ v) (G .F-id))) ⟩
+ D .id ⋆⟨ D ⟩ D .id
+ ≡⟨ D .⋆IdL _ ⟩
+ D .id
+ ∎
+
+
+
+ Δ₂' : ∀ d → η' ⟦ G ⟅ d ⟆ ⟧ ⋆⟨ C ⟩ G ⟪ ε' ⟦ d ⟧ ⟫ ≡ C .id
+ Δ₂' d =
+ (η' ⟦ G ⟅ d ⟆ ⟧) ⋆⟨ C ⟩ (G ⟪ ε' ⟦ d ⟧ ⟫)
+ ≡⟨ fst adjNat' (cong (λ v → v ⋆⟨ D ⟩ (ε' ⟦ d ⟧)) (sym (F .F-id))) ⟩
+ C .id ⋆⟨ C ⟩ C .id
+ ≡⟨ C .⋆IdL _ ⟩
+ C .id
+ ∎
+
+
+ module _ (adj : F ⊣ G) where
+ open _⊣_ adj
+ open _⊣²_
+ open NatTrans
+
+ adj→adj' : F ⊣² G
+
+
+ adj→adj' .adjIso {c = c} .fun f = η ⟦ c ⟧ ⋆⟨ C ⟩ G ⟪ f ⟫
+
+ adj→adj' .adjIso {d = d} .inv g = F ⟪ g ⟫ ⋆⟨ D ⟩ ε ⟦ d ⟧
+
+ adj→adj' .adjIso {c = c} {d} .rightInv g
+ = η ⟦ c ⟧ ⋆⟨ C ⟩ G ⟪ F ⟪ g ⟫ ⋆⟨ D ⟩ ε ⟦ d ⟧ ⟫
+ ≡⟨ cong (λ v → η ⟦ c ⟧ ⋆⟨ C ⟩ v) (G .F-seq _ _) ⟩
+ η ⟦ c ⟧ ⋆⟨ C ⟩ (G ⟪ F ⟪ g ⟫ ⟫ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫)
+ ≡⟨ sym (C .⋆Assoc _ _ _) ⟩
+ η ⟦ c ⟧ ⋆⟨ C ⟩ G ⟪ F ⟪ g ⟫ ⟫ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫
+
+ ≡⟨ rCatWhisker {C = C} _ _ _ natu ⟩
+ (g ⋆⟨ C ⟩ η ⟦ G ⟅ d ⟆ ⟧) ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫
+ ≡⟨ C .⋆Assoc _ _ _ ⟩
+ g ⋆⟨ C ⟩ (η ⟦ G ⟅ d ⟆ ⟧ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫)
+ ≡⟨ lCatWhisker {C = C} _ _ _ (Δ₂ d) ⟩
+ g ⋆⟨ C ⟩ C .id
+ ≡⟨ C .⋆IdR _ ⟩
+ g
+ ∎
+ where
+ natu : η ⟦ c ⟧ ⋆⟨ C ⟩ G ⟪ F ⟪ g ⟫ ⟫ ≡ g ⋆⟨ C ⟩ η ⟦ G ⟅ d ⟆ ⟧
+ natu = sym (η .N-hom _)
+ adj→adj' .adjIso {c = c} {d} .leftInv f
+ = F ⟪ η ⟦ c ⟧ ⋆⟨ C ⟩ G ⟪ f ⟫ ⟫ ⋆⟨ D ⟩ ε ⟦ d ⟧
+ ≡⟨ cong (λ v → v ⋆⟨ D ⟩ ε ⟦ d ⟧) (F .F-seq _ _) ⟩
+ F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ F ⟪ G ⟪ f ⟫ ⟫ ⋆⟨ D ⟩ ε ⟦ d ⟧
+ ≡⟨ D .⋆Assoc _ _ _ ⟩
+ F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ (F ⟪ G ⟪ f ⟫ ⟫ ⋆⟨ D ⟩ ε ⟦ d ⟧)
+
+ ≡⟨ lCatWhisker {C = D} _ _ _ natu ⟩
+ F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ (ε ⟦ F ⟅ c ⟆ ⟧ ⋆⟨ D ⟩ f)
+ ≡⟨ sym (D .⋆Assoc _ _ _) ⟩
+ F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε ⟦ F ⟅ c ⟆ ⟧ ⋆⟨ D ⟩ f
+
+ ≡⟨ rCatWhisker {C = D} _ _ _ (Δ₁ c) ⟩
+ D .id ⋆⟨ D ⟩ f
+ ≡⟨ D .⋆IdL _ ⟩
+ f
+ ∎
+ where
+ natu : F ⟪ G ⟪ f ⟫ ⟫ ⋆⟨ D ⟩ ε ⟦ d ⟧ ≡ ε ⟦ F ⟅ c ⟆ ⟧ ⋆⟨ D ⟩ f
+ natu = ε .N-hom _
+
+ adj→adj' .adjNatInD {c = c} f k = cong (λ v → η ⟦ c ⟧ ⋆⟨ C ⟩ v) (G .F-seq _ _) ∙ (sym (C .⋆Assoc _ _ _))
+ adj→adj' .adjNatInC {d = d} g h = cong (λ v → v ⋆⟨ D ⟩ ε ⟦ d ⟧) (F .F-seq _ _) ∙ D .⋆Assoc _ _ _