initial objects in a CCC are strict

src/Categories/Category/CartesianClosed/Properties.agda

@@ -1,53 +1,109 @@
 {-# OPTIONS --without-K --safe #-}
 
-module Categories.Category.CartesianClosed.Properties where
 
 open import Level
 open import Data.Product using (Σ; _,_; Σ-syntax; proj₁; proj₂)
 
 open import Categories.Category.BinaryProducts using (BinaryProducts)
 open import Categories.Category.Cartesian using (Cartesian)
-open import Categories.Category.CartesianClosed using (CartesianClosed)
+open import Categories.Category.CartesianClosed using (CartesianClosed; module CartesianMonoidalClosed)
+open import Categories.Category.Monoidal.Closed using (Closed)
 open import Categories.Category.Core using (Category)
 open import Categories.Object.Terminal
+open import Categories.Diagram.Colimit
+open import Categories.Adjoint.Properties using (lapc)
 
 import Categories.Morphism.Reasoning as MR
 
-module _ {o ℓ e} {𝒞 : Category o ℓ e} (𝓥 : CartesianClosed 𝒞) where
-  open Category 𝒞
-  open CartesianClosed 𝓥 using (_^_; eval′; cartesian)
-  open Cartesian cartesian using (products; terminal)
-  open BinaryProducts products
-  open Terminal terminal using (⊤)
-  open HomReasoning
-  open MR 𝒞
-
-  PointSurjective : ∀ {A X Y : Obj} → (X ⇒ Y ^ A) → Set (ℓ ⊔ e)
-  PointSurjective {A = A} {X = X} {Y = Y} ϕ =
-    ∀ (f : A ⇒ Y) → Σ[ x ∈ ⊤ ⇒ X ] (∀ (a : ⊤ ⇒ A) → eval′ ∘ first ϕ ∘ ⟨ x , a ⟩  ≈ f ∘ a)
-
-  lawvere-fixed-point : ∀ {A B : Obj} → (ϕ : A ⇒ B ^ A) → PointSurjective ϕ → (f : B ⇒ B) → Σ[ s ∈ ⊤ ⇒ B ] f ∘ s ≈ s
-  lawvere-fixed-point {A = A} {B = B} ϕ surjective f = g ∘ x , g-fixed-point
-    where
-      g : A ⇒ B
-      g = f ∘ eval′ ∘ ⟨ ϕ , id ⟩
-
-      x : ⊤ ⇒ A
-      x = proj₁ (surjective  g)
-
-      g-surjective : eval′ ∘ first ϕ ∘ ⟨ x , x ⟩ ≈ g ∘ x
-      g-surjective = proj₂ (surjective g) x
-
-      lemma : ∀ {A B C D} → (f : B ⇒ C) → (g : B ⇒ D) → (h : A ⇒ B) → (f ⁂ g) ∘ ⟨ h , h ⟩ ≈ ⟨ f , g ⟩ ∘ h
-      lemma f g h = begin
-        (f ⁂ g) ∘ ⟨ h , h ⟩ ≈⟨  ⁂∘⟨⟩ ⟩
-        ⟨ f ∘ h , g ∘ h ⟩   ≈˘⟨ ⟨⟩∘ ⟩
-        ⟨ f , g ⟩ ∘ h       ∎
-
-      g-fixed-point : f ∘ (g ∘ x) ≈ g ∘ x
-      g-fixed-point = begin
-        f ∘ g ∘ x                       ≈˘⟨  refl⟩∘⟨ g-surjective ⟩
-        f ∘ eval′ ∘ first ϕ ∘ ⟨ x , x ⟩  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ lemma ϕ id x ⟩
-        f ∘ eval′ ∘ ⟨ ϕ , id ⟩ ∘ x       ≈⟨ ∘-resp-≈ʳ sym-assoc ○ sym-assoc ⟩
-        (f ∘ eval′ ∘ ⟨ ϕ , id ⟩) ∘ x     ≡⟨⟩
-        g ∘ x                            ∎
+open import Categories.Category.Finite.Fin.Construction.Discrete
+open import Categories.Functor using (Functor; _∘F_)
+open import Categories.Category.Lift
+
+module Categories.Category.CartesianClosed.Properties {o ℓ e} {𝒞 : Category o ℓ e} (𝓥 : CartesianClosed 𝒞) where
+
+open Category 𝒞
+open CartesianClosed 𝓥 using (_^_; eval′; cartesian)
+open Cartesian cartesian using (products; terminal)
+open BinaryProducts products
+open Terminal terminal using (⊤)
+open HomReasoning
+open MR 𝒞
+
+open CartesianMonoidalClosed 𝒞 𝓥 using (closedMonoidal)
+private
+  module closedMonoidal = Closed closedMonoidal
+
+open import Categories.Object.Initial 𝒞
+open import Categories.Object.StrictInitial 𝒞
+open import Categories.Object.Initial.Colimit 𝒞
+
+
+PointSurjective : ∀ {A X Y : Obj} → (X ⇒ Y ^ A) → Set (ℓ ⊔ e)
+PointSurjective {A = A} {X = X} {Y = Y} ϕ =
+  ∀ (f : A ⇒ Y) → Σ[ x ∈ ⊤ ⇒ X ] (∀ (a : ⊤ ⇒ A) → eval′ ∘ first ϕ ∘ ⟨ x , a ⟩  ≈ f ∘ a)
+
+lawvere-fixed-point : ∀ {A B : Obj} → (ϕ : A ⇒ B ^ A) → PointSurjective ϕ → (f : B ⇒ B) → Σ[ s ∈ ⊤ ⇒ B ] f ∘ s ≈ s
+lawvere-fixed-point {A = A} {B = B} ϕ surjective f = g ∘ x , g-fixed-point
+  where
+    g : A ⇒ B
+    g = f ∘ eval′ ∘ ⟨ ϕ , id ⟩
+
+    x : ⊤ ⇒ A
+    x = proj₁ (surjective  g)
+
+    g-surjective : eval′ ∘ first ϕ ∘ ⟨ x , x ⟩ ≈ g ∘ x
+    g-surjective = proj₂ (surjective g) x
+
+    lemma : ∀ {A B C D} → (f : B ⇒ C) → (g : B ⇒ D) → (h : A ⇒ B) → (f ⁂ g) ∘ ⟨ h , h ⟩ ≈ ⟨ f , g ⟩ ∘ h
+    lemma f g h = begin
+      (f ⁂ g) ∘ ⟨ h , h ⟩ ≈⟨  ⁂∘⟨⟩ ⟩
+      ⟨ f ∘ h , g ∘ h ⟩   ≈˘⟨ ⟨⟩∘ ⟩
+      ⟨ f , g ⟩ ∘ h       ∎
+
+    g-fixed-point : f ∘ (g ∘ x) ≈ g ∘ x
+    g-fixed-point = begin
+      f ∘ g ∘ x                       ≈˘⟨  refl⟩∘⟨ g-surjective ⟩
+      f ∘ eval′ ∘ first ϕ ∘ ⟨ x , x ⟩  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ lemma ϕ id x ⟩
+      f ∘ eval′ ∘ ⟨ ϕ , id ⟩ ∘ x       ≈⟨ ∘-resp-≈ʳ sym-assoc ○ sym-assoc ⟩
+      (f ∘ eval′ ∘ ⟨ ϕ , id ⟩) ∘ x     ≡⟨⟩
+      g ∘ x                            ∎
+
+private
+  empty-diagram : Functor (liftC o ℓ e (Discrete 0)) 𝒞
+  empty-diagram = record
+    { F₀           = λ ()
+    ; F₁           = λ { {()} }
+    ; identity     = λ { {()} }
+    ; homomorphism = λ { {()} }
+    ; F-resp-≈     = λ { {()} }
+    }
+
+initial→product-initial : ∀ {⊥ A} → IsInitial ⊥ → IsInitial (⊥ × A)
+initial→product-initial {⊥} {A} i = initial.⊥-is-initial
+  where colim : Colimit empty-diagram
+        colim = ⊥⇒colimit record { ⊥ = ⊥ ; ⊥-is-initial = i }
+        colim' : Colimit (-× A ∘F empty-diagram)
+        colim' = lapc closedMonoidal.adjoint empty-diagram colim
+        initial : Initial
+        initial = colimit⇒⊥ colim'
+        module initial = Initial initial
+
+open IsStrictInitial using (is-initial; is-strict)
+initial→strict-initial : ∀ {⊥} → IsInitial ⊥ → IsStrictInitial ⊥
+initial→strict-initial i .is-initial = i
+initial→strict-initial {⊥} i .is-strict f = record 
+  { from = f
+  ; to = !
+  ; iso = record
+    { isoˡ = begin
+      ! ∘ f                ≈˘⟨ refl⟩∘⟨ project₁ ⟩
+      ! ∘ π₁ ∘ ⟨ f , id ⟩   ≈⟨ pullˡ (initial-product.!-unique₂ (! ∘ π₁) π₂)  ⟩
+      π₂ ∘ ⟨ f , id ⟩       ≈⟨ project₂ ⟩
+      id                    ∎
+    ; isoʳ = !-unique₂ (f ∘ !) id
+    }
+  }
+  where open IsInitial i
+        module initial-product {A} =
+          IsInitial (initial→product-initial {⊥} {A} i)
+

src/Categories/Object/Initial/Colimit.agda

@@ -0,0 +1,62 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category
+
+open import Categories.Diagram.Limit
+open import Categories.Diagram.Colimit
+open import Categories.Category.Finite.Fin.Construction.Discrete
+open import Categories.Category.Lift
+open import Categories.Functor.Core
+open import Categories.Category.Construction.Cocones
+
+module Categories.Object.Initial.Colimit {o ℓ e} (C : Category o ℓ e) where
+
+open module C = Category C
+
+open import Categories.Object.Initial C
+
+module _ {o′ ℓ′ e′} {F : Functor (liftC o′ ℓ′ e′ (Discrete 0)) C} where
+  colimit⇒⊥ : Colimit F → Initial
+  colimit⇒⊥ L = record
+    { ⊥        = coapex
+    ; ⊥-is-initial = record
+      { !        = rep record
+        { coapex = record
+          { ψ       = λ ()
+          ; commute = λ { {()} }
+          }
+        }
+      ; !-unique = λ f → initial.!-unique record
+        { arr     = f
+        ; commute = λ { {()} }
+        }
+      }
+    }
+    where open Colimit L
+
+module _ {o′ ℓ′ e′} {F : Functor (liftC o′ ℓ′ e′ (Discrete 0)) C} where
+
+  ⊥⇒colimit : Initial → Colimit F
+  ⊥⇒colimit t = record
+    { initial = record
+      { ⊥        = record
+        { N    = ⊥
+        ; coapex = record
+          { ψ       = λ ()
+          ; commute = λ { {()} }
+          }
+        }
+      ; ⊥-is-initial = record
+        { !        = λ {K} →
+          let open Cocone F K
+          in record
+          { arr     = !
+          ; commute = λ { {()} }
+          }
+        ; !-unique = λ f →
+          let module f = Cocone⇒ F f
+          in !-unique f.arr
+        }
+      }
+    }
+    where open Initial t

src/Categories/Object/StrictInitial.agda

@@ -0,0 +1,30 @@
+{-# OPTIONS --without-K --safe #-}
+open import Categories.Category
+open import Level
+
+module Categories.Object.StrictInitial {o ℓ e} (C : Category o ℓ e) where
+
+open Category C
+open import Categories.Morphism C using (Epi; _≅_)
+open import Categories.Object.Initial C
+
+record IsStrictInitial (⊥ : Obj) : Set (o ⊔ ℓ ⊔ e) where
+  field
+    is-initial : IsInitial ⊥
+  open IsInitial is-initial public
+
+  field
+    is-strict : ∀ {A} → A ⇒ ⊥ → A ≅ ⊥
+
+open IsStrictInitial
+
+record StrictInitial  : Set (o ⊔ ℓ ⊔ e) where
+  field
+    ⊥ : Obj
+    is-strict-initial : IsStrictInitial ⊥
+
+  initial : Initial
+  initial .Initial.⊥ = ⊥
+  initial .Initial.⊥-is-initial = is-strict-initial .is-initial
+
+  open Initial initial public

src/Categories/Object/Terminal/Limit.agda

@@ -35,18 +35,8 @@ module _ {o′ ℓ′ e′} {F : Functor (liftC o′ ℓ′ e′ (Discrete 0)) C
     }
     where open Limit L
 
-module _ o′ ℓ′ e′ where
-
-  ⊤⇒limit-F : Functor (liftC o′ ℓ′ e′ (Discrete 0)) C
-  ⊤⇒limit-F = record
-    { F₀           = λ ()
-    ; F₁           = λ { {()} }
-    ; identity     = λ { {()} }
-    ; homomorphism = λ { {()} }
-    ; F-resp-≈     = λ { {()} }
-    }
-
-  ⊤⇒limit : Terminal → Limit ⊤⇒limit-F
+module _ {o′ ℓ′ e′} {F : Functor (liftC o′ ℓ′ e′ (Discrete 0)) C} where
+  ⊤⇒limit : Terminal → Limit F
   ⊤⇒limit t = record
     { terminal = record
       { ⊤        = record
@@ -58,13 +48,13 @@ module _ o′ ℓ′ e′ where
         }
       ; ⊤-is-terminal = record
         { !        = λ {K} →
-          let open Co.Cone ⊤⇒limit-F K
+          let open Co.Cone F K
           in record
           { arr     = !
           ; commute = λ { {()} }
           }
         ; !-unique = λ f →
-          let module f = Co.Cone⇒ ⊤⇒limit-F f
+          let module f = Co.Cone⇒ F f
           in !-unique f.arr
         }
       }