1 files changed, 173 insertions, 127 deletions

diff --git a/Category/Instance/Cospans.agda b/Category/Instance/Cospans.agda
index d54499d..ae6d359 100644
--- a/Category/Instance/Cospans.agda
+++ b/Category/Instance/Cospans.agda
@@ -7,16 +7,20 @@ open import Level using (_⊔_)
 
 module Category.Instance.Cospans {o ℓ e} (𝒞 : FinitelyCocompleteCategory o ℓ e) where
 
-open FinitelyCocompleteCategory 𝒞
+module 𝒞 = FinitelyCocompleteCategory 𝒞
+open 𝒞 using (U; pushout)
+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ˡ
     )
 
 open import Category.Diagram.Pushout U 
@@ -26,254 +30,296 @@ open import Category.Diagram.Pushout U 
     ; extend-i₁-iso ; extend-i₂-iso
     )
 
-private
-
-  variable
-    A B C D X Y Z : Obj
-    f g h : A ⇒ B
-
 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
+
 compose : Cospan A B → Cospan B C → Cospan A C
-compose c₁ c₂ = record { f₁ = p.i₁ ∘ C₁.f₁ ; f₂ = p.i₂ ∘ C₂.f₂ }
+compose (cospan f g) (cospan h i) = cospan (i₁ ∘ f) (i₂ ∘ i)
   where
-    module C₁ = Cospan c₁
-    module C₂ = Cospan c₂
-    module p = pushout C₁.f₂ C₂.f₁
+    open pushout g h
 
-id-Cospan : Cospan A A
-id-Cospan = record { f₁ = id ; f₂ = id }
+identity : Cospan A A
+identity = cospan id 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₂ }
+compose-3 (cospan f₁ f₂) (cospan g₁ g₂) (cospan h₁ h₂) = cospan (P₃.i₁ ∘ P₁.i₁ ∘ f₁) (P₃.i₂ ∘ P₂.i₂ ∘ h₂)
   where
-    module C₁ = Cospan c₁
-    module C₂ = Cospan c₂
-    module C₃ = Cospan c₃
-    module P₁ = pushout C₁.f₂ C₂.f₁
-    module P₂ = pushout C₂.f₂ C₃.f₁
+    module P₁ = pushout f₂ g₁
+    module P₂ = pushout g₂ h₁
     module P₃ = pushout P₁.i₂ P₂.i₁
 
-record Same (C C′ : Cospan A B) : Set (ℓ ⊔ e) where
+record _≈_ (C D : Cospan A B) : Set (ℓ ⊔ e) where
 
   module C = Cospan C
-  module C′ = Cospan C′
+  module D = Cospan D
 
   field
-    ≅N : C.N ≅ C′.N
+    ≅N : C.N ≅ D.N
 
   open _≅_ ≅N public
   module ≅N = _≅_ ≅N
 
   field
-    from∘f₁≈f₁′ : from ∘ C.f₁ ≈ C′.f₁
-    from∘f₂≈f₂′ : from ∘ C.f₂ ≈ C′.f₂
+    from∘f₁≈f₁ : from ∘ C.f₁ 𝒞.≈ D.f₁
+    from∘f₂≈f₂ : from ∘ C.f₂ 𝒞.≈ D.f₂
+
+private
+  variable
+    f g h : Cospan A B
 
-same-refl : {C : Cospan A B} → Same C C
-same-refl = record
+≈-refl : f ≈ f
+≈-refl {f = cospan f₁ f₂} = record
     { ≅N = ≅.refl
-    ; from∘f₁≈f₁′ = identityˡ
-    ; from∘f₂≈f₂′ = identityˡ
+    ; 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ˡ
 
-same-sym : {C C′ : Cospan A B} → Same C C′ → Same C′ C
-same-sym C≅C′ = record
+≈-sym : f ≈ g → g ≈ f
+≈-sym f≈g = record
     { ≅N = ≅.sym ≅N
-    ; from∘f₁≈f₁′ = Equiv.sym (switch-fromtoˡ ≅N from∘f₁≈f₁′)
-    ; from∘f₂≈f₂′ = Equiv.sym (switch-fromtoˡ ≅N from∘f₂≈f₂′)
+    ; from∘f₁≈f₁ = a
+    ; from∘f₂≈f₂ = b
     }
-  where
-    open Same C≅C′
+  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₂)
 
