diff options
Diffstat (limited to 'Category/Instance/Cospans.agda')
| -rw-r--r-- | Category/Instance/Cospans.agda | 106 |
1 files changed, 11 insertions, 95 deletions
diff --git a/Category/Instance/Cospans.agda b/Category/Instance/Cospans.agda index ccefcf5..0dee26c 100644 --- a/Category/Instance/Cospans.agda +++ b/Category/Instance/Cospans.agda @@ -9,24 +9,23 @@ module Category.Instance.Cospans {o ℓ e} (𝒞 : FinitelyCocompleteCategory o open FinitelyCocompleteCategory 𝒞 -open import Categories.Diagram.Duality U using (Pushout⇒coPullback) open import Categories.Diagram.Pushout U using (Pushout) -open import Categories.Diagram.Pushout.Properties U using (glue; swap; pushout-resp-≈) +open import Categories.Diagram.Pushout.Properties U using (pushout-resp-≈) open import Categories.Morphism U using (_≅_; module ≅) -open import Categories.Morphism.Duality U using (op-≅⇒≅) -open import Categories.Morphism.Reasoning U using +open import Categories.Morphism.Reasoning U + using ( switch-fromtoˡ ; glueTrianglesˡ - ; id-comm - ; id-comm-sym - ; pullˡ - ; pullʳ - ; assoc²'' - ; assoc²' + ; pullˡ ; pullʳ ) -import Categories.Diagram.Pullback op as Pb using (up-to-iso) - +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 + ) private @@ -102,89 +101,6 @@ same-trans C≈C′ C′≈C″ = record module C≈C′ = Same C≈C′ module C′≈C″ = Same C′≈C″ -glue-i₁ : (p : Pushout f g) → Pushout h (Pushout.i₁ p) → Pushout (h ∘ f) g -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ʳ - } - where - open HomReasoning - -pushout-id-g : Pushout id g -pushout-id-g {_} {_} {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ʳ - } - where - open HomReasoning - -extend-i₁-iso - : {f : A ⇒ B} - {g : A ⇒ C} - (p : Pushout f g) - (B≅D : B ≅ D) - → Pushout (_≅_.from B≅D ∘ f) g -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₂ - } - where - module P = Pushout p - module B≅D = _≅_ B≅D - open HomReasoning - -extend-i₂-iso - : {f : A ⇒ B} - {g : A ⇒ C} - (p : Pushout f g) - (C≅D : C ≅ D) - → Pushout f (_≅_.from C≅D ∘ g) -extend-i₂-iso {_} {_} {_} {_} {f} {g} p C≅D = swap (extend-i₁-iso (swap p) C≅D) - compose-idˡ : {C : Cospan A B} → Same (compose C identity) C compose-idˡ {_} {_} {C} = record { ≅N = ≅P |