From d63ecc3a6577463bddcd7f1d5dd53bdd760605ac Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Sun, 25 Feb 2018 14:39:11 +0100 Subject: [PATCH] Use abbreviation --- src/Cat/Category/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda index e929d81..1b75397 100644 --- a/src/Cat/Category/Properties.agda +++ b/src/Cat/Category/Properties.agda @@ -15,7 +15,7 @@ open Equality.Data.Product module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where 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 (f- , left-inv , right-inv) g₀ g₁ eq = begin g₀ ≡⟨ sym (proj₁ isIdentity) ⟩