-same-trans : {C C′ C″ : Cospan A B} → Same C C′ → Same C′ C″ → Same C C″
-same-trans C≈C′ C′≈C″ = record
-    { ≅N = ≅.trans C≈C′.≅N C′≈C″.≅N
-    ; from∘f₁≈f₁′ = glueTrianglesˡ C′≈C″.from∘f₁≈f₁′ C≈C′.from∘f₁≈f₁′
-    ; from∘f₂≈f₂′ = glueTrianglesˡ C′≈C″.from∘f₂≈f₂′ C≈C′.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
-    module C≈C′ = Same C≈C′
-    module C′≈C″ = Same C′≈C″
+  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₂
 
-compose-idˡ : {C : Cospan A B} → Same (compose C id-Cospan) C
-compose-idˡ {_} {_} {C} = record
+≈-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
-    ; from∘f₁≈f₁′ = begin
-          ≅P.from ∘ P.i₁ ∘ C.f₁     ≈⟨ assoc ⟨
-          (≅P.from ∘ P.i₁) ∘ C.f₁   ≈⟨ P.universal∘i₁≈h₁ ⟩∘⟨refl ⟩
-          id ∘ C.f₁                 ≈⟨ identityˡ ⟩
-          C.f₁                      ∎
-    ; from∘f₂≈f₂′ = begin
-          ≅P.from ∘ P.i₂ ∘ id       ≈⟨ refl⟩∘⟨ identityʳ ⟩
-          ≅P.from ∘ P.i₂            ≈⟨ P.universal∘i₂≈h₂ ⟩
-          C.f₂                      ∎
+    ; from∘f₁≈f₁ = from∘f₁≈f₁
+    ; from∘f₂≈f₂ = from∘f₂≈f₂
     }
   where
     open HomReasoning
-    module C = Cospan C
-    P = pushout C.f₂ id
+    P P′ : Pushout f₂ id
+    P = pushout f₂ id
+    P′ = pushout-f-id {f = f₂}
     module P = Pushout P
-    P′ = pushout-f-id {f = C.f₂}
+    ≅P : P.Q ≅ N
     ≅P = up-to-iso P P′
     module ≅P = _≅_ ≅P
+    abstract
+      from∘f₁≈f₁ : ≅P.from ∘ P.i₁ ∘ f₁ 𝒞.≈ f₁
+      from∘f₁≈f₁ = begin
+          ≅P.from ∘ P.i₁ ∘ f₁ ≈⟨ cancelˡ P.universal∘i₁≈h₁ ⟩
+          f₁                  ∎
+      from∘f₂≈f₂ : ≅P.from ∘ P.i₂ ∘ id 𝒞.≈ f₂
+      from∘f₂≈f₂ = begin
+          ≅P.from ∘ P.i₂ ∘ id ≈⟨ refl⟩∘⟨ identityʳ ⟩
+          ≅P.from ∘ P.i₂      ≈⟨ P.universal∘i₂≈h₂ ⟩
+          f₂                  ∎
 
