Finish category of decorated cospans

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