diff options
| -rw-r--r-- | Category/Diagram/Pushout.agda | 92 | ||||
| -rw-r--r-- | Category/Instance/Cospans.agda | 15 | ||||
| -rw-r--r-- | Category/Instance/DecoratedCospans.agda | 9 | ||||
| -rw-r--r-- | Coeq.agda | 6 |
4 files changed, 64 insertions, 58 deletions
diff --git a/Category/Diagram/Pushout.agda b/Category/Diagram/Pushout.agda index 8ca384f..1523223 100644 --- a/Category/Diagram/Pushout.agda +++ b/Category/Diagram/Pushout.agda @@ -5,8 +5,6 @@ module Category.Diagram.Pushout {o ℓ e} (𝒞 : Category o ℓ e) where open Category 𝒞 -import Categories.Diagram.Pullback op as Pb using (up-to-iso) - open import Categories.Diagram.Duality 𝒞 using (Pushout⇒coPullback) open import Categories.Diagram.Pushout 𝒞 using (Pushout) open import Categories.Diagram.Pushout.Properties 𝒞 using (glue; swap) @@ -15,8 +13,12 @@ open import Categories.Morphism.Duality 𝒞 using (op-≅⇒≅) open import Categories.Morphism.Reasoning 𝒞 using ( id-comm ; id-comm-sym - ; assoc²'' - ; assoc²' + ; assoc²εβ + ; assoc²γδ + ; assoc²γβ + ; assoc²βγ + ; introʳ + ; elimʳ ) @@ -32,31 +34,32 @@ glue-i₁ p = glue p glue-i₂ : (p₁ : Pushout f g) → Pushout (Pushout.i₂ p₁) h → Pushout f (h ∘ g) glue-i₂ p₁ p₂ = swap (glue (swap p₁) (swap p₂)) -up-to-iso : (p p′ : Pushout f g) → Pushout.Q p ≅ Pushout.Q p′ -up-to-iso p p′ = op-≅⇒≅ (Pb.up-to-iso (Pushout⇒coPullback p) (Pushout⇒coPullback p′)) - pushout-f-id : Pushout f id pushout-f-id {_} {_} {f} = record { i₁ = id ; i₂ = f - ; commute = id-comm-sym - ; universal = λ {B} {h₁} {h₂} eq → h₁ - ; unique = λ {E} {h₁} {h₂} {eq} {j} j∘i₁≈h₁ j∘i₂≈h₂ → Equiv.sym identityʳ ○ j∘i₁≈h₁ - ; universal∘i₁≈h₁ = λ {E} {h₁} {h₂} {eq} → identityʳ - ; universal∘i₂≈h₂ = λ {E} {h₁} {h₂} {eq} → eq ○ identityʳ + ; isPushout = record + { commute = id-comm-sym + ; universal = λ {B} {h₁} {h₂} eq → h₁ + ; universal∘i₁≈h₁ = λ {E} {h₁} {h₂} {eq} → identityʳ + ; universal∘i₂≈h₂ = λ {E} {h₁} {h₂} {eq} → eq ○ identityʳ + ; unique-diagram = λ eq₁ eq₂ → Equiv.sym identityʳ ○ eq₁ ○ identityʳ + } } where open HomReasoning pushout-id-g : Pushout id g -pushout-id-g {_} {_} {g} = record +pushout-id-g {A} {B} {g} = record { i₁ = g ; i₂ = id - ; commute = id-comm - ; universal = λ {B} {h₁} {h₂} eq → h₂ - ; unique = λ {E} {h₁} {h₂} {eq} {j} j∘i₁≈h₁ j∘i₂≈h₂ → Equiv.sym identityʳ ○ j∘i₂≈h₂ - ; universal∘i₁≈h₁ = λ {E} {h₁} {h₂} {eq} → Equiv.sym eq ○ identityʳ - ; universal∘i₂≈h₂ = λ {E} {h₁} {h₂} {eq} → identityʳ + ; isPushout = record + { commute = id-comm + ; universal = λ {B} {h₁} {h₂} eq → h₂ + ; universal∘i₁≈h₁ = λ {E} {h₁} {h₂} {eq} → Equiv.sym eq ○ identityʳ + ; universal∘i₂≈h₂ = λ {E} {h₁} {h₂} {eq} → identityʳ + ; unique-diagram = λ eq₁ eq₂ → Equiv.sym identityʳ ○ eq₂ ○ identityʳ + } } where open HomReasoning @@ -70,31 +73,34 @@ extend-i₁-iso extend-i₁-iso {_} {_} {_} {_} {f} {g} p B≅D = record { i₁ = P.i₁ ∘ B≅D.to ; i₂ = P.i₂ - ; commute = begin - (P.i₁ ∘ B≅D.to) ∘ B≅D.from ∘ f ≈⟨ assoc²'' ⟨ - P.i₁ ∘ (B≅D.to ∘ B≅D.from) ∘ f ≈⟨ refl⟩∘⟨ B≅D.isoˡ ⟩∘⟨refl ⟩ - P.i₁ ∘ id ∘ f ≈⟨ refl⟩∘⟨ identityˡ ⟩ - P.i₁ ∘ f ≈⟨ P.commute ⟩ - P.i₂ ∘ g ∎ - ; universal = λ { eq → P.universal (assoc ○ eq) } - ; unique = λ {_} {h₁} {_} {j} ≈₁ ≈₂ → - let - ≈₁′ = begin - j ∘ P.i₁ ≈⟨ refl⟩∘⟨ identityʳ ⟨ - j ∘ P.i₁ ∘ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ B≅D.isoˡ ⟨ - j ∘ P.i₁ ∘ B≅D.to ∘ B≅D.from ≈⟨ assoc²' ⟨ - (j ∘ P.i₁ ∘ B≅D.to) ∘ B≅D.from ≈⟨ ≈₁ ⟩∘⟨refl ⟩ - h₁ ∘ B≅D.from ∎ - in P.unique ≈₁′ ≈₂ - ; universal∘i₁≈h₁ = λ {E} {h₁} {_} {eq} → - begin - P.universal (assoc ○ eq) ∘ P.i₁ ∘ B≅D.to ≈⟨ sym-assoc ⟩ - (P.universal (assoc ○ eq) ∘ P.i₁) ∘ B≅D.to ≈⟨ P.universal∘i₁≈h₁ ⟩∘⟨refl ⟩ - (h₁ ∘ B≅D.from) ∘ B≅D.to ≈⟨ assoc ⟩ - h₁ ∘ B≅D.from ∘ B≅D.to ≈⟨ refl⟩∘⟨ B≅D.isoʳ ⟩ - h₁ ∘ id ≈⟨ identityʳ ⟩ - h₁ ∎ - ; universal∘i₂≈h₂ = P.universal∘i₂≈h₂ + ; isPushout = record + { commute = begin + (P.i₁ ∘ B≅D.to) ∘ B≅D.from ∘ f ≈⟨ assoc²γδ ⟩ + P.i₁ ∘ (B≅D.to ∘ B≅D.from) ∘ f ≈⟨ refl⟩∘⟨ B≅D.isoˡ ⟩∘⟨refl ⟩ + P.i₁ ∘ id ∘ f ≈⟨ refl⟩∘⟨ identityˡ ⟩ + P.i₁ ∘ f ≈⟨ P.commute ⟩ + P.i₂ ∘ g ∎ + ; universal = λ { eq → P.universal (assoc ○ eq) } + ; universal∘i₁≈h₁ = λ {E} {h₁} {_} {eq} → + begin + P.universal (assoc ○ eq) ∘ P.i₁ ∘ B≅D.to ≈⟨ sym-assoc ⟩ + (P.universal (assoc ○ eq) ∘ P.i₁) ∘ B≅D.to ≈⟨ P.universal∘i₁≈h₁ ⟩∘⟨refl ⟩ + (h₁ ∘ B≅D.from) ∘ B≅D.to ≈⟨ assoc ⟩ + h₁ ∘ B≅D.from ∘ B≅D.to ≈⟨ refl⟩∘⟨ B≅D.isoʳ ⟩ + h₁ ∘ id ≈⟨ identityʳ ⟩ + h₁ ∎ + ; universal∘i₂≈h₂ = P.universal∘i₂≈h₂ + ; unique-diagram = λ {_} {h} {j} ≈₁ ≈₂ → + let + ≈₁′ = begin + h ∘ P.i₁ ≈⟨ introʳ B≅D.isoˡ ⟩ + (h ∘ P.i₁) ∘ B≅D.to ∘ B≅D.from ≈⟨ assoc²γβ ⟩ + (h ∘ P.i₁ ∘ B≅D.to) ∘ B≅D.from ≈⟨ ≈₁ ⟩∘⟨refl ⟩ + (j ∘ P.i₁ ∘ B≅D.to) ∘ B≅D.from ≈⟨ assoc²βγ ⟩ + (j ∘ P.i₁) ∘ B≅D.to ∘ B≅D.from ≈⟨ elimʳ B≅D.isoˡ ⟩ + j ∘ P.i₁ ∎ + in P.unique-diagram ≈₁′ ≈₂ + } } where module P = Pushout p diff --git a/Category/Instance/Cospans.agda b/Category/Instance/Cospans.agda index 0dee26c..d54499d 100644 --- a/Category/Instance/Cospans.agda +++ b/Category/Instance/Cospans.agda @@ -10,7 +10,7 @@ module Category.Instance.Cospans {o ℓ e} (𝒞 : FinitelyCocompleteCategory o open FinitelyCocompleteCategory 𝒞 open import Categories.Diagram.Pushout U using (Pushout) -open import Categories.Diagram.Pushout.Properties U using (pushout-resp-≈) +open import Categories.Diagram.Pushout.Properties U using (pushout-resp-≈; up-to-iso) open import Categories.Morphism U using (_≅_; module ≅) open import Categories.Morphism.Reasoning U using @@ -22,7 +22,6 @@ open import Categories.Morphism.Reasoning U open import Category.Diagram.Pushout U using ( glue-i₁ ; glue-i₂ - ; up-to-iso ; pushout-f-id ; pushout-id-g ; extend-i₁-iso ; extend-i₂-iso ) @@ -47,8 +46,8 @@ compose c₁ c₂ = record { f₁ = p.i₁ ∘ C₁.f₁ ; f₂ = p.i₂ ∘ C module C₂ = Cospan c₂ module p = pushout C₁.f₂ C₂.f₁ -identity : Cospan A A -identity = record { f₁ = id ; f₂ = id } +id-Cospan : Cospan A A +id-Cospan = record { f₁ = id ; f₂ = id } compose-3 : Cospan A B → Cospan B C → Cospan C D → Cospan A D compose-3 c₁ c₂ c₃ = record { f₁ = P₃.i₁ ∘ P₁.i₁ ∘ C₁.f₁ ; f₂ = P₃.i₂ ∘ P₂.i₂ ∘ C₃.f₂ } @@ -101,7 +100,7 @@ same-trans C≈C′ C′≈C″ = record module C≈C′ = Same C≈C′ module C′≈C″ = Same C′≈C″ -compose-idˡ : {C : Cospan A B} → Same (compose C identity) C +compose-idˡ : {C : Cospan A B} → Same (compose C id-Cospan) C compose-idˡ {_} {_} {C} = record { ≅N = ≅P ; from∘f₁≈f₁′ = begin @@ -123,7 +122,7 @@ compose-idˡ {_} {_} {C} = record ≅P = up-to-iso P P′ module ≅P = _≅_ ≅P -compose-idʳ : {C : Cospan A B} → Same (compose identity C) C +compose-idʳ : {C : Cospan A B} → Same (compose id-Cospan C) C compose-idʳ {_} {_} {C} = record { ≅N = ≅P ; from∘f₁≈f₁′ = begin @@ -145,7 +144,7 @@ compose-idʳ {_} {_} {C} = record ≅P = up-to-iso P P′ module ≅P = _≅_ ≅P -compose-id² : Same {A} (compose identity identity) identity +compose-id² : Same {A} (compose id-Cospan id-Cospan) id-Cospan compose-id² = compose-idˡ compose-3-right @@ -264,7 +263,7 @@ Cospans = record { Obj = Obj ; _⇒_ = Cospan ; _≈_ = Same - ; id = identity + ; id = id-Cospan ; _∘_ = flip compose ; assoc = compose-assoc ; sym-assoc = compose-sym-assoc diff --git a/Category/Instance/DecoratedCospans.agda b/Category/Instance/DecoratedCospans.agda index 3f9b6ee..c0c62c7 100644 --- a/Category/Instance/DecoratedCospans.agda +++ b/Category/Instance/DecoratedCospans.agda @@ -23,6 +23,7 @@ import Category.Instance.Cospans 𝒞 as Cospans open import Categories.Category using (Category; _[_∘_]) open import Categories.Category.Cocartesian using (module CocartesianMonoidal) open import Categories.Diagram.Pushout using (Pushout) +open import Categories.Diagram.Pushout.Properties 𝒞.U using (up-to-iso) open import Categories.Functor.Properties using ([_]-resp-≅) open import Categories.Morphism.Reasoning using (switch-fromtoˡ; glueTrianglesˡ) open import Cospan.Decorated 𝒞 F using (DecoratedCospan) @@ -30,7 +31,7 @@ open import Data.Product using (_,_) open import Function using (flip) open import Level using (_⊔_) -open import Category.Diagram.Pushout 𝒞.U using (glue-i₁; glue-i₂; pushout-id-g; pushout-f-id; up-to-iso) +open import Category.Diagram.Pushout 𝒞.U using (glue-i₁; glue-i₂; pushout-id-g; pushout-f-id) import Category.Monoidal.Coherence as Coherence @@ -66,7 +67,7 @@ compose c₁ c₂ = record identity : DecoratedCospan A A identity = record - { cospan = Cospans.identity + { cospan = Cospans.id-Cospan ; decoration = 𝒟.U [ F₁ 𝒞.initial.! ∘ ε ] } @@ -629,8 +630,8 @@ compose-equiv {_} {_} {_} {c₂} {c₂′} {c₁} {c₁′} ≅C₂ ≅C₁ = re F₁ [ P′.i₁ , P′.i₂ ] ∘ φ (N′ , M′) ∘ (F₁ N⇒ ∘ s) ⊗₁ (F₁ M⇒ ∘ t) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ≅C₁.same-deco ⟩⊗⟨ ≅C₂.same-deco ⟩∘⟨refl ⟩ F₁ [ P′.i₁ , P′.i₂ ] ∘ φ (N′ , M′) ∘ s′ ⊗₁ t′ ∘ ρ⇐ ∎ -Cospans : Category o (o ⊔ ℓ ⊔ ℓ′) (ℓ ⊔ e ⊔ e′) -Cospans = record +DecoratedCospans : Category o (o ⊔ ℓ ⊔ ℓ′) (ℓ ⊔ e ⊔ e′) +DecoratedCospans = record { Obj = 𝒞.Obj ; _⇒_ = DecoratedCospan ; _≈_ = Same @@ -5,7 +5,7 @@ module Coeq {o ℓ e} (C : Category o ℓ e) where open import Categories.Diagram.Coequalizer C using (IsCoequalizer) open import Categories.Object.Coproduct C using (Coproduct; IsCoproduct; IsCoproduct⇒Coproduct) -open import Categories.Morphism.Reasoning.Core C using (pullˡ; pushˡ; extendˡ; extendʳ; assoc²') +open import Categories.Morphism.Reasoning.Core C using (pullˡ; pushˡ; extendˡ; extendʳ; assoc²βε; assoc²εβ) open import Function using (_$_) open Category C @@ -33,9 +33,9 @@ coequalizer-on-coproduct {C = C} {Q₁} {Q₂} {f = f} {g} {q₁} {q₂} coprod module X₂ = IsCoequalizer coeq₂ open Coproduct (IsCoproduct⇒Coproduct coprod) using (g-η; [_,_]; unique; i₁; i₂) on-i₁ : (q₂ ∘ q₁ ∘ f) ∘ i₁ ≈ (q₂ ∘ q₁ ∘ g) ∘ i₁ - on-i₁ = assoc²' ○ refl⟩∘⟨ X₁.equality ○ Equiv.sym assoc²' + on-i₁ = assoc²βε ○ refl⟩∘⟨ X₁.equality ○ assoc²εβ on-i₂ : (q₂ ∘ q₁ ∘ f) ∘ i₂ ≈ (q₂ ∘ q₁ ∘ g) ∘ i₂ - on-i₂ = assoc²' ○ X₂.equality ○ Equiv.sym assoc²' + on-i₂ = assoc²βε ○ X₂.equality ○ assoc²εβ equality : q₂ ∘ q₁ ∘ f ≈ q₂ ∘ q₁ ∘ g equality = begin q₂ ∘ q₁ ∘ f ≈⟨ unique on-i₁ on-i₂ ⟨ |