-compose-idʳ : {C : Cospan A B} → Same (compose id-Cospan C) C
-compose-idʳ {_} {_} {C} = record
+compose-idʳ : compose identity f ≈ f
+compose-idʳ {f = cospan {N} f₁ f₂} = record
     { ≅N = ≅P
-    ; from∘f₁≈f₁′ = begin
-          ≅P.from ∘ P.i₁ ∘ id       ≈⟨ refl⟩∘⟨ identityʳ ⟩
-          ≅P.from ∘ P.i₁            ≈⟨ P.universal∘i₁≈h₁ ⟩
-          C.f₁                      ∎
-    ; from∘f₂≈f₂′ = begin
-          ≅P.from ∘ P.i₂ ∘ C.f₂     ≈⟨ assoc ⟨
-          (≅P.from ∘ P.i₂) ∘ C.f₂   ≈⟨ P.universal∘i₂≈h₂ ⟩∘⟨refl ⟩
-          id ∘ C.f₂                 ≈⟨ identityˡ ⟩
-          C.f₂                      ∎
+    ; from∘f₁≈f₁ = from∘f₁≈f₁
+    ; from∘f₂≈f₂ = from∘f₂≈f₂
     }
   where
     open HomReasoning
-    module C = Cospan C
-    P = pushout id C.f₁
+    P P′ : Pushout id f₁
+    P = pushout id f₁
     module P = Pushout P
-    P′ = pushout-id-g {g = C.f₁}
+    P′ = pushout-id-g {g = f₁}
+    ≅P : P.Q ≅ N
     ≅P = up-to-iso P P′
     module ≅P = _≅_ ≅P
+    abstract
+      from∘f₁≈f₁ : ≅P.from ∘ P.i₁ ∘ id 𝒞.≈ f₁
+      from∘f₁≈f₁ = begin
+          ≅P.from ∘ P.i₁ ∘ id ≈⟨ refl⟩∘⟨ identityʳ ⟩
+          ≅P.from ∘ P.i₁      ≈⟨ P.universal∘i₁≈h₁ ⟩
+          f₁                  ∎
+      from∘f₂≈f₂ : ≅P.from ∘ P.i₂ ∘ f₂ 𝒞.≈ f₂
+      from∘f₂≈f₂ = begin
+          ≅P.from ∘ P.i₂ ∘ f₂ ≈⟨ cancelˡ P.universal∘i₂≈h₂ ⟩
+          f₂                  ∎
 
-compose-id² : Same {A} (compose id-Cospan id-Cospan) id-Cospan
+compose-id² : compose identity identity ≈ identity {A}
 compose-id² = compose-idˡ
 
