Free category with terminal object (#79)

Co-authored-by: Max New <[email protected]>

Cubical/Categories/Constructions/Free/CategoryWithTerminal.agda

@@ -0,0 +1,128 @@
+-- Free category with a terminal object, over a Quiver
+module Cubical.Categories.Constructions.Free.CategoryWithTerminal where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Categories.Category.Base
+open import Cubical.Categories.Limits.Terminal.More
+open import Cubical.Data.Quiver.Base
+open import Cubical.Data.Sum.Base as Sum hiding (elim)
+open import Cubical.Data.Unit
+open import Cubical.Categories.Displayed.Base
+open import Cubical.Categories.Presheaf
+open import Cubical.Categories.Displayed.Presheaf
+open import Cubical.Categories.Displayed.Limits.Terminal
+open import Cubical.Foundations.Equiv
+open import Cubical.Data.Sigma.Properties
+open import Cubical.Categories.Displayed.Section.Base
+
+private
+  variable
+    ℓg ℓg' ℓC ℓC' ℓCᴰ ℓCᴰ' : Level
+
+CategoryWithTerminal' : (ℓC ℓC' : Level) → Type _
+CategoryWithTerminal' ℓC ℓC' = Σ[ C ∈ Category ℓC ℓC' ] Terminal' C
+
+-- freely throw in a terminal object
+module _ (Ob : Type ℓg) where
+
+  -- adjoin a new terminal object
+  Ob' = Ob ⊎ Unit
+
+  𝟙' : Ob'
+  𝟙' = inr tt
+
+  module _ (Q : QuiverOver Ob' ℓg') where
+    open Category
+    open QuiverOver
+    open UniversalElement
+
+    -- copied from Categories.Constructions.Free.Category.Quiver
+    -- and suitably modified
+    data Exp : Ob' → Ob' → Type (ℓ-max ℓg ℓg') where
+      ↑_   : ∀ g → Exp (Q .dom g) (Q .cod g)
+      idₑ  : ∀ {A} → Exp A A
+      _⋆ₑ_ : ∀ {A B C} → (e : Exp A B) → (e' : Exp B C) → Exp A C
+      ⋆ₑIdL : ∀ {A B} (e : Exp A B) → idₑ ⋆ₑ e ≡ e
+      ⋆ₑIdR : ∀ {A B} (e : Exp A B) → e ⋆ₑ idₑ ≡ e
+      ⋆ₑAssoc : ∀ {A B C D} (e : Exp A B)(f : Exp B C)(g : Exp C D)
+              → (e ⋆ₑ f) ⋆ₑ g ≡ e ⋆ₑ (f ⋆ₑ g)
+      isSetExp : ∀ {A B} → isSet (Exp A B)
+      !ₑ : ∀ {A} → Exp A 𝟙'
+      isProp!ₑ : ∀ {A} → isProp (Exp A 𝟙')
+
+    FC : Category _ _
+    FC .ob = Ob'
+    FC .Hom[_,_] = Exp
+    FC .id = idₑ
+    FC ._⋆_ = _⋆ₑ_
+    FC .⋆IdL = ⋆ₑIdL
+    FC .⋆IdR = ⋆ₑIdR
+    FC .⋆Assoc = ⋆ₑAssoc
+    FC .isSetHom = isSetExp
+
+    FCTerminal' : Terminal' FC
+    FCTerminal' .vertex = inr tt
+    FCTerminal' .element = tt
+    FCTerminal' .universal A .equiv-proof y =
+      uniqueExists !ₑ refl (λ _ _ _ → refl) (λ _ _ → isProp!ₑ _ _)
+
+    FreeCatw/Terminal' : CategoryWithTerminal' _ _
+    FreeCatw/Terminal' = (FC , FCTerminal')
+
+    module _ (Cᴰ : Categoryᴰ (FreeCatw/Terminal' .fst) ℓCᴰ ℓCᴰ')
+      (term'ᴰ : Terminalᴰ Cᴰ (FreeCatw/Terminal' .snd)) where
+
+      open import Cubical.Foundations.HLevels
+      open import Cubical.Categories.Displayed.Reasoning
+      open Section
+      open UniversalElementᴰ
+      open TerminalᴰNotation Cᴰ term'ᴰ
+
+      private
+        module FC = Category (FreeCatw/Terminal' .fst)
+        module Cᴰ = Categoryᴰ Cᴰ
+
+      -- given an interpretation of atomic objects
+      module _ (ϕ : (v : Ob) → Cᴰ.ob[ inl v ]) where
+        -- extend it to all objects
+        ϕ* : (v : Ob') → Cᴰ.ob[ v ]
+        ϕ* = Sum.elim (λ a → ϕ a) (λ b → term'ᴰ .vertexᴰ)
+
+        -- and given an interpretation of atomic morphisms
+        module _ (ψ : (e : Q .mor) →
+          Cᴰ.Hom[ ↑ e ][ ϕ* (Q .dom e) , ϕ* (Q .cod e) ]) where
+
+          -- extend it to all morphisms
+          -- (copied from
+          -- Cubical.Categories.Constructions.Free.Category.Quiver)
+          elim-F-homᴰ : ∀ {d d'} → (f : FC.Hom[ d , d' ]) →
+            Cᴰ.Hom[ f ][ ϕ* d , ϕ* d' ]
+          elim-F-homᴰ (↑ g) = ψ g
+          elim-F-homᴰ idₑ = Cᴰ.idᴰ
+          elim-F-homᴰ (f ⋆ₑ g) = elim-F-homᴰ f Cᴰ.⋆ᴰ elim-F-homᴰ g
+          elim-F-homᴰ (⋆ₑIdL f i) = Cᴰ.⋆IdLᴰ (elim-F-homᴰ f) i
+          elim-F-homᴰ (⋆ₑIdR f i) = Cᴰ.⋆IdRᴰ (elim-F-homᴰ f) i
+          elim-F-homᴰ (⋆ₑAssoc f g h i) = Cᴰ.⋆Assocᴰ
+            (elim-F-homᴰ f) (elim-F-homᴰ g) (elim-F-homᴰ h) i
+          elim-F-homᴰ (isSetExp f g p q i j) =
+            isOfHLevel→isOfHLevelDep 2
+            ((λ x → Cᴰ.isSetHomᴰ))
+            ((elim-F-homᴰ f)) ((elim-F-homᴰ g))
+            ((cong elim-F-homᴰ p)) ((cong elim-F-homᴰ q))
+            ((isSetExp f g p q))
+            i j
+          elim-F-homᴰ {d = d} !ₑ = !tᴰ (ϕ* d)
+          elim-F-homᴰ {d = d} (isProp!ₑ f g i) = goal i
+            where
+            goal : elim-F-homᴰ f Cᴰ.≡[ isProp!ₑ f g ] elim-F-homᴰ g
+            goal = ≡[]-rectify Cᴰ
+              (≡[]∙ Cᴰ _ _
+              (𝟙ηᴰ {f = f} (elim-F-homᴰ f))
+              (symP (𝟙ηᴰ {f = g} (elim-F-homᴰ g))))
+
+          elim : GlobalSection Cᴰ
+          elim .F-obᴰ = ϕ*
+          elim .F-homᴰ = elim-F-homᴰ
+          elim .F-idᴰ = refl
+          elim .F-seqᴰ _ _ = refl

Cubical/Categories/Displayed/Limits/Terminal.agda

@@ -13,6 +13,7 @@ open import Cubical.Categories.Category
 open import Cubical.Categories.Presheaf
 open import Cubical.Categories.Instances.Sets
 open import Cubical.Categories.Displayed.Base
+open import Cubical.Categories.Displayed.Reasoning as HomᴰReasoning
 open import Cubical.Categories.Displayed.Presheaf
 open import Cubical.Categories.Displayed.Functor
 open import Cubical.Categories.Limits.Terminal
@@ -47,6 +48,24 @@ module _ {C : Category ℓC ℓC'} (D : Categoryᴰ C ℓD ℓD') where
   Terminalᴰ : (term : Terminal' C) → Type (ℓ-max (ℓ-max (ℓ-max ℓC ℓC') ℓD) ℓD')
   Terminalᴰ term = UniversalElementᴰ _ TerminalᴰSpec term
 
+  module TerminalᴰNotation {term' : Terminal' C} (termᴰ : Terminalᴰ term') where
+    open UniversalElement
+    open UniversalElementᴰ
+    open Terminal'Notation term'
+    private module R = HomᴰReasoning D
+
+    𝟙ᴰ : D.ob[ 𝟙 ]
+    𝟙ᴰ = termᴰ .vertexᴰ
+
+    !tᴰ : ∀ {c} (d : D.ob[ c ]) → D.Hom[ !t ][ d , 𝟙ᴰ ]
+    !tᴰ {c} d = termᴰ .universalᴰ .equiv-proof tt .fst .fst
+
+    𝟙ηᴰ : ∀ {c} {d : D.ob[ c ]} {f} (fᴰ : D.Hom[ f ][ d , 𝟙ᴰ ])
+        → fᴰ D.≡[ 𝟙η f ] !tᴰ d
+    𝟙ηᴰ {c} {d} {f} fᴰ = R.≡[]-rectify (toPathP (sym fᴰ-commutes))
+      where contr!tᴰ = termᴰ .universalᴰ {c}{d}{ !t } .equiv-proof tt
+            fᴰ-commutes = cong fst (contr!tᴰ .snd (reind D (𝟙η _) fᴰ , refl))
+
   module _ (c : C .ob) where
     -- Terminal object of the fiber of a fixed object
 

Cubical/Categories/Limits/Terminal/More.agda

@@ -54,6 +54,13 @@ terminalToUniversalElement {C = C} One .universal x = isoToIsEquiv (iso
   (λ b i → tt)
   λ a → terminalArrowUnique C {T = One} a)
 
+Terminal'ToTerminal : ∀ {C : Category ℓc ℓc'} → Terminal' C → Terminal C
+Terminal'ToTerminal term' .fst = term' .vertex
+Terminal'ToTerminal term' .snd c =
+  contr!t .fst .fst
+  , (λ !t' → cong fst (contr!t .snd (!t' , refl)) )
+  where contr!t = term' .universal c .equiv-proof tt
+
 module TerminalNotation (C : Category ℓ ℓ') (term : Terminal C) where
   𝟙 = term .fst
 
@@ -65,3 +72,6 @@ module TerminalNotation (C : Category ℓ ℓ') (term : Terminal C) where
 
   𝟙η' : ∀ {a} → {f g : C [ a , 𝟙 ]} → f ≡ g
   𝟙η' = 𝟙η _ ∙ sym (𝟙η _)
+
+module Terminal'Notation {ℓ}{ℓ'} {C : Category ℓ ℓ'} (term' : Terminal' C)
+  = TerminalNotation C (Terminal'ToTerminal term')