diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2024-08-24 12:59:59 -0500 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2024-08-24 12:59:59 -0500 |
| commit | dc3b799d6f9cdd4fb0b2b32f323b7128ccc14a80 (patch) | |
| tree | 142676656f8d57ac8680611d026209806c65d313 /Cospan.agda | |
| parent | 4df023f2f98b5105dbd3164f74fe7b431dd628bc (diff) | |
Generalize coequalizer result to arbitrary category
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 |