From 319c9f47c25debfba939e5afa78004c02e8e558c Mon Sep 17 00:00:00 2001 From: Calvin Lee Date: Sun, 26 May 2024 13:24:36 +0000 Subject: [PATCH] initial objects in a CCC are strict --- .../Category/CartesianClosed/Properties.agda | 136 ++++++++++++------ src/Categories/Object/Initial/Colimit.agda | 62 ++++++++ src/Categories/Object/StrictInitial.agda | 30 ++++ src/Categories/Object/Terminal/Limit.agda | 18 +-- 4 files changed, 192 insertions(+), 54 deletions(-) create mode 100644 src/Categories/Object/Initial/Colimit.agda create mode 100644 src/Categories/Object/StrictInitial.agda diff --git a/src/Categories/Category/CartesianClosed/Properties.agda b/src/Categories/Category/CartesianClosed/Properties.agda index 30ed46d8c..d9dfcc055 100644 --- a/src/Categories/Category/CartesianClosed/Properties.agda +++ b/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) + diff --git a/src/Categories/Object/Initial/Colimit.agda b/src/Categories/Object/Initial/Colimit.agda new file mode 100644 index 000000000..27705652c --- /dev/null +++ b/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 diff --git a/src/Categories/Object/StrictInitial.agda b/src/Categories/Object/StrictInitial.agda new file mode 100644 index 000000000..3e5ca3514 --- /dev/null +++ b/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 diff --git a/src/Categories/Object/Terminal/Limit.agda b/src/Categories/Object/Terminal/Limit.agda index e8f91e08d..668c2982f 100644 --- a/src/Categories/Object/Terminal/Limit.agda +++ b/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 } }