diff --git a/docs/Cubical.Categories.Adjoint.html b/docs/Cubical.Categories.Adjoint.html index 2c878d2..6007114 100644 --- a/docs/Cubical.Categories.Adjoint.html +++ b/docs/Cubical.Categories.Adjoint.html @@ -1,25 +1,25 @@ -
{-# OPTIONS --allow-unsolved-metas #-} +\ No newline at end of file diff --git a/docs/Cubical.Categories.Category.Properties.html b/docs/Cubical.Categories.Category.Properties.html index 71ac7f0..92726db 100644 --- a/docs/Cubical.Categories.Category.Properties.html +++ b/docs/Cubical.Categories.Category.Properties.html @@ -18,21 +18,21 @@ -- isSet where your allowed to compare paths where one side is only -- equal up to path. Is there a generalization of this? isSetHomP1 : ∀ {x y : C .ob} {n : C [ x , y ]} - → isOfHLevelDep 1 (λ m → m ≡ n) - isSetHomP1 {x = x} {y} {n} = isOfHLevel→isOfHLevelDep 1 (λ m → isSetHom C m n) + → isOfHLevelDep 1 (λ m → m ≡ n) + isSetHomP1 {x = x} {y} {n} = isOfHLevel→isOfHLevelDep 1 (λ m → isSetHom C m n) -- isSet where the arrows can be between non-definitionally equal obs isSetHomP2l : ∀ {y : C .ob} - → isOfHLevelDep 2 (λ x → C [ x , y ]) - isSetHomP2l = isOfHLevel→isOfHLevelDep 2 (λ a → isSetHom C {x = a}) + → isOfHLevelDep 2 (λ x → C [ x , y ]) + isSetHomP2l = isOfHLevel→isOfHLevelDep 2 (λ a → isSetHom C {x = a}) isSetHomP2r : ∀ {x : C .ob} - → isOfHLevelDep 2 (λ y → C [ x , y ]) - isSetHomP2r = isOfHLevel→isOfHLevelDep 2 (λ a → isSetHom C {y = a}) + → isOfHLevelDep 2 (λ y → C [ x , y ]) + isSetHomP2r = isOfHLevel→isOfHLevelDep 2 (λ a → isSetHom C {y = a}) -- opposite of opposite is definitionally equal to itself -involutiveOp : ∀ {C : Category ℓ ℓ'} → C ^op ^op ≡ C +involutiveOp : ∀ {C : Category ℓ ℓ'} → C ^op ^op ≡ C involutiveOp = refl module _ {C : Category ℓ ℓ'} where @@ -40,12 +40,12 @@ -- whisker the parallel morphisms g and g' with f lCatWhisker : {x y z : C .ob} (f : C [ x , y ]) (g g' : C [ y , z ]) (p : g ≡ g') - → f ⋆⟨ C ⟩ g ≡ f ⋆⟨ C ⟩ g' + → f ⋆⟨ C ⟩ g ≡ f ⋆⟨ C ⟩ g' lCatWhisker f _ _ p = cong (_⋆_ C f) p rCatWhisker : {x y z : C .ob} (f f' : C [ x , y ]) (g : C [ y , z ]) (p : f ≡ f') - → f ⋆⟨ C ⟩ g ≡ f' ⋆⟨ C ⟩ g - rCatWhisker _ _ g p = cong (λ v → v ⋆⟨ C ⟩ g) p + → f ⋆⟨ C ⟩ g ≡ f' ⋆⟨ C ⟩ g + rCatWhisker _ _ g p = cong (λ v → v ⋆⟨ C ⟩ g) p -- working with equal objects idP : ∀ {x x'} {p : x ≡ x'} → C [ x , x' ] @@ -55,65 +55,65 @@ seqP : ∀ {x y y' z} {p : y ≡ y'} → (f : C [ x , y ]) (g : C [ y' , z ]) → C [ x , z ] - seqP {x} {_} {_} {z} {p} f g = f ⋆⟨ C ⟩ (subst (λ a → C [ a , z ]) (sym p) g) + seqP {x} {_} {_} {z} {p} f g = f ⋆⟨ C ⟩ (subst (λ a → C [ a , z ]) (sym p) g) -- also heterogeneous seq, but substituting on the left seqP' : ∀ {x y y' z} {p : y ≡ y'} → (f : C [ x , y ]) (g : C [ y' , z ]) → C [ x , z ] - seqP' {x} {_} {_} {z} {p} f g = subst (λ a → C [ x , a ]) p f ⋆⟨ C ⟩ g + seqP' {x} {_} {_} {z} {p} f g = subst (λ a → C [ x , a ]) p f ⋆⟨ C ⟩ g -- show that they're equal seqP≡seqP' : ∀ {x y y' z} {p : y ≡ y'} → (f : C [ x , y ]) (g : C [ y' , z ]) → seqP {p = p} f g ≡ seqP' {p = p} f g seqP≡seqP' {x = x} {z = z} {p = p} f g i = - (toPathP {A = λ i' → C [ x , p i' ]} {f} refl i) - ⋆⟨ C ⟩ - (toPathP {A = λ i' → C [ p (~ i') , z ]} {x = g} (sym refl) (~ i)) + (toPathP {A = λ i' → C [ x , p i' ]} {f} refl i) + ⋆⟨ C ⟩ + (toPathP {A = λ i' → C [ p (~ i') , z ]} {x = g} (sym refl) (~ i)) -- seqP is equal to normal seq when y ≡ y' seqP≡seq : ∀ {x y z} → (f : C [ x , y ]) (g : C [ y , z ]) - → seqP {p = refl} f g ≡ f ⋆⟨ C ⟩ g - seqP≡seq {y = y} {z} f g i = f ⋆⟨ C ⟩ toPathP {A = λ _ → C [ y , z ]} {x = g} refl (~ i) + → seqP {p = refl} f g ≡ f ⋆⟨ C ⟩ g + seqP≡seq {y = y} {z} f g i = f ⋆⟨ C ⟩ toPathP {A = λ _ → C [ y , z ]} {x = g} refl (~ i) -- whiskering with heterogenous seq -- (maybe should let z be heterogeneous too) lCatWhiskerP : {x y z y' : C .ob} {p : y ≡ y'} → (f : C [ x , y ]) (g : C [ y , z ]) (g' : C [ y' , z ]) → (r : PathP (λ i → C [ p i , z ]) g g') - → f ⋆⟨ C ⟩ g ≡ seqP {p = p} f g' + → f ⋆⟨ C ⟩ g ≡ seqP {p = p} f g' lCatWhiskerP {z = z} {p = p} f g g' r = - cong (λ v → f ⋆⟨ C ⟩ v) (sym (fromPathP (symP {A = λ i → C [ p (~ i) , z ]} r))) + cong (λ v → f ⋆⟨ C ⟩ v) (sym (fromPathP (symP {A = λ i → C [ p (~ i) , z ]} r))) rCatWhiskerP : {x y' y z : C .ob} {p : y' ≡ y} → (f' : C [ x , y' ]) (f : C [ x , y ]) (g : C [ y , z ]) → (r : PathP (λ i → C [ x , p i ]) f' f) - → f ⋆⟨ C ⟩ g ≡ seqP' {p = p} f' g - rCatWhiskerP f' f g r = cong (λ v → v ⋆⟨ C ⟩ g) (sym (fromPathP r)) + → f ⋆⟨ C ⟩ g ≡ seqP' {p = p} f' g + rCatWhiskerP f' f g r = cong (λ v → v ⋆⟨ C ⟩ g) (sym (fromPathP r)) AssocCong₂⋆L : {x y' y z w : C .ob} → {f' : C [ x , y' ]} {f : C [ x , y ]} {g' : C [ y' , z ]} {g : C [ y , z ]} - → f ⋆⟨ C ⟩ g ≡ f' ⋆⟨ C ⟩ g' → (h : C [ z , w ]) - → f ⋆⟨ C ⟩ (g ⋆⟨ C ⟩ h) ≡ - f' ⋆⟨ C ⟩ (g' ⋆⟨ C ⟩ h) + → f ⋆⟨ C ⟩ g ≡ f' ⋆⟨ C ⟩ g' → (h : C [ z , w ]) + → f ⋆⟨ C ⟩ (g ⋆⟨ C ⟩ h) ≡ + f' ⋆⟨ C ⟩ (g' ⋆⟨ C ⟩ h) AssocCong₂⋆L p h = sym (⋆Assoc C _ _ h) - ∙∙ (λ i → p i ⋆⟨ C ⟩ h) ∙∙ + ∙∙ (λ i → p i ⋆⟨ C ⟩ h) ∙∙ ⋆Assoc C _ _ h AssocCong₂⋆R : {x y z z' w : C .ob} → (f : C [ x , y ]) {g' : C [ y , z' ]} {g : C [ y , z ]} {h' : C [ z' , w ]} {h : C [ z , w ]} - → g ⋆⟨ C ⟩ h ≡ g' ⋆⟨ C ⟩ h' - → (f ⋆⟨ C ⟩ g) ⋆⟨ C ⟩ h ≡ - (f ⋆⟨ C ⟩ g') ⋆⟨ C ⟩ h' + → g ⋆⟨ C ⟩ h ≡ g' ⋆⟨ C ⟩ h' + → (f ⋆⟨ C ⟩ g) ⋆⟨ C ⟩ h ≡ + (f ⋆⟨ C ⟩ g') ⋆⟨ C ⟩ h' AssocCong₂⋆R f p = ⋆Assoc C f _ _ - ∙∙ (λ i → f ⋆⟨ C ⟩ p i) ∙∙ + ∙∙ (λ i → f ⋆⟨ C ⟩ p i) ∙∙ sym (⋆Assoc C _ _ _)Cubical.Categories.Adjoint {-# OPTIONS --safe #-} -module Cubical.Categories.Adjoint where +module Cubical.Categories.Adjoint where -open import Cubical.Foundations.Prelude -open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv -open import Cubical.Data.Sigma -open import Cubical.Categories.Category -open import Cubical.Categories.Functor -open import Cubical.Categories.Instances.Functors -open import Cubical.Categories.NaturalTransformation -open import Cubical.Foundations.Isomorphism -open import Cubical.Foundations.Univalence +open import Cubical.Data.Sigma +open import Cubical.Categories.Category +open import Cubical.Categories.Functor +open import Cubical.Categories.Instances.Functors +open import Cubical.Categories.NaturalTransformation +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Univalence -open Functor +open Functor -open Iso -open Category +open Iso +open Category -{- +{- ============================================== Overview ============================================== @@ -30,11 +30,11 @@ equivalence. -} -private - variable - ℓC ℓC' ℓD ℓD' : Level +private + variable + ℓC ℓC' ℓD ℓD' : Level -{- +{- ============================================== Adjoint definitions ============================================== @@ -45,195 +45,195 @@ definition. -} -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 - - -- Adjoint def 1: unit-counit - record _⊣_ : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where - field - -- unit - η : 𝟙⟨ C ⟩ ⇒ (funcComp G F) - -- counit - ε : (funcComp F G) ⇒ 𝟙⟨ D ⟩ - triangleIdentities : TriangleIdentities η ε - open TriangleIdentities triangleIdentities public - - -private - variable - C : Category ℓC ℓC' - D : Category ℓC ℓC' - - -module _ {F : Functor C D} {G : Functor D C} where - open UnitCounit - open _⊣_ - open NatTrans - open TriangleIdentities - opositeAdjunction : (F ⊣ G) → ((G ^opF) ⊣ (F ^opF)) - N-ob (η (opositeAdjunction x)) = N-ob (ε x) - N-hom (η (opositeAdjunction x)) f = sym (N-hom (ε x) f) - N-ob (ε (opositeAdjunction x)) = N-ob (η x) - N-hom (ε (opositeAdjunction x)) f = sym (N-hom (η x) f) - Δ₁ (triangleIdentities (opositeAdjunction x)) = - Δ₂ (triangleIdentities x) - Δ₂ (triangleIdentities (opositeAdjunction x)) = - Δ₁ (triangleIdentities x) - - Iso⊣^opF : Iso (F ⊣ G) ((G ^opF) ⊣ (F ^opF)) - fun Iso⊣^opF = opositeAdjunction - inv Iso⊣^opF = _ - rightInv Iso⊣^opF _ = refl - leftInv Iso⊣^opF _ = refl - -private - variable - F F' : Functor C D - G G' : Functor D C - - -module AdjointUniqeUpToNatIso where - open UnitCounit - module Left - (F⊣G : _⊣_ {D = D} F G) - (F'⊣G : F' ⊣ G) where - open NatTrans - - private - variable - H H' : Functor C D - - _D⋆_ = seq' D - - m : (H⊣G : H ⊣ G) (H'⊣G : H' ⊣ G) → - ∀ {x} → D [ H ⟅ x ⟆ , H' ⟅ x ⟆ ] - m {H = H} H⊣G H'⊣G = - H ⟪ (H'⊣G .η) ⟦ _ ⟧ ⟫ ⋆⟨ D ⟩ (H⊣G .ε) ⟦ _ ⟧ where open _⊣_ - - private - s : (H⊣G : H ⊣ G) (H'⊣G : H' ⊣ G) → ∀ {x} → - seq' D (m H'⊣G H⊣G {x}) (m H⊣G H'⊣G {x}) - ≡ D .id - s {H = H} {H' = H'} H⊣G H'⊣G = by-N-homs ∙ by-Δs - where - open _⊣_ H⊣G using (η ; Δ₂) - open _⊣_ H'⊣G using (ε ; Δ₁) - by-N-homs = - AssocCong₂⋆R {C = D} _ - (AssocCong₂⋆L {C = D} (sym (N-hom ε _)) _) - ∙ cong₂ _D⋆_ - (sym (F-seq H' _ _) - ∙∙ cong (H' ⟪_⟫) ((sym (N-hom η _))) - ∙∙ F-seq H' _ _) - (sym (N-hom ε _)) - - by-Δs = - ⋆Assoc D _ _ _ - ∙∙ cong (H' ⟪ _ ⟫ D⋆_) - (sym (⋆Assoc D _ _ _) - ∙ cong (_D⋆ ε ⟦ _ ⟧) - ( sym (F-seq H' _ _) - ∙∙ cong (H' ⟪_⟫) (Δ₂ (H' ⟅ _ ⟆)) - ∙∙ F-id H') - ∙ ⋆IdL D _) - ∙∙ Δ₁ _ - - open NatIso - open isIso - - F≅ᶜF' : F ≅ᶜ F' - N-ob (trans F≅ᶜF') _ = _ - N-hom (trans F≅ᶜF') _ = - sym (⋆Assoc D _ _ _) - ∙∙ cong (_D⋆ (F⊣G .ε) ⟦ _ ⟧) - (sym (F-seq F _ _) - ∙∙ cong (F ⟪_⟫) (N-hom (F'⊣G .η) _) - ∙∙ (F-seq F _ _)) - ∙∙ AssocCong₂⋆R {C = D} _ (N-hom (F⊣G .ε) _) - where open _⊣_ - inv (nIso F≅ᶜF' _) = _ - sec (nIso F≅ᶜF' _) = s F⊣G F'⊣G - ret (nIso F≅ᶜF' _) = s F'⊣G F⊣G - - F≡F' : isUnivalent D → F ≡ F' - F≡F' univD = - isUnivalent.CatIsoToPath - (isUnivalentFUNCTOR _ _ univD) - (NatIso→FUNCTORIso _ _ F≅ᶜF') - - module Right (F⊣G : F UnitCounit.⊣ G) - (F⊣G' : F UnitCounit.⊣ G') where - - G≅ᶜG' : G ≅ᶜ G' - G≅ᶜG' = Iso.inv congNatIso^opFiso - (Left.F≅ᶜF' (opositeAdjunction F⊣G') - (opositeAdjunction F⊣G)) - - open NatIso - - G≡G' : isUnivalent _ → G ≡ G' - G≡G' univC = - isUnivalent.CatIsoToPath - (isUnivalentFUNCTOR _ _ univC) - (NatIso→FUNCTORIso _ _ G≅ᶜG') - -module NaturalBijection where - -- Adjoint def 2: natural bijection - 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 + + -- Adjoint def 1: unit-counit + record _⊣_ : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where + field + -- unit + η : 𝟙⟨ C ⟩ ⇒ (funcComp G F) + -- counit + ε : (funcComp F G) ⇒ 𝟙⟨ D ⟩ + triangleIdentities : TriangleIdentities η ε + open TriangleIdentities triangleIdentities public + + +private + variable + C : Category ℓC ℓC' + D : Category ℓC ℓC' + + +module _ {F : Functor C D} {G : Functor D C} where + open UnitCounit + open _⊣_ + open NatTrans + open TriangleIdentities + opositeAdjunction : (F ⊣ G) → ((G ^opF) ⊣ (F ^opF)) + N-ob (η (opositeAdjunction x)) = N-ob (ε x) + N-hom (η (opositeAdjunction x)) f = sym (N-hom (ε x) f) + N-ob (ε (opositeAdjunction x)) = N-ob (η x) + N-hom (ε (opositeAdjunction x)) f = sym (N-hom (η x) f) + Δ₁ (triangleIdentities (opositeAdjunction x)) = + Δ₂ (triangleIdentities x) + Δ₂ (triangleIdentities (opositeAdjunction x)) = + Δ₁ (triangleIdentities x) + + Iso⊣^opF : Iso (F ⊣ G) ((G ^opF) ⊣ (F ^opF)) + fun Iso⊣^opF = opositeAdjunction + inv Iso⊣^opF = _ + rightInv Iso⊣^opF _ = refl + leftInv Iso⊣^opF _ = refl + +private + variable + F F' : Functor C D + G G' : Functor D C + + +module AdjointUniqeUpToNatIso where + open UnitCounit + module Left + (F⊣G : _⊣_ {D = D} F G) + (F'⊣G : F' ⊣ G) where + open NatTrans + + private + variable + H H' : Functor C D + + _D⋆_ = seq' D + + m : (H⊣G : H ⊣ G) (H'⊣G : H' ⊣ G) → + ∀ {x} → D [ H ⟅ x ⟆ , H' ⟅ x ⟆ ] + m {H = H} H⊣G H'⊣G = + H ⟪ (H'⊣G .η) ⟦ _ ⟧ ⟫ ⋆⟨ D ⟩ (H⊣G .ε) ⟦ _ ⟧ where open _⊣_ + + private + s : (H⊣G : H ⊣ G) (H'⊣G : H' ⊣ G) → ∀ {x} → + seq' D (m H'⊣G H⊣G {x}) (m H⊣G H'⊣G {x}) + ≡ D .id + s {H = H} {H' = H'} H⊣G H'⊣G = by-N-homs ∙ by-Δs + where + open _⊣_ H⊣G using (η ; Δ₂) + open _⊣_ H'⊣G using (ε ; Δ₁) + by-N-homs = + AssocCong₂⋆R {C = D} _ + (AssocCong₂⋆L {C = D} (sym (N-hom ε _)) _) + ∙ cong₂ _D⋆_ + (sym (F-seq H' _ _) + ∙∙ cong (H' ⟪_⟫) ((sym (N-hom η _))) + ∙∙ F-seq H' _ _) + (sym (N-hom ε _)) + + by-Δs = + ⋆Assoc D _ _ _ + ∙∙ cong (H' ⟪ _ ⟫ D⋆_) + (sym (⋆Assoc D _ _ _) + ∙ cong (_D⋆ ε ⟦ _ ⟧) + ( sym (F-seq H' _ _) + ∙∙ cong (H' ⟪_⟫) (Δ₂ (H' ⟅ _ ⟆)) + ∙∙ F-id H') + ∙ ⋆IdL D _) + ∙∙ Δ₁ _ + + open NatIso + open isIso + + F≅ᶜF' : F ≅ᶜ F' + N-ob (trans F≅ᶜF') _ = _ + N-hom (trans F≅ᶜF') _ = + sym (⋆Assoc D _ _ _) + ∙∙ cong (_D⋆ (F⊣G .ε) ⟦ _ ⟧) + (sym (F-seq F _ _) + ∙∙ cong (F ⟪_⟫) (N-hom (F'⊣G .η) _) + ∙∙ (F-seq F _ _)) + ∙∙ AssocCong₂⋆R {C = D} _ (N-hom (F⊣G .ε) _) + where open _⊣_ + inv (nIso F≅ᶜF' _) = _ + sec (nIso F≅ᶜF' _) = s F⊣G F'⊣G + ret (nIso F≅ᶜF' _) = s F'⊣G F⊣G + + F≡F' : isUnivalent D → F ≡ F' + F≡F' univD = + isUnivalent.CatIsoToPath + (isUnivalentFUNCTOR _ _ univD) + (NatIso→FUNCTORIso _ _ F≅ᶜF') + + module Right (F⊣G : F UnitCounit.⊣ G) + (F⊣G' : F UnitCounit.⊣ G') where + + G≅ᶜG' : G ≅ᶜ G' + G≅ᶜG' = Iso.inv congNatIso^opFiso + (Left.F≅ᶜF' (opositeAdjunction F⊣G') + (opositeAdjunction F⊣G)) + + open NatIso + + G≡G' : isUnivalent _ → G ≡ G' + G≡G' univC = + isUnivalent.CatIsoToPath + (isUnivalentFUNCTOR _ _ univC) + (NatIso→FUNCTORIso _ _ G≅ᶜG') + +module NaturalBijection where + -- Adjoint def 2: natural bijection + 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 + +{- ============================================== Proofs of equivalence ============================================== @@ -245,160 +245,160 @@ The second unnamed module does the reverse. -} -module _ (F : Functor C D) (G : Functor D C) where - open UnitCounit - open NaturalBijection renaming (_⊣_ to _⊣²_) - module _ (adj : F ⊣² G) where - open _⊣²_ adj - open _⊣_ - - -- Naturality condition implies that a commutative square in C - -- appears iff the transpose in D is commutative as well - -- Used in adj'→adj - adjNat' : ∀ {c c' d d'} {f : D [ F ⟅ c ⟆ , d ]} {k : D [ d , d' ]} - → {h : C [ c , c' ]} {g : C [ c' , G ⟅ d' ⟆ ]} - -- commutativity of squares is iff - → ((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 - - -- note : had to make this record syntax because termination checker was complaining - -- due to referencing η and ε from the definitions of Δs - adj'→adj : F ⊣ G - adj'→adj = record - { η = η' - ; ε = ε' - ; triangleIdentities = record - {Δ₁ = Δ₁' - ; Δ₂ = Δ₂' }} - - where - -- ETA - - -- trivial commutative diagram between identities in D - 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)) - - -- EPSILON - - -- trivial commutative diagram between identities in C - 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)) - - -- DELTA 1 - - Δ₁' : ∀ 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 - ∎ - - -- DELTA 2 - - Δ₂' : ∀ 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 - -- ∀ {c d} → Iso (D [ F ⟅ c ⟆ , d ]) (C [ c , G ⟅ d ⟆ ]) - -- takes f to Gf precomposed with the unit - adj→adj' .adjIso {c = c} .fun f = η ⟦ c ⟧ ⋆⟨ C ⟩ G ⟪ f ⟫ - -- takes g to Fg postcomposed with the counit - adj→adj' .adjIso {d = d} .inv g = F ⟪ g ⟫ ⋆⟨ D ⟩ ε ⟦ d ⟧ - -- invertibility follows from the triangle identities - 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 ⟧ ⟫ - -- apply naturality - ≡⟨ 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 ⟧) - -- apply naturality - ≡⟨ lCatWhisker {C = D} _ _ _ natu ⟩ - F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ (ε ⟦ F ⟅ c ⟆ ⟧ ⋆⟨ D ⟩ f) - ≡⟨ sym (D .⋆Assoc _ _ _) ⟩ - F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε ⟦ F ⟅ c ⟆ ⟧ ⋆⟨ D ⟩ f - -- apply triangle identity - ≡⟨ 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 _ - -- follows directly from functoriality - 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 _ (F : Functor C D) (G : Functor D C) where + open UnitCounit + open NaturalBijection renaming (_⊣_ to _⊣²_) + module _ (adj : F ⊣² G) where + open _⊣²_ adj + open _⊣_ + + -- Naturality condition implies that a commutative square in C + -- appears iff the transpose in D is commutative as well + -- Used in adj'→adj + adjNat' : ∀ {c c' d d'} {f : D [ F ⟅ c ⟆ , d ]} {k : D [ d , d' ]} + → {h : C [ c , c' ]} {g : C [ c' , G ⟅ d' ⟆ ]} + -- commutativity of squares is iff + → ((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 + + -- note : had to make this record syntax because termination checker was complaining + -- due to referencing η and ε from the definitions of Δs + adj'→adj : F ⊣ G + adj'→adj = record + { η = η' + ; ε = ε' + ; triangleIdentities = record + {Δ₁ = Δ₁' + ; Δ₂ = Δ₂' }} + + where + -- ETA + + -- trivial commutative diagram between identities in D + 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)) + + -- EPSILON + + -- trivial commutative diagram between identities in C + 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)) + + -- DELTA 1 + + Δ₁' : ∀ 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 + ∎ + + -- DELTA 2 + + Δ₂' : ∀ 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 + -- ∀ {c d} → Iso (D [ F ⟅ c ⟆ , d ]) (C [ c , G ⟅ d ⟆ ]) + -- takes f to Gf precomposed with the unit + adj→adj' .adjIso {c = c} .fun f = η ⟦ c ⟧ ⋆⟨ C ⟩ G ⟪ f ⟫ + -- takes g to Fg postcomposed with the counit + adj→adj' .adjIso {d = d} .inv g = F ⟪ g ⟫ ⋆⟨ D ⟩ ε ⟦ d ⟧ + -- invertibility follows from the triangle identities + 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 ⟧ ⟫ + -- apply naturality + ≡⟨ 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 ⟧) + -- apply naturality + ≡⟨ lCatWhisker {C = D} _ _ _ natu ⟩ + F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ (ε ⟦ F ⟅ c ⟆ ⟧ ⋆⟨ D ⟩ f) + ≡⟨ sym (D .⋆Assoc _ _ _) ⟩ + F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε ⟦ F ⟅ c ⟆ ⟧ ⋆⟨ D ⟩ f + -- apply triangle identity + ≡⟨ 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 _ + -- follows directly from functoriality + 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 _ _ _\ No newline at end of file diff --git a/docs/Cubical.Categories.Category.Base.html b/docs/Cubical.Categories.Category.Base.html index 1163e41..bd0d8b8 100644 --- a/docs/Cubical.Categories.Category.Base.html +++ b/docs/Cubical.Categories.Category.Base.html @@ -24,7 +24,7 @@ ⋆IdR : ∀ {x y} (f : Hom[ x , y ]) → f ⋆ id ≡ f ⋆Assoc : ∀ {x y z w} (f : Hom[ x , y ]) (g : Hom[ y , z ]) (h : Hom[ z , w ]) → (f ⋆ g) ⋆ h ≡ f ⋆ (g ⋆ h) - isSetHom : ∀ {x y} → isSet Hom[ x , y ] + isSetHom : ∀ {x y} → isSet Hom[ x , y ] -- composition: alternative to diagramatic order _∘_ : ∀ {x y z} (g : Hom[ y , z ]) (f : Hom[ x , y ]) → Hom[ x , z ] @@ -39,119 +39,127 @@ _[_,_] : (C : Category ℓ ℓ') → (x y : C .ob) → Type ℓ' _[_,_] = Hom[_,_] --- Needed to define this in order to be able to make the subsequence syntax declaration -seq' : ∀ (C : Category ℓ ℓ') {x y z} (f : C [ x , y ]) (g : C [ y , z ]) → C [ x , z ] -seq' = _⋆_ +_End[_] : (C : Category ℓ ℓ') → (x : C .ob) → Type ℓ' +C End[ x ] = C [ x , x ] -infixl 15 seq' -syntax seq' C f g = f ⋆⟨ C ⟩ g - --- composition -comp' : ∀ (C : Category ℓ ℓ') {x y z} (g : C [ y , z ]) (f : C [ x , y ]) → C [ x , z ] -comp' = _∘_ - -infixr 16 comp' -syntax comp' C g f = g ∘⟨ C ⟩ f - - --- Isomorphisms and paths in categories - -record isIso (C : Category ℓ ℓ'){x y : C .ob}(f : C [ x , y ]) : Type ℓ' where - constructor isiso - field - inv : C [ y , x ] - sec : inv ⋆⟨ C ⟩ f ≡ C .id - ret : f ⋆⟨ C ⟩ inv ≡ C .id - -open isIso - -isPropIsIso : {C : Category ℓ ℓ'}{x y : C .ob}(f : C [ x , y ]) → isProp (isIso C f) -isPropIsIso {C = C} f p q i .inv = - (sym (C .⋆IdL _) - ∙ (λ i → q .sec (~ i) ⋆⟨ C ⟩ p .inv) - ∙ C .⋆Assoc _ _ _ - ∙ (λ i → q .inv ⋆⟨ C ⟩ p .ret i) - ∙ C .⋆IdR _) i -isPropIsIso {C = C} f p q i .sec j = - isSet→SquareP (λ i j → C .isSetHom) - (p .sec) (q .sec) (λ i → isPropIsIso {C = C} f p q i .inv ⋆⟨ C ⟩ f) refl i j -isPropIsIso {C = C} f p q i .ret j = - isSet→SquareP (λ i j → C .isSetHom) - (p .ret) (q .ret) (λ i → f ⋆⟨ C ⟩ isPropIsIso {C = C} f p q i .inv) refl i j - -CatIso : (C : Category ℓ ℓ') (x y : C .ob) → Type ℓ' -CatIso C x y = Σ[ f ∈ C [ x , y ] ] isIso C f - -CatIso≡ : {C : Category ℓ ℓ'}{x y : C .ob}(f g : CatIso C x y) → f .fst ≡ g .fst → f ≡ g -CatIso≡ f g = Σ≡Prop isPropIsIso - --- `constructor` of CatIso -catiso : {C : Category ℓ ℓ'}{x y : C .ob} - → (mor : C [ x , y ]) - → (inv : C [ y , x ]) - → (sec : inv ⋆⟨ C ⟩ mor ≡ C .id) - → (ret : mor ⋆⟨ C ⟩ inv ≡ C .id) - → CatIso C x y -catiso mor inv sec ret = mor , isiso inv sec ret - - -idCatIso : {C : Category ℓ ℓ'} {x : C .ob} → CatIso C x x -idCatIso {C = C} = C .id , isiso (C .id) (C .⋆IdL (C .id)) (C .⋆IdL (C .id)) - -isSet-CatIso : {C : Category ℓ ℓ'} → ∀ x y → isSet (CatIso C x y) -isSet-CatIso {C = C} x y = isOfHLevelΣ 2 (C .isSetHom) (λ f → isProp→isSet (isPropIsIso f)) - - -pathToIso : {C : Category ℓ ℓ'} {x y : C .ob} (p : x ≡ y) → CatIso C x y -pathToIso {C = C} p = J (λ z _ → CatIso C _ z) idCatIso p - -pathToIso-refl : {C : Category ℓ ℓ'} {x : C .ob} → pathToIso {C = C} {x} refl ≡ idCatIso -pathToIso-refl {C = C} {x} = JRefl (λ z _ → CatIso C x z) (idCatIso) - - --- Univalent Categories -record isUnivalent (C : Category ℓ ℓ') : Type (ℓ-max ℓ ℓ') where - field - univ : (x y : C .ob) → isEquiv (pathToIso {C = C} {x = x} {y = y}) - - -- package up the univalence equivalence - univEquiv : ∀ (x y : C .ob) → (x ≡ y) ≃ (CatIso _ x y) - univEquiv x y = pathToIso , univ x y - - -- The function extracting paths from category-theoretic isomorphisms. - CatIsoToPath : {x y : C .ob} (p : CatIso _ x y) → x ≡ y - CatIsoToPath = invEq (univEquiv _ _) - - isGroupoid-ob : isGroupoid (C .ob) - isGroupoid-ob = isOfHLevelPath'⁻ 2 (λ _ _ → isOfHLevelRespectEquiv 2 (invEquiv (univEquiv _ _)) (isSet-CatIso _ _)) - - --- Opposite category -_^op : Category ℓ ℓ' → Category ℓ ℓ' -ob (C ^op) = ob C -Hom[_,_] (C ^op) x y = C [ y , x ] -id (C ^op) = id C -_⋆_ (C ^op) f g = g ⋆⟨ C ⟩ f -⋆IdL (C ^op) = C .⋆IdR -⋆IdR (C ^op) = C .⋆IdL -⋆Assoc (C ^op) f g h = sym (C .⋆Assoc _ _ _) -isSetHom (C ^op) = C .isSetHom - -ΣPropCat : (C : Category ℓ ℓ') (P : ℙ (ob C)) → Category ℓ ℓ' -ob (ΣPropCat C P) = Σ[ x ∈ ob C ] x ∈ P -Hom[_,_] (ΣPropCat C P) x y = C [ fst x , fst y ] -id (ΣPropCat C P) = id C -_⋆_ (ΣPropCat C P) = _⋆_ C -⋆IdL (ΣPropCat C P) = ⋆IdL C -⋆IdR (ΣPropCat C P) = ⋆IdR C -⋆Assoc (ΣPropCat C P) = ⋆Assoc C -isSetHom (ΣPropCat C P) = isSetHom C - -isIsoΣPropCat : {C : Category ℓ ℓ'} {P : ℙ (ob C)} - {x y : ob C} (p : x ∈ P) (q : y ∈ P) - (f : C [ x , y ]) - → isIso C f → isIso (ΣPropCat C P) {x , p} {y , q} f -inv (isIsoΣPropCat p q f isIsoF) = isIsoF .inv -sec (isIsoΣPropCat p q f isIsoF) = isIsoF .sec -ret (isIsoΣPropCat p q f isIsoF) = isIsoF .ret + +-- Needed to define this in order to be able to make the subsequence syntax declaration +seq' : ∀ (C : Category ℓ ℓ') {x y z} (f : C [ x , y ]) (g : C [ y , z ]) → C [ x , z ] +seq' = _⋆_ + +infixl 15 seq' +syntax seq' C f g = f ⋆⟨ C ⟩ g + +-- composition +comp' : ∀ (C : Category ℓ ℓ') {x y z} (g : C [ y , z ]) (f : C [ x , y ]) → C [ x , z ] +comp' = _∘_ + +infixr 16 comp' +syntax comp' C g f = g ∘⟨ C ⟩ f + + +-- Isomorphisms and paths in categories + +record isIso (C : Category ℓ ℓ'){x y : C .ob}(f : C [ x , y ]) : Type ℓ' where + constructor isiso + field + inv : C [ y , x ] + sec : inv ⋆⟨ C ⟩ f ≡ C .id + ret : f ⋆⟨ C ⟩ inv ≡ C .id + +open isIso + +isPropIsIso : {C : Category ℓ ℓ'}{x y : C .ob}(f : C [ x , y ]) → isProp (isIso C f) +isPropIsIso {C = C} f p q i .inv = + (sym (C .⋆IdL _) + ∙ (λ i → q .sec (~ i) ⋆⟨ C ⟩ p .inv) + ∙ C .⋆Assoc _ _ _ + ∙ (λ i → q .inv ⋆⟨ C ⟩ p .ret i) + ∙ C .⋆IdR _) i +isPropIsIso {C = C} f p q i .sec j = + isSet→SquareP (λ i j → C .isSetHom) + (p .sec) (q .sec) (λ i → isPropIsIso {C = C} f p q i .inv ⋆⟨ C ⟩ f) refl i j +isPropIsIso {C = C} f p q i .ret j = + isSet→SquareP (λ i j → C .isSetHom) + (p .ret) (q .ret) (λ i → f ⋆⟨ C ⟩ isPropIsIso {C = C} f p q i .inv) refl i j + +CatIso : (C : Category ℓ ℓ') (x y : C .ob) → Type ℓ' +CatIso C x y = Σ[ f ∈ C [ x , y ] ] isIso C f + +CatIso≡ : {C : Category ℓ ℓ'}{x y : C .ob}(f g : CatIso C x y) → f .fst ≡ g .fst → f ≡ g +CatIso≡ f g = Σ≡Prop isPropIsIso + +-- `constructor` of CatIso +catiso : {C : Category ℓ ℓ'}{x y : C .ob} + → (mor : C [ x , y ]) + → (inv : C [ y , x ]) + → (sec : inv ⋆⟨ C ⟩ mor ≡ C .id) + → (ret : mor ⋆⟨ C ⟩ inv ≡ C .id) + → CatIso C x y +catiso mor inv sec ret = mor , isiso inv sec ret + + +idCatIso : {C : Category ℓ ℓ'} {x : C .ob} → CatIso C x x +idCatIso {C = C} = C .id , isiso (C .id) (C .⋆IdL (C .id)) (C .⋆IdL (C .id)) + +isSet-CatIso : {C : Category ℓ ℓ'} → ∀ x y → isSet (CatIso C x y) +isSet-CatIso {C = C} x y = isOfHLevelΣ 2 (C .isSetHom) (λ f → isProp→isSet (isPropIsIso f)) + + +pathToIso : {C : Category ℓ ℓ'} {x y : C .ob} (p : x ≡ y) → CatIso C x y +pathToIso {C = C} p = J (λ z _ → CatIso C _ z) idCatIso p + +pathToIso-refl : {C : Category ℓ ℓ'} {x : C .ob} → pathToIso {C = C} {x} refl ≡ idCatIso +pathToIso-refl {C = C} {x} = JRefl (λ z _ → CatIso C x z) (idCatIso) + + +-- Univalent Categories +record isUnivalent (C : Category ℓ ℓ') : Type (ℓ-max ℓ ℓ') where + field + univ : (x y : C .ob) → isEquiv (pathToIso {C = C} {x = x} {y = y}) + + -- package up the univalence equivalence + univEquiv : ∀ (x y : C .ob) → (x ≡ y) ≃ (CatIso _ x y) + univEquiv x y = pathToIso , univ x y + + -- The function extracting paths from category-theoretic isomorphisms. + CatIsoToPath : {x y : C .ob} (p : CatIso _ x y) → x ≡ y + CatIsoToPath = invEq (univEquiv _ _) + + isGroupoid-ob : isGroupoid (C .ob) + isGroupoid-ob = isOfHLevelPath'⁻ 2 (λ _ _ → isOfHLevelRespectEquiv 2 (invEquiv (univEquiv _ _)) (isSet-CatIso _ _)) + +isPropIsUnivalent : {C : Category ℓ ℓ'} → isProp (isUnivalent C) +isPropIsUnivalent = + isPropRetract isUnivalent.univ _ (λ _ → refl) + (isPropΠ2 λ _ _ → isPropIsEquiv _ ) + +-- Opposite category +_^op : Category ℓ ℓ' → Category ℓ ℓ' +ob (C ^op) = ob C +Hom[_,_] (C ^op) x y = C [ y , x ] +id (C ^op) = id C +_⋆_ (C ^op) f g = g ⋆⟨ C ⟩ f +⋆IdL (C ^op) = C .⋆IdR +⋆IdR (C ^op) = C .⋆IdL +⋆Assoc (C ^op) f g h = sym (C .⋆Assoc _ _ _) +isSetHom (C ^op) = C .isSetHom + +ΣPropCat : (C : Category ℓ ℓ') (P : ℙ (ob C)) → Category ℓ ℓ' +ob (ΣPropCat C P) = Σ[ x ∈ ob C ] x ∈ P +Hom[_,_] (ΣPropCat C P) x y = C [ fst x , fst y ] +id (ΣPropCat C P) = id C +_⋆_ (ΣPropCat C P) = _⋆_ C +⋆IdL (ΣPropCat C P) = ⋆IdL C +⋆IdR (ΣPropCat C P) = ⋆IdR C +⋆Assoc (ΣPropCat C P) = ⋆Assoc C +isSetHom (ΣPropCat C P) = isSetHom C + +isIsoΣPropCat : {C : Category ℓ ℓ'} {P : ℙ (ob C)} + {x y : ob C} (p : x ∈ P) (q : y ∈ P) + (f : C [ x , y ]) + → isIso C f → isIso (ΣPropCat C P) {x , p} {y , q} f +inv (isIsoΣPropCat p q f isIsoF) = isIsoF .inv +sec (isIsoΣPropCat p q f isIsoF) = isIsoF .sec +ret (isIsoΣPropCat p q f isIsoF) = isIsoF .ret