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

refactor(hott/algebra/category/constructions/functor): cleanup proof

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-07 15:29:02 -07:00
parent 45c8cdc626
commit 21ee0a5ff9
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
hott/algebra/category/constructions/functor.hlean
View file

@ -122,12 +122,12 @@ namespace category
begin begin
fapply functor_eq, fapply functor_eq,
{exact (eq_of_iso_ob η)}, {exact (eq_of_iso_ob η)},
{intro c c' f, --unfold eq_of_iso_ob, --TODO: report: this fails {intro c c' f,
apply concat, esimp [eq_of_iso_ob, inv_of_eq, hom_of_eq, eq_of_iso],
{apply (ap (λx, to_hom x ∘ to_fun_hom F f ∘ _)), apply (right_inv iso_of_eq)}, rewrite [*right_inv iso_of_eq],
apply concat, esimp [function.id],
{apply (ap (λx, _ ∘ to_fun_hom F f ∘ (to_hom x)⁻¹)), apply (right_inv iso_of_eq)}, symmetry, apply naturality_iso
symmetry, apply naturality_iso} }
end end
definition iso_of_eq_eq_of_iso (η : F ≅ G) : iso_of_eq (eq_of_iso η) = η := definition iso_of_eq_eq_of_iso (η : F ≅ G) : iso_of_eq (eq_of_iso η) = η :=