From 807a0f3dcdd76c3db5dfff02f7689220af4580ca Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 21 Mar 2018 18:05:25 +0100 Subject: [PATCH] Slight readability improvement --- src/Cat/Categories/Sets.agda | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index 65533a4..b96822b 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -151,9 +151,8 @@ module _ (ℓ : Level) where g : Σ A Q → Σ A P g (a , qA) = a , g' qA where - module E = Equivalence (eA a) k : Eqv.Isomorphism _ - k = E.toIso (_≃_.isEqv (eA a)) + k = Equiv≃.toIso _ _ (_≃_.isEqv (eA a)) open Σ k renaming (proj₁ to g') ve-re : (x : Σ A P) → (g ∘ f) x ≡ x ve-re x i = proj₁ x , eq i @@ -166,9 +165,8 @@ module _ (ℓ : Level) where pA ∎ where open Σ x renaming (proj₁ to a ; proj₂ to pA) - module E = Equivalence (eA a) k : Eqv.Isomorphism _ - k = E.toIso (_≃_.isEqv (eA a)) + k = Equiv≃.toIso _ _ (_≃_.isEqv (eA a)) open Σ k renaming (proj₁ to g' ; proj₂ to inv) module A = AreInverses inv -- anti-funExt @@ -183,9 +181,8 @@ module _ (ℓ : Level) where _≃_.eqv (eA a) (g' qA) ≡⟨ (λ i → A.recto-verso i qA) ⟩ qA ∎ where - module E = Equivalence (eA a) k : Eqv.Isomorphism _ - k = E.toIso (_≃_.isEqv (eA a)) + k = Equiv≃.toIso _ _ (_≃_.isEqv (eA a)) open Σ k renaming (proj₁ to g' ; proj₂ to inv) module A = AreInverses inv inv : AreInverses f g