diff options
Diffstat (limited to 'Category/Cartesian/Instance')
| -rw-r--r-- | Category/Cartesian/Instance/FinitelyCocompletes.agda | 51 |
1 files changed, 46 insertions, 5 deletions
diff --git a/Category/Cartesian/Instance/FinitelyCocompletes.agda b/Category/Cartesian/Instance/FinitelyCocompletes.agda index 5425233..8c779d5 100644 --- a/Category/Cartesian/Instance/FinitelyCocompletes.agda +++ b/Category/Cartesian/Instance/FinitelyCocompletes.agda @@ -16,8 +16,8 @@ open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; ni open import Categories.NaturalTransformation.NaturalIsomorphism.Properties using (pointwise-iso) open import Categories.Object.Coproduct using (IsCoproduct; IsCoproduct⇒Coproduct; Coproduct) open import Categories.Object.Initial using (IsInitial) -open import Data.Product.Base using (_,_) renaming (_×_ to _×′_) - +open import Data.Product using (_,_; swap) renaming (_×_ to _×′_) +open import Function using () renaming (_∘_ to _∘′_) open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) open import Category.Instance.FinitelyCocompletes {o} {ℓ} {e} using (FinitelyCocompletes; FinitelyCocompletes-Cartesian; _×₁_) open import Functor.Exact using (IsRightExact; RightExactFunctor) @@ -44,13 +44,48 @@ module _ (𝒞 : FinitelyCocompleteCategory o ℓ e) where private module -+- = Functor -+- + flip-IsInitial + : {(A , B) : 𝒞×𝒞.Obj} + → IsInitial 𝒞×𝒞.U (A , B) + → IsInitial 𝒞×𝒞.U (B , A) + flip-IsInitial isInitial = let open IsInitial isInitial in record + { ! = swap ! + ; !-unique = swap ∘′ !-unique ∘′ swap + } + + flip-IsCoproduct + : {(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₂-₁) + flip-IsCoproduct isCoproduct = let module + = IsCoproduct isCoproduct in record + { [_,_] = λ x y → swap (+.[ swap x , swap y ]) + ; inject₁ = swap +.inject₁ + ; inject₂ = swap +.inject₂ + ; unique = λ x y → swap (+.unique (swap x) (swap y)) + } + + flip-IsCoequalizer + : {(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₁) + flip-IsCoequalizer isCoeq = let open IsCoequalizer isCoeq in record + { equality = swap equality + ; coequalize = swap ∘′ coequalize ∘′ swap + ; universal = swap universal + ; unique = swap ∘′ unique ∘′ swap + } + +-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₂))) } + ; !-unique = λ f → +-unique (sym (A-isInitial.!-unique (f ∘ i₁))) (sym (B-isInitial.!-unique (f ∘ i₂))) } where open IsRightExact @@ -209,7 +244,14 @@ module _ {𝒞 : FinitelyCocompleteCategory o ℓ e} where module x+y = RightExactFunctor -+- ↔-+- : 𝒞 × 𝒞 ⇒ 𝒞 - ↔-+- = -+- ∘ Swap 𝒞 𝒞 + ↔-+- = record + { F = flip-bifunctor 𝒞.-+- + ; isRightExact = record + { F-resp-⊥ = λ x → +-resp-⊥ 𝒞 (flip-IsInitial 𝒞 x) + ; F-resp-+ = λ x → +-resp-+ 𝒞 (flip-IsCoproduct 𝒞 x) + ; F-resp-coeq = λ x → (+-resp-coeq 𝒞 (flip-IsCoequalizer 𝒞 x)) + } + } module y+x = RightExactFunctor ↔-+- [x+y]+z : (𝒞 × 𝒞) × 𝒞 ⇒ 𝒞 @@ -227,7 +269,6 @@ module _ {𝒞 : FinitelyCocompleteCategory o ℓ e} where module 𝒞×𝒞×𝒞 = FinitelyCocompleteCategory ((𝒞 × 𝒞) × 𝒞) open Morphism U using (_≅_; module ≅) module +-assoc {X} {Y} {Z} = _≅_ (≅.sym (+-assoc {X} {Y} {Z})) - open import Categories.Category.BinaryProducts using (BinaryProducts) open import Categories.Object.Duality 𝒞.U using (Coproduct⇒coProduct) op-binaryProducts : BinaryProducts op op-binaryProducts = record { product = Coproduct⇒coProduct coproduct } |