michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(hott/algebra) make previously added lemma more applicable to groupoids

Browse source
This commit is contained in:
Jakob von Raumer 2015-03-19 17:25:20 -04:00 committed by Leonardo de Moura
parent 97a1cc8edb
commit 024ce8012f
1 changed files with 3 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
hott/algebra/precategory/functor.hlean
View file

@ -99,16 +99,15 @@ namespace functor
attribute preserve_iso [instance] 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)⁻¹ := F (f⁻¹) = (F f)⁻¹ :=
begin begin
fapply @left_inverse_eq_right_inverse, apply (F f), fapply @left_inverse_eq_right_inverse, apply (F f),
apply concat, apply inverse, apply (respect_comp F), apply concat, apply inverse, apply (respect_comp F),
apply concat, apply (ap (λ x, to_fun_hom F x)), apply concat, apply (ap (λ x, to_fun_hom F x)),
apply left_inverse, apply respect_id, apply left_inverse, apply respect_id,
apply concat, apply inverse, apply (respect_comp F), apply right_inverse,
apply concat, apply (ap (λ x, to_fun_hom F x)),
apply right_inverse, apply respect_id,
end end
protected definition assoc (H : C ⇒ D) (G : B ⇒ C) (F : A ⇒ B) : protected definition assoc (H : C ⇒ D) (G : B ⇒ C) (F : A ⇒ B) :