diff options
Diffstat (limited to 'Cospan.agda')
| -rw-r--r-- | Cospan.agda | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/Cospan.agda b/Cospan.agda index f3bb5f5..3c5296d 100644 --- a/Cospan.agda +++ b/Cospan.agda @@ -110,9 +110,6 @@ 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′)) -id-unique : (p : Pushout f g) → (Pushout.universal p) (Pushout.commute p) ≈ id -id-unique p = Equiv.sym (Pushout.unique p identityˡ identityˡ) - pushout-f-id : Pushout f id pushout-f-id {_} {_} {f} = record { i₁ = id |