Split initial and terminal objects into separate files and rewrite

Cubical/Categories/Constructions/Quotient.agda

@@ -6,6 +6,7 @@ module Cubical.Categories.Constructions.Quotient where
 open import Cubical.Categories.Category.Base
 open import Cubical.Categories.Functor.Base
 open import Cubical.Categories.Limits.Terminal
+open import Cubical.Categories.Limits.Initial
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Prelude
 open import Cubical.HITs.SetQuotients renaming ([_] to ⟦_⟧)
@@ -77,6 +78,6 @@ module _ (C : Category ℓ ℓ') where
     isInitial/~ zInit x = ⟦ zInit x .fst ⟧ , elimProp (λ _ → squash/ _ _)
         λ f → eq/ _ _ (subst (_~ f) (sym (zInit x .snd f)) (~refl _))
 
-    isFinal/~ : {z : ob C} → isFinal C z → isFinal C/~ z
-    isFinal/~ zFinal x = ⟦ zFinal x .fst ⟧ , elimProp (λ _ → squash/ _ _)
-        λ f → eq/ _ _ (subst (_~ f) (sym (zFinal x .snd f)) (~refl _))
+    isTerminal/~ : {z : ob C} → isTerminal C z → isTerminal C/~ z
+    isTerminal/~ zTerminal x = ⟦ zTerminal x .fst ⟧ , elimProp (λ _ → squash/ _ _)
+        λ f → eq/ _ _ (subst (_~ f) (sym (zTerminal x .snd f)) (~refl _))

Cubical/Categories/Limits.agda

@@ -2,5 +2,6 @@
 module Cubical.Categories.Limits where
 
 open import Cubical.Categories.Limits.Base public
+open import Cubical.Categories.Limits.Initial public
 open import Cubical.Categories.Limits.Terminal public
 open import Cubical.Categories.Limits.Pullback public

Cubical/Categories/Limits/Initial.agda

@@ -0,0 +1,61 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Limits.Initial where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.HITs.PropositionalTruncation.Base
+
+open import Cubical.Data.Sigma
+
+open import Cubical.Categories.Category
+
+private
+  variable
+    ℓ ℓ' : Level
+
+module _ (C : Category ℓ ℓ') where
+  open Category C
+
+  isInitial : (x : ob) → Type (ℓ-max ℓ ℓ')
+  isInitial x = ∀ (y : ob) → isContr (C [ x , y ])
+
+  Initial : Type (ℓ-max ℓ ℓ')
+  Initial = Σ[ x ∈ ob ] isInitial x
+
+  initialOb : Initial → ob
+  initialOb = fst
+
+  initialArrow : (T : Initial) (y : ob) → C [ initialOb T , y ]
+  initialArrow T y = T .snd y .fst
+
+  initialArrowUnique : {T : Initial} {y : ob} (f : C [ initialOb T , y ])
+                      → initialArrow T y ≡ f
+  initialArrowUnique {T} {y} f = T .snd y .snd f
+
+  initialEndoIsId : (T : Initial) (f : C [ initialOb T , initialOb T ])
+                   → f ≡ id
+  initialEndoIsId T f = isContr→isProp (T .snd (initialOb T)) f id
+
+  hasInitial : Type (ℓ-max ℓ ℓ')
+  hasInitial = ∥ Initial ∥
+
+  -- Initiality of an object is a proposition.
+  isPropIsInitial : (x : ob) → isProp (isInitial x)
+  isPropIsInitial _ = isPropΠ λ _ → isPropIsContr
+
+  open CatIso
+
+  -- Objects that are initial are isomorphic.
+  initialToIso : (x y : Initial) → CatIso C (initialOb x) (initialOb y)
+  mor (initialToIso x y) = initialArrow x (initialOb y)
+  inv (initialToIso x y) = initialArrow y (initialOb x)
+  sec (initialToIso x y) = initialEndoIsId y _
+  ret (initialToIso x y) = initialEndoIsId x _
+
+  open isUnivalent
+
+  -- The type of initial objects of a univalent category is a proposition,
+  -- i.e. all initial objects are equal.
+  isPropInitial : (hC : isUnivalent C) → isProp Initial
+  isPropInitial hC x y =
+    Σ≡Prop isPropIsInitial (CatIsoToPath hC (initialToIso x y))

Cubical/Categories/Limits/Terminal.agda

@@ -1,13 +1,13 @@
 {-# OPTIONS --safe #-}
-
 module Cubical.Categories.Limits.Terminal where
 
 open import Cubical.Foundations.Prelude
-open import Cubical.Data.Sigma
 open import Cubical.Foundations.HLevels
--- open import Cubical.Categories.Limits.Base
+open import Cubical.HITs.PropositionalTruncation.Base
+
+open import Cubical.Data.Sigma
+
 open import Cubical.Categories.Category
-open import Cubical.Categories.Functor
 
 private
   variable
@@ -16,72 +16,46 @@ private
 module _ (C : Category ℓ ℓ') where
   open Category C
 
-  isInitial : (x : ob) → Type (ℓ-max ℓ ℓ')
-  isInitial x = ∀ (y : ob) → isContr (C [ x , y ])
+  isTerminal : (x : ob) → Type (ℓ-max ℓ ℓ')
+  isTerminal x = ∀ (y : ob) → isContr (C [ y , x ])
 
-  isFinal : (x : ob) → Type (ℓ-max ℓ ℓ')
-  isFinal x = ∀ (y : ob) → isContr (C [ y , x ])
+  Terminal : Type (ℓ-max ℓ ℓ')
+  Terminal = Σ[ x ∈ ob ] isTerminal x
 
-  hasInitialOb : Type (ℓ-max ℓ ℓ')
-  hasInitialOb = Σ[ x ∈ ob ] isInitial x
+  terminalOb : Terminal → ob
+  terminalOb = fst
 
-  hasFinalOb : Type (ℓ-max ℓ ℓ')
-  hasFinalOb = Σ[ x ∈ ob ] isFinal x
+  terminalArrow : (T : Terminal) (y : ob) → C [ y , terminalOb T ]
+  terminalArrow T y = T .snd y .fst
 
-  -- Initiality of an object is a proposition.
-  isPropIsInitial : (x : ob) → isProp (isInitial x)
-  isPropIsInitial x = isPropΠ λ y → isPropIsContr
+  terminalArrowUnique : {T : Terminal} {y : ob} (f : C [ y , terminalOb T ])
+                      → terminalArrow T y ≡ f
+  terminalArrowUnique {T} {y} f = T .snd y .snd f
 
-  -- Objects that are initial are isomorphic.
-  isInitialToIso : {x y : ob} (hx : isInitial x) (hy : isInitial y) →
-    CatIso C x y
-  isInitialToIso {x = x} {y = y} hx hy =
-    let x→y : C [ x , y ]
-        x→y = fst (hx y) -- morphism forwards
-        y→x : C [ y , x ]
-        y→x = fst (hy x) -- morphism backwards
-        x→y→x : x→y ⋆⟨ C ⟩ y→x ≡ id
-        x→y→x = isContr→isProp (hx x) _ _ -- compose to id by uniqueness
-        y→x→y : y→x ⋆⟨ C ⟩ x→y ≡ id
-        y→x→y = isContr→isProp (hy y) _ _ -- similar.
-    in catiso x→y y→x y→x→y x→y→x
+  terminalEndoIsId : (T : Terminal) (f : C [ terminalOb T , terminalOb T ])
+                   → f ≡ id
+  terminalEndoIsId T f = isContr→isProp (T .snd (terminalOb T)) f id
 
-  open isUnivalent
-
-  -- The type of initial objects of a univalent category is a proposition,
-  -- i.e. all initial objects are equal.
-  isPropInitial : (hC : isUnivalent C) → isProp (hasInitialOb)
-  isPropInitial hC x y =
-    -- Being initial is a prop ∴ Suffices equal as objects in C.
-    Σ≡Prop (isPropIsInitial)
-    -- C is univalent ∴ Suffices isomorphic as objects in C.
-    (CatIsoToPath hC (isInitialToIso (snd x) (snd y)))
+  hasTerminal : Type (ℓ-max ℓ ℓ')
+  hasTerminal = ∥ Terminal ∥
 
-  -- Now the dual argument for final objects.
+  -- Terminality of an object is a proposition.
+  isPropIsTerminal : (x : ob) → isProp (isTerminal x)
+  isPropIsTerminal _ = isPropΠ λ _ → isPropIsContr
 
-  -- Finality of an object is a proposition.
-  isPropIsFinal : (x : ob) → isProp (isFinal x)
-  isPropIsFinal x = isPropΠ λ y → isPropIsContr
+  open CatIso
 
   -- Objects that are initial are isomorphic.
-  isFinalToIso : {x y : ob} (hx : isFinal x) (hy : isFinal y) →
-    CatIso C x y
-  isFinalToIso {x = x} {y = y} hx hy =
-    let x→y : C [ x , y ]
-        x→y = fst (hy x) -- morphism forwards
-        y→x : C [ y , x ]
-        y→x = fst (hx y) -- morphism backwards
-        x→y→x : x→y ⋆⟨ C ⟩ y→x ≡ id
-        x→y→x = isContr→isProp (hx x) _ _ -- compose to id by uniqueness
-        y→x→y : y→x ⋆⟨ C ⟩ x→y ≡ id
-        y→x→y = isContr→isProp (hy y) _ _ -- similar.
-    in catiso x→y y→x y→x→y x→y→x
-
-  -- The type of final objects of a univalent category is a proposition,
-  -- i.e. all final objects are equal.
-  isPropFinal : (hC : isUnivalent C) → isProp (hasFinalOb)
-  isPropFinal hC x y =
-    -- Being final is a prop ∴ Suffices equal as objects in C.
-    Σ≡Prop isPropIsFinal
-    -- C is univalent ∴ Suffices isomorphic as objects in C.
-    (CatIsoToPath hC (isFinalToIso (snd x) (snd y)))
+  terminalToIso : (x y : Terminal) → CatIso C (terminalOb x) (terminalOb y)
+  mor (terminalToIso x y) = terminalArrow y (terminalOb x)
+  inv (terminalToIso x y) = terminalArrow x (terminalOb y)
+  sec (terminalToIso x y) = terminalEndoIsId y _
+  ret (terminalToIso x y) = terminalEndoIsId x _
+
+  open isUnivalent
+
+  -- The type of terminal objects of a univalent category is a proposition,
+  -- i.e. all terminal objects are equal.
+  isPropTerminal : (hC : isUnivalent C) → isProp Terminal
+  isPropTerminal hC x y =
+    Σ≡Prop isPropIsTerminal (CatIsoToPath hC (terminalToIso x y))