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

refactor(hott/arity): cleanup

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-10 15:45:46 -07:00
parent 8b062b4448
commit 01127061f5
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/arity.hlean
View file

@ -185,12 +185,12 @@ namespace funext
adjointify _
eq_of_homotopy3
begin
intro H, apply eq_of_homotopy, intro a,
apply concat,
{apply (ap (λx, @apd100 _ _ (λ(b : B a)(c : C a b), _) _ _ (x a))),
apply (right_inv apd10)},
--TODO: remove implicit argument after #469 is closed
apply (@right_inv _ _ apd100 !is_equiv_apd100) --is explicit argument needed here?
intro H, esimp,
apply eq_of_homotopy, intro a,
transitivity apd100 (eq_of_homotopy2 (H a)),
{apply ap (λx, apd100 (x a)),
apply right_inv apd10},
apply right_inv apd100
end
begin
intro p, cases p, apply eq_of_homotopy3_id