-compose-3-right
-    : {c₁ : Cospan A B}
-      {c₂ : Cospan B C}
-      {c₃ : Cospan C D}
-    → Same (compose c₁ (compose c₂ c₃)) (compose-3 c₁ c₂ c₃)
-compose-3-right {_} {_} {_} {_} {c₁} {c₂} {c₃} = record
-    { ≅N = up-to-iso P₄′ P₄
-    ; from∘f₁≈f₁′ = sym-assoc ○ P₄′.universal∘i₁≈h₁ ⟩∘⟨refl ○ assoc
-    ; from∘f₂≈f₂′ = sym-assoc ○ P₄′.universal∘i₂≈h₂ ⟩∘⟨refl
+compose-3-right : compose f (compose g h) ≈ compose-3 f g h
+compose-3-right {f = f} {g = g} {h = h} = record
+    { ≅N = ≅N
+    ; from∘f₁≈f₁ = from∘f₁≈f₁
+    ; from∘f₂≈f₂ = from∘f₂≈f₂
     }
   where
     open HomReasoning
-    module C₁ = Cospan c₁
-    module C₂ = Cospan c₂
-    module C₃ = Cospan c₃
+    module C₁ = Cospan f
+    module C₂ = Cospan g
+    module C₃ = Cospan h
+    P₁ : Pushout C₁.f₂ C₂.f₁
     P₁ = pushout C₁.f₂ C₂.f₁
+    P₂ : Pushout C₂.f₂ C₃.f₁
     P₂ = pushout C₂.f₂ C₃.f₁
     module P₁ = Pushout P₁
     module P₂ = Pushout P₂
+    P₃ : Pushout P₁.i₂ P₂.i₁
     P₃ = pushout P₁.i₂ P₂.i₁
     module P₃ = Pushout P₃
+    P₄ P₄′ : Pushout C₁.f₂ (P₂.i₁ ∘ C₂.f₁)
     P₄ = glue-i₂ P₁ P₃
-    module P₄ = Pushout P₄
     P₄′ = pushout C₁.f₂ (P₂.i₁ ∘ C₂.f₁)
+    module P₄ = Pushout P₄
     module P₄′ = Pushout P₄′
+    ≅N : P₄′.Q ≅ P₄.Q
+    ≅N = up-to-iso P₄′ P₄
+    module ≅N = _≅_ ≅N
+    abstract
+      from∘f₁≈f₁ : ≅N.from ∘ P₄′.i₁ ∘ C₁.f₁ 𝒞.≈ P₃.i₁ ∘ P₁.i₁ ∘ C₁.f₁
+      from∘f₁≈f₁ = sym-assoc ○ P₄′.universal∘i₁≈h₁ ⟩∘⟨refl ○ assoc
+      from∘f₂≈f₂ : ≅N.from ∘ P₄′.i₂ ∘ P₂.i₂ ∘ C₃.f₂ 𝒞.≈ P₄.i₂ ∘ P₂.i₂ ∘ C₃.f₂
+      from∘f₂≈f₂ = sym-assoc ○ P₄′.universal∘i₂≈h₂ ⟩∘⟨refl
 
-compose-3-left
-    : {c₁ : Cospan A B}
-      {c₂ : Cospan B C}
-      {c₃ : Cospan C D}
-    → Same (compose (compose c₁ c₂) c₃) (compose-3 c₁ c₂ c₃)
-compose-3-left {_} {_} {_} {_} {c₁} {c₂} {c₃} = record
+compose-3-left : compose (compose f g) h ≈ compose-3 f g h
+compose-3-left {f = f} {g = g} {h = h} = record
     { ≅N = up-to-iso P₄′ P₄
-    ; from∘f₁≈f₁′ = sym-assoc ○ P₄′.universal∘i₁≈h₁ ⟩∘⟨refl
-    ; from∘f₂≈f₂′ = sym-assoc ○ P₄′.universal∘i₂≈h₂ ⟩∘⟨refl ○ assoc
+    ; from∘f₁≈f₁ = from∘f₁≈f₁
+    ; from∘f₂≈f₂ = from∘f₂≈f₂
     }
   where
     open HomReasoning
-    module C₁ = Cospan c₁
-    module C₂ = Cospan c₂
-    module C₃ = Cospan c₃
+    module C₁ = Cospan f
+    module C₂ = Cospan g
+    module C₃ = Cospan h
+    P₁ : Pushout C₁.f₂ C₂.f₁
     P₁ = pushout C₁.f₂ C₂.f₁
+    P₂ : Pushout C₂.f₂ C₃.f₁
     P₂ = pushout C₂.f₂ C₃.f₁
     module P₁ = Pushout P₁
     module P₂ = Pushout P₂
+    P₃ : Pushout P₁.i₂ P₂.i₁
     P₃ = pushout P₁.i₂ P₂.i₁
     module P₃ = Pushout P₃
+    P₄ P₄′ : Pushout (P₁.i₂ ∘ C₂.f₂) C₃.f₁
     P₄ = glue-i₁ P₂ P₃
-    module P₄ = Pushout P₄
     P₄′ = pushout (P₁.i₂ ∘ C₂.f₂) C₃.f₁
+    module P₄ = Pushout P₄
     module P₄′ = Pushout P₄′
+    ≅N : P₄′.Q ≅ P₄.Q
+    ≅N = up-to-iso P₄′ P₄
+    module ≅N = _≅_ ≅N
+    abstract
+      from∘f₁≈f₁ : ≅N.from ∘ P₄′.i₁ ∘ P₁.i₁ ∘ C₁.f₁ 𝒞.≈ P₄.i₁ ∘ P₁.i₁ ∘ C₁.f₁
+      from∘f₁≈f₁ = sym-assoc ○ P₄′.universal∘i₁≈h₁ ⟩∘⟨refl
+      from∘f₂≈f₂ : ≅N.from ∘ P₄′.i₂ ∘ C₃.f₂ 𝒞.≈ P₃.i₂ ∘ P₂.i₂ ∘ C₃.f₂
+      from∘f₂≈f₂ = sym-assoc ○ P₄′.universal∘i₂≈h₂ ⟩∘⟨refl ○ assoc
 
 compose-assoc
     : {c₁ : Cospan A B}
       {c₂ : Cospan B C}
       {c₃ : Cospan C D}
-    → Same (compose c₁ (compose c₂ c₃)) (compose (compose c₁ c₂) c₃)
-compose-assoc = same-trans compose-3-right (same-sym compose-3-left)
+    → compose c₁ (compose c₂ c₃) ≈ (compose (compose c₁ c₂) c₃)
+compose-assoc = ≈-trans compose-3-right (≈-sym compose-3-left)
 
 compose-sym-assoc
     : {c₁ : Cospan A B}
       {c₂ : Cospan B C}
       {c₃ : Cospan C D}
-    → Same (compose (compose c₁ c₂) c₃) (compose c₁ (compose c₂ c₃))
-compose-sym-assoc = same-trans compose-3-left (same-sym compose-3-right)
+    → compose (compose c₁ c₂) c₃ ≈ compose c₁ (compose c₂ c₃)
+compose-sym-assoc = ≈-trans compose-3-left (≈-sym compose-3-right)
 
 compose-equiv
     : {c₂ c₂′ : Cospan B C}
       {c₁ c₁′ : Cospan A B}
-    → Same c₂ c₂′
-    → Same c₁ c₁′
-    → Same (compose c₁ c₂) (compose c₁′ c₂′)
+    → c₂ ≈ c₂′
+    → c₁ ≈ c₁′
+    → compose c₁ c₂ ≈ compose c₁′ c₂′
 compose-equiv {_} {_} {_} {c₂} {c₂′} {c₁} {c₁′} ≈C₂ ≈C₁ = record
-    { ≅N = up-to-iso P P″
-    ; from∘f₁≈f₁′ = begin
-          ≅P.from ∘ P.i₁ ∘ C₁.f₁      ≈⟨ assoc ⟨
-          (≅P.from ∘ P.i₁) ∘ C₁.f₁    ≈⟨ P.universal∘i₁≈h₁ ⟩∘⟨refl ⟩
-          (P′.i₁ ∘ ≈C₁.from) ∘ C₁.f₁  ≈⟨ assoc ⟩
-          P′.i₁ ∘ ≈C₁.from ∘ C₁.f₁    ≈⟨ refl⟩∘⟨ ≈C₁.from∘f₁≈f₁′ ⟩
-          P′.i₁ ∘ C₁′.f₁              ∎
-    ; from∘f₂≈f₂′ = begin
-          ≅P.from ∘ P.i₂ ∘ C₂.f₂      ≈⟨ assoc ⟨
-          (≅P.from ∘ P.i₂) ∘ C₂.f₂    ≈⟨ P.universal∘i₂≈h₂ ⟩∘⟨refl ⟩
-          (P′.i₂ ∘ ≈C₂.from) ∘ C₂.f₂  ≈⟨ assoc ⟩
-          P′.i₂ ∘ ≈C₂.from ∘ C₂.f₂    ≈⟨ refl⟩∘⟨ ≈C₂.from∘f₂≈f₂′ ⟩
-          P′.i₂ ∘ C₂′.f₂              ∎
+    { ≅N = ≅P
+    ; from∘f₁≈f₁ = from∘f₁≈f₁
+    ; from∘f₂≈f₂ = from∘f₂≈f₂
     }
   where
     module C₁ = Cospan c₁
     module C₁′ = Cospan c₁′
     module C₂ = Cospan c₂
     module C₂′ = Cospan c₂′
+    P : Pushout C₁.f₂ C₂.f₁
     P = pushout C₁.f₂ C₂.f₁
+    P′ : Pushout C₁′.f₂ C₂′.f₁
     P′ = pushout C₁′.f₂ C₂′.f₁
-    module ≈C₁ = Same ≈C₁
-    module ≈C₂ = Same ≈C₂
+    module ≈C₁ = _≈_ ≈C₁
+    module ≈C₂ = _≈_ ≈C₂
     P′′ : Pushout (≈C₁.to ∘ C₁′.f₂) (≈C₂.to ∘ C₂′.f₁)
     P′′ = extend-i₂-iso (extend-i₁-iso P′ (≅.sym ≈C₁.≅N)) (≅.sym ≈C₂.≅N)
     P″ : Pushout C₁.f₂ C₂.f₁
     P″ =
         pushout-resp-≈
             P′′
-            (Equiv.sym (switch-fromtoˡ ≈C₁.≅N ≈C₁.from∘f₂≈f₂′))
-            (Equiv.sym (switch-fromtoˡ ≈C₂.≅N ≈C₂.from∘f₁≈f₁′))
+            (Equiv.sym (switch-fromtoˡ ≈C₁.≅N ≈C₁.from∘f₂≈f₂))
+            (Equiv.sym (switch-fromtoˡ ≈C₂.≅N ≈C₂.from∘f₁≈f₁))
     module P = Pushout P
     module P′ = Pushout P′
     ≅P : P.Q ≅ P′.Q
     ≅P = up-to-iso P P″
     module ≅P = _≅_ ≅P
     open HomReasoning
+    abstract
+      from∘f₁≈f₁ : ≅P.from ∘ P.i₁ ∘ C₁.f₁ 𝒞.≈ P′.i₁ ∘ C₁′.f₁
+      from∘f₁≈f₁ = begin
+          ≅P.from ∘ P.i₁ ∘ C₁.f₁      ≈⟨ pullˡ P.universal∘i₁≈h₁ ⟩
+          (P′.i₁ ∘ ≈C₁.from) ∘ C₁.f₁  ≈⟨ pullʳ ≈C₁.from∘f₁≈f₁ ⟩
+          P′.i₁ ∘ C₁′.f₁              ∎
+      from∘f₂≈f₂ : ≅P.from ∘ P.i₂ ∘ C₂.f₂ 𝒞.≈ P′.i₂ ∘ C₂′.f₂
+      from∘f₂≈f₂ = begin
+          ≅P.from ∘ P.i₂ ∘ C₂.f₂      ≈⟨ pullˡ P.universal∘i₂≈h₂ ⟩
+          (P′.i₂ ∘ ≈C₂.from) ∘ C₂.f₂  ≈⟨ pullʳ ≈C₂.from∘f₂≈f₂ ⟩
+          P′.i₂ ∘ C₂′.f₂              ∎
 
 Cospans : Category o (o ⊔ ℓ) (ℓ ⊔ e)
 Cospans = record
     { Obj = Obj
     ; _⇒_ = Cospan
-    ; _≈_ = Same
-    ; id = id-Cospan
+    ; _≈_ = _≈_
+    ; id = identity
     ; _∘_ = flip compose
     ; assoc = compose-assoc
     ; sym-assoc = compose-sym-assoc
     ; identityˡ = compose-idˡ
     ; identityʳ = compose-idʳ
     ; identity² = compose-id²
-    ; equiv = record
-        { refl = same-refl
-        ; sym = same-sym
-        ; trans = same-trans
-        }
+    ; equiv = ≈-equiv
     ; ∘-resp-≈ = compose-equiv
     }