From 29c4c4a3b9156b66a8bbe428d80abcbf40469cf9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Mon, 7 May 2018 10:12:11 +0200 Subject: [PATCH] Equality principle for isomorphisms --- src/Cat/Category.agda | 20 +++++++------------- 1 file changed, 7 insertions(+), 13 deletions(-) diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index fab184b..95db7ee 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -222,9 +222,9 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where propIsInverseOf : ∀ {A B f g} → isProp (IsInverseOf {A} {B} f g) propIsInverseOf = propSig (arrowsAreSets _ _) (λ _ → arrowsAreSets _ _) - module _ {A B : Object} (f : Arrow A B) where - propIsomorphism : isProp (Isomorphism f) - propIsomorphism a@(g , η , ε) a'@(g' , η' , ε') = + module _ {A B : Object} where + propIsomorphism : (f : Arrow A B) → isProp (Isomorphism f) + propIsomorphism f a@(g , η , ε) a'@(g' , η' , ε') = lemSig (λ g → propIsInverseOf) a a' geq where geq : g ≡ g' @@ -236,6 +236,9 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where identity <<< g' ≡⟨ leftIdentity ⟩ g' ∎ + isoEq : {a b : A ≊ B} → fst a ≡ fst b → a ≡ b + isoEq = lemSig propIsomorphism _ _ + propIsInitial : ∀ I → isProp (IsInitial I) propIsInitial I x y i {X} = res X i where @@ -673,16 +676,7 @@ module Opposite {ℓa ℓb : Level} where -- Shouldn't be necessary to use `arrowsAreSets` here, but we have it, -- so why not? lem : (p : A ≡ B) → idToIso A B p ≡ shuffle~ (ℂ.idToIso A B p) - lem p = Σ≡ refl (Σ≡ refl (Σ≡ (ℂ.arrowsAreSets _ _ l-l r-l) (ℂ.arrowsAreSets _ _ l-r r-r))) - where - l = idToIso A B p - r = shuffle~ (ℂ.idToIso A B p) - open Σ l renaming (fst to l-obv ; snd to l-areInv) - open Σ l-areInv renaming (fst to l-invs ; snd to l-iso) - open Σ l-iso renaming (fst to l-l ; snd to l-r) - open Σ r renaming (fst to r-obv ; snd to r-areInv) - open Σ r-areInv renaming (fst to r-invs ; snd to r-iso) - open Σ r-iso renaming (fst to r-l ; snd to r-r) + lem p = isoEq refl ζ : A ≊ B → A ≡ B ζ = η ∘ shuffle