Update agda-categories version

3 files changed, 61 insertions, 55 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