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

feat(hit.trunc): replace sorry by proof

Browse source
This commit is contained in:
Floris van Doorn 2015-05-15 20:23:34 -04:00 committed by Leonardo de Moura
parent de6294a4ce
commit 6ca9635d53
2 changed files with 28 additions and 30 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
hott/hit/trunc.hlean
View file

@ -77,24 +77,18 @@ namespace trunc
section
open prod.ops
-- definition trunc_prod_equiv : trunc n (X × Y) ≃ trunc n X × trunc n Y :=
-- sorry
-- equiv.MK (λpp, trunc.rec_on pp (λp, (tr p.1, tr p.2)))
-- (λp, trunc.rec_on p.1 (λx, trunc.rec_on p.2 (λy, tr (x,y))))
-- sorry --(λp, trunc.rec_on p.1 (λx, trunc.rec_on p.2 (λy, idp)))
-- (λpp, trunc.rec_on pp (λp, prod.rec_on p (λx y, idp)))
-- begin
-- fapply equiv.MK,
-- apply sorry, --{exact (λpp, trunc.rec_on pp (λp, (tr p.1, tr p.2)))},
-- apply sorry, /-{intro p, cases p with xx yy,
-- apply (trunc.rec_on xx), intro x,
-- apply (trunc.rec_on yy), intro y, exact (tr (x,y))},-/
-- apply sorry, /-{intro p, cases p with xx yy,
-- apply (trunc.rec_on xx), intro x,
-- apply (trunc.rec_on yy), intro y, apply idp},-/
-- apply sorry --{intro pp, apply (trunc.rec_on pp), intro p, cases p, apply idp},
-- end
definition trunc_prod_equiv : trunc n (X × Y) ≃ trunc n X × trunc n Y :=
begin
fapply equiv.MK,
{exact (λpp, trunc.rec_on pp (λp, (tr p.1, tr p.2)))},
{intro p, cases p with xx yy,
apply (trunc.rec_on xx), intro x,
apply (trunc.rec_on yy), intro y, exact (tr (x,y))},
{intro p, cases p with xx yy,
apply (trunc.rec_on xx), intro x,
apply (trunc.rec_on yy), intro y, apply idp},
{intro pp, apply (trunc.rec_on pp), intro p, cases p, apply idp}
end
end
/- Propositional truncation -/

28
hott/types/trunc.hlean
View file

@ -148,25 +148,29 @@ namespace trunc
protected definition code (n : trunc_index) (aa aa' : trunc n.+1 A) : n-Type :=
trunc.rec_on aa (λa, trunc.rec_on aa' (λa', trunctype.mk' n (trunc n (a = a'))))
-- protected definition encode (n : trunc_index) (aa aa' : trunc n.+1 A) : aa = aa' → code n aa aa' :=
-- trunc.rec_on aa (λa, trunc.rec_on aa' (λa' p, _))
protected definition encode (n : trunc_index) (aa aa' : trunc n.+1 A) : aa = aa' → code n aa aa' :=
begin
intro p, cases p, apply (trunc.rec_on aa),
intro a, esimp [code,trunc.rec_on], exact (tr idp)
end
protected definition decode (n : trunc_index) (aa aa' : trunc n.+1 A) : code n aa aa' → aa = aa' :=
begin
eapply (trunc.rec_on aa'), eapply (trunc.rec_on aa),
intro a a' x, esimp [code, trunc.rec_on] at x,
apply (trunc.rec_on x), intro p, exact (ap tr p)
end
definition trunc_eq_equiv (n : trunc_index) (aa aa' : trunc n.+1 A)
: aa = aa' ≃ code n aa aa' :=
begin
fapply equiv.MK,
{ intro p, cases p, apply (trunc.rec_on aa),
intro a, esimp [code,trunc.rec_on], exact (tr idp)},
{ apply encode},
{ apply decode},
{ eapply (trunc.rec_on aa'), eapply (trunc.rec_on aa),
intro a a' x, esimp [code, trunc.rec_on] at x,
apply (trunc.rec_on x), intro p, exact (ap tr p)},
{
-- apply (trunc.rec_on aa'), apply (trunc.rec_on aa),
-- intro a a' x, esimp [code, trunc.rec_on] at x,
-- apply (trunc.rec_on x), intro p,
-- cases p, esimp [trunc.rec_on,eq.cases_on,compose,id], -- apply idp --?
apply sorry},
{ intro p, cases p, apply (trunc.rec_on aa), intro a, apply sorry},
apply (trunc.rec_on x), intro p, cases p, exact idp},
{ intro p, cases p, apply (trunc.rec_on aa), intro a, exact idp},
end
definition tr_eq_tr_equiv (n : trunc_index) (a a' : A)