aboutsummaryrefslogtreecommitdiff
path: root/Category
diff options
context:
space:
mode:
Diffstat (limited to 'Category')
-rw-r--r--Category/Diagram/Cospan.agda117
-rw-r--r--Category/Instance/Cospans.agda87
-rw-r--r--Category/Instance/DecoratedCospans.agda17
-rw-r--r--Category/Instance/FinitelyCocompletes.agda19
4 files changed, 137 insertions, 103 deletions
diff --git a/Category/Diagram/Cospan.agda b/Category/Diagram/Cospan.agda
new file mode 100644
index 0000000..b988651
--- /dev/null
+++ b/Category/Diagram/Cospan.agda
@@ -0,0 +1,117 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
+open import Level using (Level; _⊔_)
+
+module Category.Diagram.Cospan {o ℓ e : Level} (𝒞 : FinitelyCocompleteCategory o ℓ e) where
+
+import Categories.Morphism as Morphism
+import Categories.Morphism.Reasoning as ⇒-Reasoning
+
+open import Relation.Binary using (IsEquivalence)
+
+module 𝒞 = FinitelyCocompleteCategory 𝒞
+
+open 𝒞 hiding (i₁; i₂; _≈_)
+open ⇒-Reasoning U using (switch-fromtoˡ; glueTrianglesˡ)
+open Morphism U using (_≅_; module ≅)
+
+record Cospan (A B : Obj) : Set (o ⊔ ℓ) where
+
+ constructor cospan
+
+ field
+ {N} : Obj
+ f₁ : A ⇒ N
+ f₂ : B ⇒ N
+
+private
+ variable
+ A B C D : Obj
+
+record _≈_ (C D : Cospan A B) : Set (ℓ ⊔ e) where
+
+ module C = Cospan C
+ module D = Cospan D
+
+ field
+ ≅N : C.N ≅ D.N
+
+ open _≅_ ≅N public
+ module ≅N = _≅_ ≅N
+
+ field
+ from∘f₁≈f₁ : from ∘ C.f₁ 𝒞.≈ D.f₁
+ from∘f₂≈f₂ : from ∘ C.f₂ 𝒞.≈ D.f₂
+
+infix 4 _≈_
+
+private
+ variable
+ f g h : Cospan A B
+
+≈-refl : f ≈ f
+≈-refl {f = cospan f₁ f₂} = record
+ { ≅N = ≅.refl
+ ; from∘f₁≈f₁ = from∘f₁≈f₁
+ ; from∘f₂≈f₂ = from∘f₂≈f₂
+ }
+ where abstract
+ from∘f₁≈f₁ : id ∘ f₁ 𝒞.≈ f₁
+ from∘f₁≈f₁ = identityˡ
+ from∘f₂≈f₂ : id ∘ f₂ 𝒞.≈ f₂
+ from∘f₂≈f₂ = identityˡ
+
+≈-sym : f ≈ g → g ≈ f
+≈-sym f≈g = record
+ { ≅N = ≅.sym ≅N
+ ; from∘f₁≈f₁ = a
+ ; from∘f₂≈f₂ = b
+ }
+ where abstract
+ open _≈_ f≈g
+ a : ≅N.to ∘ D.f₁ 𝒞.≈ C.f₁
+ a = Equiv.sym (switch-fromtoˡ ≅N from∘f₁≈f₁)
+ b : ≅N.to ∘ D.f₂ 𝒞.≈ C.f₂
+ b = Equiv.sym (switch-fromtoˡ ≅N from∘f₂≈f₂)
+
+≈-trans : f ≈ g → g ≈ h → f ≈ h
+≈-trans f≈g g≈h = record
+ { ≅N = ≅.trans f≈g.≅N g≈h.≅N
+ ; from∘f₁≈f₁ = a
+ ; from∘f₂≈f₂ = b
+ }
+ where abstract
+ module f≈g = _≈_ f≈g
+ module g≈h = _≈_ g≈h
+ a : (g≈h.≅N.from ∘ f≈g.≅N.from) ∘ f≈g.C.f₁ 𝒞.≈ g≈h.D.f₁
+ a = glueTrianglesˡ g≈h.from∘f₁≈f₁ f≈g.from∘f₁≈f₁
+ b : (g≈h.≅N.from ∘ f≈g.≅N.from) ∘ f≈g.C.f₂ 𝒞.≈ g≈h.D.f₂
+ b = glueTrianglesˡ g≈h.from∘f₂≈f₂ f≈g.from∘f₂≈f₂
+
+≈-equiv : {A B : 𝒞.Obj} → IsEquivalence (_≈_ {A} {B})
+≈-equiv = record
+ { refl = ≈-refl
+ ; sym = ≈-sym
+ ; trans = ≈-trans
+ }
+
+compose : Cospan A B → Cospan B C → Cospan A C
+compose (cospan f g) (cospan h i) = cospan (i₁ ∘ f) (i₂ ∘ i)
+ where
+ open pushout g h
+
+identity : Cospan A A
+identity = cospan id id
+
+compose-3 : Cospan A B → Cospan B C → Cospan C D → Cospan A D
+compose-3 (cospan f₁ f₂) (cospan g₁ g₂) (cospan h₁ h₂) = cospan (P₃.i₁ ∘ P₁.i₁ ∘ f₁) (P₃.i₂ ∘ P₂.i₂ ∘ h₂)
+ where
+ module P₁ = pushout f₂ g₁
+ module P₂ = pushout g₂ h₁
+ module P₃ = pushout P₁.i₂ P₂.i₁
+
+_⊗_ : Cospan A B → Cospan C D → Cospan (A + C) (B + D)
+_⊗_ (cospan f₁ f₂) (cospan g₁ g₂) = cospan (f₁ +₁ g₁) (f₂ +₁ g₂)
+
+infixr 10 _⊗_
diff --git a/Category/Instance/Cospans.agda b/Category/Instance/Cospans.agda
index ae6d359..d17a58d 100644
--- a/Category/Instance/Cospans.agda
+++ b/Category/Instance/Cospans.agda
@@ -13,12 +13,10 @@ open Category U hiding (_≈_)
open import Categories.Diagram.Pushout U using (Pushout)
open import Categories.Diagram.Pushout.Properties U using (pushout-resp-≈; up-to-iso)
-open import Relation.Binary using (IsEquivalence)
open import Categories.Morphism U using (_≅_; module ≅)
open import Categories.Morphism.Reasoning U
using
( switch-fromtoˡ
- ; glueTrianglesˡ
; pullˡ ; pullʳ
; cancelˡ
)
@@ -30,99 +28,16 @@ open import Category.Diagram.Pushout U 
; extend-i₁-iso ; extend-i₂-iso
)
-record Cospan (A B : Obj) : Set (o ⊔ ℓ) where
-
- constructor cospan
-
- field
- {N} : Obj
- f₁ : A ⇒ N
- f₂ : B ⇒ N
+open import Category.Diagram.Cospan 𝒞 using (Cospan; compose; compose-3; identity; _≈_; cospan; ≈-trans; ≈-sym; ≈-equiv)
private
variable
A B C D : Obj
-compose : Cospan A B → Cospan B C → Cospan A C
-compose (cospan f g) (cospan h i) = cospan (i₁ ∘ f) (i₂ ∘ i)
- where
- open pushout g h
-
-identity : Cospan A A
-identity = cospan id id
-
-compose-3 : Cospan A B → Cospan B C → Cospan C D → Cospan A D
-compose-3 (cospan f₁ f₂) (cospan g₁ g₂) (cospan h₁ h₂) = cospan (P₃.i₁ ∘ P₁.i₁ ∘ f₁) (P₃.i₂ ∘ P₂.i₂ ∘ h₂)
- where
- module P₁ = pushout f₂ g₁
- module P₂ = pushout g₂ h₁
- module P₃ = pushout P₁.i₂ P₂.i₁
-
-record _≈_ (C D : Cospan A B) : Set (ℓ ⊔ e) where
-
- module C = Cospan C
- module D = Cospan D
-
- field
- ≅N : C.N ≅ D.N
-
- open _≅_ ≅N public
- module ≅N = _≅_ ≅N
-
- field
- from∘f₁≈f₁ : from ∘ C.f₁ 𝒞.≈ D.f₁
- from∘f₂≈f₂ : from ∘ C.f₂ 𝒞.≈ D.f₂
-
private
variable
f g h : Cospan A B
-≈-refl : f ≈ f
-≈-refl {f = cospan f₁ f₂} = record
- { ≅N = ≅.refl
- ; from∘f₁≈f₁ = from∘f₁≈f₁
- ; from∘f₂≈f₂ = from∘f₂≈f₂
- }
- where abstract
- from∘f₁≈f₁ : id ∘ f₁ 𝒞.≈ f₁
- from∘f₁≈f₁ = identityˡ
- from∘f₂≈f₂ : id ∘ f₂ 𝒞.≈ f₂
- from∘f₂≈f₂ = identityˡ
-
-≈-sym : f ≈ g → g ≈ f
-≈-sym f≈g = record
- { ≅N = ≅.sym ≅N
- ; from∘f₁≈f₁ = a
- ; from∘f₂≈f₂ = b
- }
- where abstract
- open _≈_ f≈g
- a : ≅N.to ∘ D.f₁ 𝒞.≈ C.f₁
- a = Equiv.sym (switch-fromtoˡ ≅N from∘f₁≈f₁)
- b : ≅N.to ∘ D.f₂ 𝒞.≈ C.f₂
- b = Equiv.sym (switch-fromtoˡ ≅N from∘f₂≈f₂)
-
-≈-trans : f ≈ g → g ≈ h → f ≈ h
-≈-trans f≈g g≈h = record
- { ≅N = ≅.trans f≈g.≅N g≈h.≅N
- ; from∘f₁≈f₁ = a
- ; from∘f₂≈f₂ = b
- }
- where abstract
- module f≈g = _≈_ f≈g
- module g≈h = _≈_ g≈h
- a : (g≈h.≅N.from ∘ f≈g.≅N.from) ∘ f≈g.C.f₁ 𝒞.≈ g≈h.D.f₁
- a = glueTrianglesˡ g≈h.from∘f₁≈f₁ f≈g.from∘f₁≈f₁
- b : (g≈h.≅N.from ∘ f≈g.≅N.from) ∘ f≈g.C.f₂ 𝒞.≈ g≈h.D.f₂
- b = glueTrianglesˡ g≈h.from∘f₂≈f₂ f≈g.from∘f₂≈f₂
-
-≈-equiv : {A B : 𝒞.Obj} → IsEquivalence (_≈_ {A} {B})
-≈-equiv = record
- { refl = ≈-refl
- ; sym = ≈-sym
- ; trans = ≈-trans
- }
-
compose-idˡ : compose f identity ≈ f
compose-idˡ {f = cospan {N} f₁ f₂} = record
{ ≅N = ≅P
diff --git a/Category/Instance/DecoratedCospans.agda b/Category/Instance/DecoratedCospans.agda
index 7e63f81..b527265 100644
--- a/Category/Instance/DecoratedCospans.agda
+++ b/Category/Instance/DecoratedCospans.agda
@@ -20,6 +20,7 @@ module 𝒟 = SymmetricMonoidalCategory 𝒟
import Categories.Category.Monoidal.Utilities as ⊗-Util
import Category.Instance.Cospans 𝒞 as Cospans
+import Category.Diagram.Cospan 𝒞 as Cospan
open import Categories.Category using (Category; _[_∘_])
open import Categories.Category.Cocartesian using (module CocartesianMonoidal)
@@ -52,7 +53,7 @@ private
compose : DecoratedCospan A B → DecoratedCospan B C → DecoratedCospan A C
compose c₁ c₂ = record
- { cospan = Cospans.compose C₁.cospan C₂.cospan
+ { cospan = Cospan.compose C₁.cospan C₂.cospan
; decoration = F₁ [ i₁ , i₂ ] ∘ φ ∘ s⊗t
}
where
@@ -69,7 +70,7 @@ compose c₁ c₂ = record
identity : DecoratedCospan A A
identity = record
- { cospan = Cospans.identity
+ { cospan = Cospan.identity
; decoration = 𝒟.U [ F₁ 𝒞.initial.! ∘ ε ]
}
@@ -80,9 +81,9 @@ record _≈_ (C₁ C₂ : DecoratedCospan A B) : Set (ℓ ⊔ e ⊔ e′) where
module C₂ = DecoratedCospan C₂
field
- cospans-≈ : C₁.cospan Cospans.≈ C₂.cospan
+ cospans-≈ : C₁.cospan Cospan.≈ C₂.cospan
- open Cospans._≈_ cospans-≈ public
+ open Cospan._≈_ cospans-≈ public
open Morphism 𝒟.U using (_≅_)
field
@@ -107,13 +108,13 @@ module _ where
≈-refl : f ≈ f
≈-refl = record
- { cospans-≈ = Cospans.≈-refl
+ { cospans-≈ = Cospan.≈-refl
; same-deco = F-identity ⟩∘⟨refl ○ identityˡ
}
≈-sym : f ≈ g → g ≈ f
≈-sym f≈g = record
- { cospans-≈ = Cospans.≈-sym cospans-≈
+ { cospans-≈ = Cospan.≈-sym cospans-≈
; same-deco = sym (switch-fromtoˡ 𝒟.U ≅F[N] same-deco)
}
where
@@ -121,7 +122,7 @@ module _ where
≈-trans : f ≈ g → g ≈ h → f ≈ h
≈-trans f≈g g≈h = record
- { cospans-≈ = Cospans.≈-trans f≈g.cospans-≈ g≈h.cospans-≈
+ { cospans-≈ = Cospan.≈-trans f≈g.cospans-≈ g≈h.cospans-≈
; same-deco =
homomorphism ⟩∘⟨refl ○
glueTrianglesˡ 𝒟.U g≈h.same-deco f≈g.same-deco
@@ -613,7 +614,7 @@ compose-equiv {_} {_} {_} {c₂} {c₂′} {c₁} {c₁′} ≅C₂ ≅C₁ = re
module C₂ = DecoratedCospan c₂
module C₂′ = DecoratedCospan c₂′
≅C₂∘C₁ = Cospans.compose-equiv ≅C₂.cospans-≈ ≅C₁.cospans-≈
- module ≅C₂∘C₁ = Cospans._≈_ ≅C₂∘C₁
+ module ≅C₂∘C₁ = Cospan._≈_ ≅C₂∘C₁
P = 𝒞.pushout C₁.f₂ C₂.f₁
P′ = 𝒞.pushout C₁′.f₂ C₂′.f₁
module P = Pushout P
diff --git a/Category/Instance/FinitelyCocompletes.agda b/Category/Instance/FinitelyCocompletes.agda
index 2766df2..9bee58e 100644
--- a/Category/Instance/FinitelyCocompletes.agda
+++ b/Category/Instance/FinitelyCocompletes.agda
@@ -1,29 +1,31 @@
{-# OPTIONS --without-K --safe #-}
-open import Level using (Level)
+
+open import Level using (Level; suc; _⊔_)
+
module Category.Instance.FinitelyCocompletes {o ℓ e : Level} where
+import Category.Instance.One.Properties as OneProps
+
open import Categories.Category using (_[_,_])
open import Categories.Category.BinaryProducts using (BinaryProducts)
open import Categories.Category.Cartesian using (Cartesian)
-open import Categories.Category.Helper using (categoryHelper)
-open import Categories.Category.Monoidal.Instance.Cats using () renaming (module Product to Products)
open import Categories.Category.Core using (Category)
+open import Categories.Category.Helper using (categoryHelper)
open import Categories.Category.Instance.Cats using (Cats)
open import Categories.Category.Instance.One using (One; One-⊤)
+open import Categories.Category.Monoidal.Instance.Cats using () renaming (module Product to Products)
open import Categories.Category.Product using (πˡ; πʳ; _※_; _⁂_) renaming (Product to ProductCat)
open import Categories.Diagram.Coequalizer using (IsCoequalizer)
open import Categories.Functor using (Functor) renaming (id to idF)
+open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; associator; unitorˡ; unitorʳ; module ≃; _ⓘₕ_)
open import Categories.Object.Coproduct using (IsCoproduct)
open import Categories.Object.Initial using (IsInitial)
open import Categories.Object.Product.Core using (Product)
-open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; associator; unitorˡ; unitorʳ; module ≃; _ⓘₕ_)
open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
open import Category.Cocomplete.Finitely.Product using (FinitelyCocomplete-×)
-open import Category.Instance.One.Properties using (One-FinitelyCocomplete)
open import Data.Product.Base using (_,_; proj₁; proj₂; map; dmap; zip′)
-open import Functor.Exact using (∘-RightExactFunctor; RightExactFunctor; idREF; IsRightExact; rightexact)
open import Function.Base using (id; flip)
-open import Level using (Level; suc; _⊔_)
+open import Functor.Exact using (∘-RightExactFunctor; RightExactFunctor; idREF; IsRightExact; rightexact)
FinitelyCocompletes : Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
FinitelyCocompletes = categoryHelper record
@@ -48,7 +50,7 @@ FinitelyCocompletes = categoryHelper record
One-FCC : FinitelyCocompleteCategory o ℓ e
One-FCC = record
{ U = One
- ; finCo = One-FinitelyCocomplete
+ ; finCo = OneProps.finitelyCocomplete
}
_×_
@@ -62,7 +64,6 @@ _×_ 𝒞 𝒟 = record
where
module 𝒞 = FinitelyCocompleteCategory 𝒞
module 𝒟 = FinitelyCocompleteCategory 𝒟
-{-# INJECTIVE_FOR_INFERENCE _×_ #-}
module _ (𝒞 𝒟 : FinitelyCocompleteCategory o ℓ e) where
generated by cgit v1.2.3 (git 2.39.1) at 2025-12-14 20:42:57 +0000