From 024ce8012f77e450e2724e943827cd93e9574a6d Mon Sep 17 00:00:00 2001 From: Jakob von Raumer Date: Thu, 19 Mar 2015 17:25:20 -0400 Subject: [PATCH] fix(hott/algebra) make previously added lemma more applicable to groupoids --- hott/algebra/precategory/functor.hlean | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/hott/algebra/precategory/functor.hlean b/hott/algebra/precategory/functor.hlean index e7512b2a0..3a1f9ef2e 100644 --- a/hott/algebra/precategory/functor.hlean +++ b/hott/algebra/precategory/functor.hlean @@ -99,16 +99,15 @@ namespace functor attribute preserve_iso [instance] - protected definition respect_inv (F : C ⇒ D) {a b : C} (f : hom a b) [H : is_iso f] : + protected definition respect_inv (F : C ⇒ D) {a b : C} (f : hom a b) + [H : is_iso f] [H' : is_iso (F f)] : F (f⁻¹) = (F f)⁻¹ := begin fapply @left_inverse_eq_right_inverse, apply (F f), apply concat, apply inverse, apply (respect_comp F), apply concat, apply (ap (λ x, to_fun_hom F x)), apply left_inverse, apply respect_id, - apply concat, apply inverse, apply (respect_comp F), - apply concat, apply (ap (λ x, to_fun_hom F x)), - apply right_inverse, apply respect_id, + apply right_inverse, end protected definition assoc (H : C ⇒ D) (G : B ⇒ C) (F : A ⇒ B) :