From 6023a49da6a08d9c58312c08bca239944f928e5e Mon Sep 17 00:00:00 2001 From: Andrea Vezzosi Date: Fri, 13 Apr 2018 14:35:10 +0200 Subject: [PATCH] Category.Product: get rid of the yellow --- src/Cat/Category/Product.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda index dcb200a..86dd336 100644 --- a/src/Cat/Category/Product.agda +++ b/src/Cat/Category/Product.agda @@ -189,9 +189,9 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} -- Should follow from c being univalent iso-id-inv : {p : X ≡ Y} → p ≡ ℂ.isoToId (ℂ.idToIso X Y p) - iso-id-inv {p} = sym (λ i → AreInverses.verso-recto ℂ.inverse-from-to-iso' i p) + iso-id-inv {p} = sym (λ i → fst (ℂ.inverse-from-to-iso' {X} {Y}) i p) id-iso-inv : {iso : X ℂ.≅ Y} → iso ≡ ℂ.idToIso X Y (ℂ.isoToId iso) - id-iso-inv {iso} = sym (λ i → AreInverses.recto-verso ℂ.inverse-from-to-iso' i iso) + id-iso-inv {iso} = sym (λ i → snd (ℂ.inverse-from-to-iso' {X} {Y}) i iso) lemA : {A B : Object} {f g : Arrow A B} → fst f ≡ fst g → f ≡ g lemA {A} {B} {f = f} {g} p i = p i , h i