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

refactor(hott/choice): rename lemmas for 3.8.2

Browse source
This commit is contained in:
seulbaek 2016-01-19 16:02:17 -08:00 committed by Leonardo de Moura
parent d42f3d313f
commit 107550238b
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
hott/choice.hlean
View file

@ -28,13 +28,13 @@ section
(to_inv !sigma_pi_equiv_pi_sigma) (H X A P HX HA HP HI))
-- AC_cart can be derived from AC' by setting P := λ _ _ , unit.
definition AC'_to_AC_cart : AC'.{u} -> AC_cart.{u} :=
definition AC_cart_of_AC' : AC'.{u} -> AC_cart.{u} :=
λ H X A HX HA HI, trunc_functor _ (λ H0 x, (H0 x).1)
(H X A (λ x a, lift.{0 u} unit) HX HA (λ x a, !is_trunc_lift)
(λ x, trunc_functor _ (λ a, ⟨a, lift.up.{0 u} unit.star⟩) (HI x)))
-- And the converse, by setting A := λ x, Σ a, P x a.
definition AC_cart_to_AC' : AC_cart.{u} -> AC'.{u} :=
definition AC'_of_AC_cart : AC_cart.{u} -> AC'.{u} :=
by intro H X A P HX HA HP HI;
apply H X (λ x, Σ a, P x a) HX (λ x, !is_trunc_sigma) HI