diff options
Diffstat (limited to 'Category/Instance/Properties/FinitelyCocompletes.agda')
| -rw-r--r-- | Category/Instance/Properties/FinitelyCocompletes.agda | 210 |
1 files changed, 0 insertions, 210 deletions
diff --git a/Category/Instance/Properties/FinitelyCocompletes.agda b/Category/Instance/Properties/FinitelyCocompletes.agda deleted file mode 100644 index dedfa16..0000000 --- a/Category/Instance/Properties/FinitelyCocompletes.agda +++ /dev/null @@ -1,210 +0,0 @@ -{-# OPTIONS --without-K --safe #-} - -open import Level using (Level) -module Category.Instance.Properties.FinitelyCocompletes {o ℓ e : Level} where - -import Categories.Morphism.Reasoning as ⇒-Reasoning - -open import Categories.Category.BinaryProducts using (BinaryProducts) -open import Categories.Category.Cartesian.Bundle using (CartesianCategory) -open import Categories.Category.Product using (Product) renaming (_⁂_ to _⁂′_) -open import Categories.Diagram.Coequalizer using (IsCoequalizer) -open import Categories.Functor.Core using (Functor) -open import Categories.Functor using (_∘F_) renaming (id to idF) -open import Categories.Object.Coproduct using (IsCoproduct; IsCoproduct⇒Coproduct; Coproduct) -open import Categories.Object.Initial using (IsInitial) -open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) -open import Category.Instance.FinitelyCocompletes {o} {ℓ} {e} using (FinitelyCocompletes; FinitelyCocompletes-Cartesian; _×₁_) -open import Data.Product.Base using (_,_) renaming (_×_ to _×′_) -open import Functor.Exact using (IsRightExact; RightExactFunctor) -open import Level using (_⊔_; suc) - -FinitelyCocompletes-CC : CartesianCategory (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) -FinitelyCocompletes-CC = record - { U = FinitelyCocompletes - ; cartesian = FinitelyCocompletes-Cartesian - } - -module FinCoCom = CartesianCategory FinitelyCocompletes-CC -open BinaryProducts (FinCoCom.products) using (_×_; π₁; π₂; _⁂_; assocˡ) -- hiding (unique) - -module _ (𝒞 : FinitelyCocompleteCategory o ℓ e) where - - private - module 𝒞 = FinitelyCocompleteCategory 𝒞 - module 𝒞×𝒞 = FinitelyCocompleteCategory (𝒞 × 𝒞) - - open 𝒞 using ([_,_]; +-unique; i₁; i₂; _∘_; _+_; module Equiv; _⇒_; _+₁_; -+-) - open Equiv - - private - module -+- = Functor -+- - - +-resp-⊥ - : {(A , B) : 𝒞×𝒞.Obj} - → IsInitial 𝒞×𝒞.U (A , B) - → IsInitial 𝒞.U (A + B) - +-resp-⊥ {A , B} A,B-isInitial = record - { ! = [ A-isInitial.! , B-isInitial.! ] - ; !-unique = λ { f → +-unique (sym (A-isInitial.!-unique (f ∘ i₁))) (sym (B-isInitial.!-unique (f ∘ i₂))) } - } - where - open IsRightExact - open RightExactFunctor - module A-isInitial = IsInitial (F-resp-⊥ (isRightExact (π₁ {𝒞} {𝒞})) A,B-isInitial) - module B-isInitial = IsInitial (F-resp-⊥ (isRightExact (π₂ {𝒞} {𝒞})) A,B-isInitial) - - +-resp-+ - : {(A₁ , A₂) (B₁ , B₂) (C₁ , C₂) : 𝒞×𝒞.Obj} - {(i₁-₁ , i₁-₂) : (A₁ ⇒ C₁) ×′ (A₂ ⇒ C₂)} - {(i₂-₁ , i₂-₂) : (B₁ ⇒ C₁) ×′ (B₂ ⇒ C₂)} - → IsCoproduct 𝒞×𝒞.U (i₁-₁ , i₁-₂) (i₂-₁ , i₂-₂) - → IsCoproduct 𝒞.U (i₁-₁ +₁ i₁-₂) (i₂-₁ +₁ i₂-₂) - +-resp-+ {A₁ , A₂} {B₁ , B₂} {C₁ , C₂} {i₁-₁ , i₁-₂} {i₂-₁ , i₂-₂} isCoproduct = record - { [_,_] = λ { h₁ h₂ → [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] } - ; inject₁ = inject₁ - ; inject₂ = inject₂ - ; unique = unique - } - where - open IsRightExact - open RightExactFunctor - module Coprod₁ = Coproduct (IsCoproduct⇒Coproduct 𝒞.U (F-resp-+ (isRightExact (π₁ {𝒞} {𝒞})) isCoproduct)) - module Coprod₂ = Coproduct (IsCoproduct⇒Coproduct 𝒞.U (F-resp-+ (isRightExact (π₂ {𝒞} {𝒞})) isCoproduct)) - open 𝒞 using ([]-cong₂; []∘+₁; +-g-η; +₁∘i₁; +₁∘i₂) - open 𝒞 using (Obj; _≈_; module HomReasoning; assoc) - open HomReasoning - open ⇒-Reasoning 𝒞.U - inject₁ - : {X : Obj} - {h₁ : A₁ + A₂ ⇒ X} - {h₂ : B₁ + B₂ ⇒ X} - → [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ∘ (i₁-₁ +₁ i₁-₂) ≈ h₁ - inject₁ {_} {h₁} {h₂} = begin - [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ∘ (i₁-₁ +₁ i₁-₂) ≈⟨ []∘+₁ ⟩ - [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] ∘ i₁-₁ , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ∘ i₁-₂ ] ≈⟨ []-cong₂ Coprod₁.inject₁ Coprod₂.inject₁ ⟩ - [ h₁ ∘ i₁ , h₁ ∘ i₂ ] ≈⟨ +-g-η ⟩ - h₁ ∎ - inject₂ - : {X : Obj} - {h₁ : A₁ + A₂ ⇒ X} - {h₂ : B₁ + B₂ ⇒ X} - → [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ∘ (i₂-₁ +₁ i₂-₂) ≈ h₂ - inject₂ {_} {h₁} {h₂} = begin - [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ∘ (i₂-₁ +₁ i₂-₂) ≈⟨ []∘+₁ ⟩ - [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] ∘ i₂-₁ , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ∘ i₂-₂ ] ≈⟨ []-cong₂ Coprod₁.inject₂ Coprod₂.inject₂ ⟩ - [ h₂ ∘ i₁ , h₂ ∘ i₂ ] ≈⟨ +-g-η ⟩ - h₂ ∎ - unique - : {X : Obj} - {i : C₁ + C₂ ⇒ X} - {h₁ : A₁ + A₂ ⇒ X} - {h₂ : B₁ + B₂ ⇒ X} - (eq₁ : i ∘ (i₁-₁ +₁ i₁-₂) ≈ h₁) - (eq₂ : i ∘ (i₂-₁ +₁ i₂-₂) ≈ h₂) - → [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ≈ i - unique {X} {i} {h₁} {h₂} eq₁ eq₂ = begin - [ Coprod₁.[ h₁ ∘ i₁ , h₂ ∘ i₁ ] , Coprod₂.[ h₁ ∘ i₂ , h₂ ∘ i₂ ] ] ≈⟨ []-cong₂ (Coprod₁.unique eq₁-₁ eq₂-₁) (Coprod₂.unique eq₁-₂ eq₂-₂) ⟩ - [ i ∘ i₁ , i ∘ i₂ ] ≈⟨ +-g-η ⟩ - i ∎ - where - eq₁-₁ : (i ∘ i₁) ∘ i₁-₁ ≈ h₁ ∘ i₁ - eq₁-₁ = begin - (i ∘ i₁) ∘ i₁-₁ ≈⟨ pushʳ +₁∘i₁ ⟨ - i ∘ (i₁-₁ +₁ i₁-₂) ∘ i₁ ≈⟨ pullˡ eq₁ ⟩ - h₁ ∘ i₁ ∎ - eq₂-₁ : (i ∘ i₁) ∘ i₂-₁ ≈ h₂ ∘ i₁ - eq₂-₁ = begin - (i ∘ i₁) ∘ i₂-₁ ≈⟨ pushʳ +₁∘i₁ ⟨ - i ∘ (i₂-₁ +₁ i₂-₂) ∘ i₁ ≈⟨ pullˡ eq₂ ⟩ - h₂ ∘ i₁ ∎ - eq₁-₂ : (i ∘ i₂) ∘ i₁-₂ ≈ h₁ ∘ i₂ - eq₁-₂ = begin - (i ∘ i₂) ∘ i₁-₂ ≈⟨ pushʳ +₁∘i₂ ⟨ - i ∘ (i₁-₁ +₁ i₁-₂) ∘ i₂ ≈⟨ pullˡ eq₁ ⟩ - h₁ ∘ i₂ ∎ - eq₂-₂ : (i ∘ i₂) ∘ i₂-₂ ≈ h₂ ∘ i₂ - eq₂-₂ = begin - (i ∘ i₂) ∘ i₂-₂ ≈⟨ pushʳ +₁∘i₂ ⟨ - i ∘ (i₂-₁ +₁ i₂-₂) ∘ i₂ ≈⟨ pullˡ eq₂ ⟩ - h₂ ∘ i₂ ∎ - - +-resp-coeq - : {(A₁ , A₂) (B₁ , B₂) (C₁ , C₂) : 𝒞×𝒞.Obj} - {(f₁ , f₂) (g₁ , g₂) : (A₁ ⇒ B₁) ×′ (A₂ ⇒ B₂)} - {(h₁ , h₂) : (B₁ ⇒ C₁) ×′ (B₂ ⇒ C₂)} - → IsCoequalizer 𝒞×𝒞.U (f₁ , f₂) (g₁ , g₂) (h₁ , h₂) - → IsCoequalizer 𝒞.U (f₁ +₁ f₂) (g₁ +₁ g₂) (h₁ +₁ h₂) - +-resp-coeq {A₁ , A₂} {B₁ , B₂} {C₁ , C₂} {f₁ , f₂} {g₁ , g₂} {h₁ , h₂} isCoeq = record - { equality = sym -+-.homomorphism ○ []-cong₂ (refl⟩∘⟨ Coeq₁.equality) (refl⟩∘⟨ Coeq₂.equality) ○ -+-.homomorphism - ; coequalize = coequalize - ; universal = universal _ - ; unique = uniq _ - } - where - open IsRightExact - open RightExactFunctor - module Coeq₁ = IsCoequalizer (F-resp-coeq (isRightExact (π₁ {𝒞} {𝒞})) isCoeq) - module Coeq₂ = IsCoequalizer (F-resp-coeq (isRightExact (π₂ {𝒞} {𝒞})) isCoeq) - open 𝒞 using ([]-cong₂; +₁∘i₁; +₁∘i₂; []∘+₁; +-g-η) - open 𝒞 using (Obj; _≈_; module HomReasoning; assoc; sym-assoc) - open 𝒞.HomReasoning - open ⇒-Reasoning 𝒞.U - - module _ {X : Obj} {k : B₁ + B₂ ⇒ X} (eq : k ∘ (f₁ +₁ f₂) ≈ k ∘ (g₁ +₁ g₂)) where - - eq₁ : (k ∘ i₁) ∘ f₁ ≈ (k ∘ i₁) ∘ g₁ - eq₁ = begin - (k ∘ i₁) ∘ f₁ ≈⟨ pushʳ +₁∘i₁ ⟨ - k ∘ (f₁ +₁ f₂) ∘ i₁ ≈⟨ extendʳ eq ⟩ - k ∘ (g₁ +₁ g₂) ∘ i₁ ≈⟨ pushʳ +₁∘i₁ ⟩ - (k ∘ i₁) ∘ g₁ ∎ - - eq₂ : (k ∘ i₂) ∘ f₂ ≈ (k ∘ i₂) ∘ g₂ - eq₂ = begin - (k ∘ i₂) ∘ f₂ ≈⟨ pushʳ +₁∘i₂ ⟨ - k ∘ (f₁ +₁ f₂) ∘ i₂ ≈⟨ extendʳ eq ⟩ - k ∘ (g₁ +₁ g₂) ∘ i₂ ≈⟨ pushʳ +₁∘i₂ ⟩ - (k ∘ i₂) ∘ g₂ ∎ - - coequalize : C₁ + C₂ ⇒ X - coequalize = [ Coeq₁.coequalize eq₁ , Coeq₂.coequalize eq₂ ] - - universal : k ≈ coequalize ∘ (h₁ +₁ h₂) - universal = begin - k ≈⟨ +-g-η ⟨ - [ k ∘ i₁ , k ∘ i₂ ] ≈⟨ []-cong₂ Coeq₁.universal Coeq₂.universal ⟩ - [ Coeq₁.coequalize eq₁ ∘ h₁ , Coeq₂.coequalize eq₂ ∘ h₂ ] ≈⟨ []∘+₁ ⟨ - coequalize ∘ (h₁ +₁ h₂) ∎ - - uniq : {i : C₁ + C₂ ⇒ X} → k ≈ i ∘ (h₁ +₁ h₂) → i ≈ coequalize - uniq {i} eq′ = begin - i ≈⟨ +-g-η ⟨ - [ i ∘ i₁ , i ∘ i₂ ] ≈⟨ []-cong₂ (Coeq₁.unique eq₁′) (Coeq₂.unique eq₂′) ⟩ - [ Coeq₁.coequalize eq₁ , Coeq₂.coequalize eq₂ ] ∎ - where - eq₁′ : k ∘ i₁ ≈ (i ∘ i₁) ∘ h₁ - eq₁′ = eq′ ⟩∘⟨refl ○ extendˡ +₁∘i₁ - eq₂′ : k ∘ i₂ ≈ (i ∘ i₂) ∘ h₂ - eq₂′ = eq′ ⟩∘⟨refl ○ extendˡ +₁∘i₂ - -module _ {𝒞 : FinitelyCocompleteCategory o ℓ e} where - - open FinCoCom using (_⇒_; _∘_; id) - module 𝒞 = FinitelyCocompleteCategory 𝒞 - - -+- : 𝒞 × 𝒞 ⇒ 𝒞 - -+- = record - { F = 𝒞.-+- - ; isRightExact = record - { F-resp-⊥ = +-resp-⊥ 𝒞 - ; F-resp-+ = +-resp-+ 𝒞 - ; F-resp-coeq = +-resp-coeq 𝒞 - } - } - - [x+y]+z : (𝒞 × 𝒞) × 𝒞 ⇒ 𝒞 - [x+y]+z = -+- ∘ (-+- ×₁ id) - - x+[y+z] : (𝒞 × 𝒞) × 𝒞 ⇒ 𝒞 - x+[y+z] = -+- ∘ (id ×₁ -+-) ∘ assocˡ |