fredefox/cat
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Use abbreviation

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-02-25 14:39:11 +01:00
parent caddf83a09
commit d63ecc3a65
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Cat/Category/Properties.agda
View file

@ -15,7 +15,7 @@ open Equality.Data.Product
module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
open Category ℂ open Category ℂ
module _ {A B : Category.Object ℂ } {X : Category.Object ℂ} (f : Category.Arrow ℂ A B) where module _ {A B : Object} {X : Object} (f : Arrow A B) where
iso-is-epi : Isomorphism f → Epimorphism {X = X} f iso-is-epi : Isomorphism f → Epimorphism {X = X} f
iso-is-epi (f- , left-inv , right-inv) g₀ g₁ eq = begin iso-is-epi (f- , left-inv , right-inv) g₀ g₁ eq = begin
g₀ ≡⟨ sym (proj₁ isIdentity) ⟩ g₀ ≡⟨ sym (proj₁ isIdentity) ⟩