From 2469b8a2f8712a654c052c08a6e94fdb4b68ac54 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Sat, 4 Apr 2015 00:20:19 -0400 Subject: [PATCH] feat(hott): add primitive hits --- hott/hit/pushout.hlean | 124 ++++++++++++++++++++++++++++++++ hott/hit/suspension.hlean | 41 +++++++++++ hott/init/default.hlean | 2 +- hott/init/hit.hlean | 144 ++++++++++++++++++++++++++++++++++++++ 4 files changed, 310 insertions(+), 1 deletion(-) create mode 100644 hott/hit/pushout.hlean create mode 100644 hott/hit/suspension.hlean create mode 100644 hott/init/hit.hlean diff --git a/hott/hit/pushout.hlean b/hott/hit/pushout.hlean new file mode 100644 index 000000000..8fd5a0777 --- /dev/null +++ b/hott/hit/pushout.hlean @@ -0,0 +1,124 @@ +/- +Copyright (c) 2015 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: hit.pushout +Authors: Floris van Doorn + +Declaration of pushout +-/ + +open colimit bool eq + +namespace pushout +context + +universe u +parameters {TL BL TR : Type.{u}} (f : TL → BL) (g : TL → TR) + + inductive pushout_ob := + | tl : pushout_ob + | bl : pushout_ob + | tr : pushout_ob + + open pushout_ob + + definition pushout_diag [reducible] : diagram := + diagram.mk pushout_ob + bool + (λi, pushout_ob.rec_on i TL BL TR) + (λj, bool.rec_on j tl tl) + (λj, bool.rec_on j bl tr) + (λj, bool.rec_on j f g) + + local notation `D` := pushout_diag + -- open bool + -- definition pushout_diag : diagram := + -- diagram.mk pushout_ob + -- bool + -- (λi, match i with | tl := TL | tr := TR | bl := BL end) + -- (λj, match j with | tt := tl | ff := tl end) + -- (λj, match j with | tt := bl | ff := tr end) + -- (λj, match j with | tt := f | ff := g end) + + definition pushout := colimit pushout_diag + local attribute pushout_diag [instance] + + definition inl (x : BL) : pushout := + @ι _ _ x + + definition inr (x : TR) : pushout := + @ι _ _ x + + definition coherence (x : TL) : inl (f x) = @ι _ _ x := + @cglue _ _ x + + definition glue (x : TL) : inl (f x) = inr (g x) := + @cglue _ _ x ⬝ (@cglue _ _ x)⁻¹ + + protected definition rec {P : pushout → Type} (Pinl : Π(x : BL), P (inl x)) + (Pinr : Π(x : TR), P (inr x)) (Pglue : Π(x : TL), glue x ▹ Pinl (f x) = Pinr (g x)) + (y : pushout) : P y := + begin + fapply (@colimit.rec_on _ _ y), + { intros [i, x], cases i, + exact (coherence x ▹ Pinl (f x)), + apply Pinl, + apply Pinr}, + { intros [j, x], cases j, + exact idp, + esimp [pushout_ob.cases_on, pushout_diag], +-- change (transport P (@cglue _ tt x) (Pinr (g x)) = transport P (coherence x) (Pinl (f x))), + -- apply concat;rotate 1;apply (idpath (coherence x ▹ Pinl (f x))), + -- apply concat;apply (ap (transport _ _));apply (idpath (Pinr (g x))), + apply tr_eq_of_eq_inv_tr, +-- rewrite -{(transport (λ (x : pushout), P x) (inverse (coherence x)) (transport P (@cglue _ tt x) (Pinr (g x))))}tr_con, + apply concat, rotate 1, apply tr_con, + rewrite -Pglue} + end + + protected definition rec_on {P : pushout → Type} (y : pushout) (Pinl : Π(x : BL), P (inl x)) + (Pinr : Π(x : TR), P (inr x)) (Pglue : Π(x : TL), glue x ▹ Pinl (f x) = Pinr (g x)) : P y := + rec Pinl Pinr Pglue y + + definition comp_inl {P : pushout → Type} (Pinl : Π(x : BL), P (inl x)) + (Pinr : Π(x : TR), P (inr x)) (Pglue : Π(x : TL), glue x ▹ Pinl (f x) = Pinr (g x)) + (x : BL) : rec Pinl Pinr Pglue (inl x) = Pinl x := + @colimit.comp_incl _ _ _ _ _ _ --idp + + definition comp_inr {P : pushout → Type} (Pinl : Π(x : BL), P (inl x)) + (Pinr : Π(x : TR), P (inr x)) (Pglue : Π(x : TL), glue x ▹ Pinl (f x) = Pinr (g x)) + (x : TR) : rec Pinl Pinr Pglue (inr x) = Pinr x := + @colimit.comp_incl _ _ _ _ _ _ --idp + + definition comp_glue {P : pushout → Type} (Pinl : Π(x : BL), P (inl x)) + (Pinr : Π(x : TR), P (inr x)) (Pglue : Π(x : TL), glue x ▹ Pinl (f x) = Pinr (g x)) + (x : TL) : apD (rec Pinl Pinr Pglue) (glue x) = sorry ⬝ Pglue x ⬝ sorry := + sorry + +end +end pushout + +open pushout equiv is_equiv unit + +namespace test + definition foo (u : empty) : unit := star + + example : pushout foo foo ≃ bool := + begin + fapply equiv.MK, + { intro x, fapply (pushout.rec_on _ _ x), + { intro u, exact ff}, + { intro u, exact tt}, + { intro c, cases c}}, + { intro b, cases b, + { exact (inl _ _ ⋆)}, + { exact (inr _ _ ⋆)},}, + { intro b, cases b, apply comp_inl, apply comp_inr}, + { intro x, fapply (pushout.rec_on _ _ x), + { intro u, cases u, rewrite [↑function.compose,↑pushout.rec_on,comp_inl]}, + { intro u, cases u, rewrite [↑function.compose,↑pushout.rec_on,comp_inr]}, + { intro c, cases c}}, + end + +end test diff --git a/hott/hit/suspension.hlean b/hott/hit/suspension.hlean new file mode 100644 index 000000000..d700335da --- /dev/null +++ b/hott/hit/suspension.hlean @@ -0,0 +1,41 @@ +/- +Copyright (c) 2015 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: hit.suspension +Authors: Floris van Doorn + +Declaration of suspension +-/ + +import .pushout + +open pushout unit eq + +definition suspension (A : Type) : Type := pushout (λ(a : A), star) (λ(a : A), star) + +namespace suspension + + definition north (A : Type) : suspension A := + inl _ _ star + + definition south (A : Type) : suspension A := + inr _ _ star + + definition merid {A : Type} (a : A) : north A = south A := + glue _ _ a + + protected definition rec {A : Type} {P : suspension A → Type} (PN : P !north) (PS : P !south) + (Pmerid : Π(a : A), merid a ▹ PN = PS) (y : suspension A) : P y := + begin + fapply (pushout.rec_on _ _ y), + { intro u, cases u, exact PN}, + { intro u, cases u, exact PS}, + { exact Pmerid}, + end + + protected definition rec_on {A : Type} {P : suspension A → Type} (y : suspension A) + (PN : P !north) (PS : P !south) (Pmerid : Π(a : A), merid a ▹ PN = PS) : P y := + rec PN PS Pmerid y + +end suspension diff --git a/hott/init/default.hlean b/hott/init/default.hlean index 9da50a761..56397d75e 100644 --- a/hott/init/default.hlean +++ b/hott/init/default.hlean @@ -12,4 +12,4 @@ import init.bool init.num init.priority init.relation init.wf import init.types.sigma init.types.prod init.types.empty import init.trunc init.path init.equiv init.util import init.axioms.ua init.axioms.funext_of_ua -import init.hedberg init.nat +import init.hedberg init.nat init.hit diff --git a/hott/init/hit.hlean b/hott/init/hit.hlean new file mode 100644 index 000000000..e1e0983ad --- /dev/null +++ b/hott/init/hit.hlean @@ -0,0 +1,144 @@ +/- +Copyright (c) 2015 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: init.hit +Authors: Floris van Doorn + +Declaration of the primitive hits in Lean +-/ + +prelude + +import .trunc + +open is_trunc eq + +constant trunc.{u} (n : trunc_index) (A : Type.{u}) : Type.{u} + +namespace trunc + + constant tr {n : trunc_index} {A : Type} (a : A) : trunc n A + constant is_trunc_trunc (n : trunc_index) (A : Type) : is_trunc n (trunc n A) + + attribute is_trunc_trunc [instance] + + /-protected-/ constant rec {n : trunc_index} {A : Type} {P : trunc n A → Type} + [Pt : Πaa, is_trunc n (P aa)] (H : Πa, P (tr a)) : Πaa, P aa + + protected definition rec_on {n : trunc_index} {A : Type} {P : trunc n A → Type} (aa : trunc n A) + [Pt : Πaa, is_trunc n (P aa)] (H : Πa, P (tr a)) : P aa := + trunc.rec H aa + + definition comp_tr {n : trunc_index} {A : Type} {P : trunc n A → Type} + [Pt : Πaa, is_trunc n (P aa)] (H : Πa, P (tr a)) (a : A) : trunc.rec H (tr a) = H a := + sorry --idp + +end trunc + +constant cylinder.{u v} {A : Type.{u}} {B : Type.{v}} (f : A → B) : B → Type.{max u v} + +namespace cylinder + + constant base {A B : Type} (f : A → B) (b : B) : cylinder f b + constant top {A B : Type} (f : A → B) (a : A) : cylinder f (f a) + constant seg {A B : Type} (f : A → B) (a : A) : top f a = base f (f a) + + axiom is_trunc_trunc (n : trunc_index) (A : Type) : is_trunc n (trunc n A) + + attribute is_trunc_trunc [instance] + + /-protected-/ constant rec {A B : Type} {f : A → B} {P : Π{b : B}, cylinder f b → Type} + (Pbase : Π(b : B), P (base f b)) (Ptop : Π(a : A), P (top f a)) + (Pseg : Π(a : A), seg f a ▹ Ptop a = Pbase (f a)) + : Π{b : B} (x : cylinder f b), P x + + protected definition rec_on {A B : Type} {f : A → B} {P : Π{b : B}, cylinder f b → Type} + {b : B} (x : cylinder f b) (Pbase : Π(b : B), P (base f b)) (Ptop : Π(a : A), P (top f a)) + (Pseg : Π(a : A), seg f a ▹ Ptop a = Pbase (f a)) : P x := + cylinder.rec Pbase Ptop Pseg x + + definition comp_base {A B : Type} {f : A → B} {P : Π{b : B}, cylinder f b → Type} + (Pbase : Π(b : B), P (base f b)) (Ptop : Π(a : A), P (top f a)) + (Pseg : Π(a : A), seg f a ▹ Ptop a = Pbase (f a)) (b : B) : + cylinder.rec Pbase Ptop Pseg (base f b) = Pbase b := + sorry --idp + + definition comp_top {A B : Type} {f : A → B} {P : Π{b : B}, cylinder f b → Type} + (Pbase : Π(b : B), P (base f b)) (Ptop : Π(a : A), P (top f a)) + (Pseg : Π(a : A), seg f a ▹ Ptop a = Pbase (f a)) (a : A) : + cylinder.rec Pbase Ptop Pseg (top f a) = Ptop a := + sorry --idp + + definition comp_seg {A B : Type} {f : A → B} {P : Π{b : B}, cylinder f b → Type} + (Pbase : Π(b : B), P (base f b)) (Ptop : Π(a : A), P (top f a)) + (Pseg : Π(a : A), seg f a ▹ Ptop a = Pbase (f a)) (a : A) : + apD (cylinder.rec Pbase Ptop Pseg) (seg f a) = sorry ⬝ Pseg a ⬝ sorry := + --the sorry's in the statement can be removed when comp_base/comp_top are definitional + sorry + +end cylinder + + +namespace colimit +structure diagram [class] := + (Iob : Type) + (Ihom : Type) + (ob : Iob → Type) + (dom cod : Ihom → Iob) + (hom : Π(j : Ihom), ob (dom j) → ob (cod j)) +end colimit +open eq colimit colimit.diagram + +constant colimit.{u v w} : diagram.{u v w} → Type.{max u v w} + +namespace colimit + + constant inclusion : Π [D : diagram] {i : Iob}, ob i → colimit D + abbreviation ι := @inclusion + + constant cglue : Π [D : diagram] (j : Ihom) (x : ob (dom j)), ι (hom j x) = ι x + + /-protected-/ constant rec : Π [D : diagram] {P : colimit D → Type} + (Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x)) + (Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▹ Pincl (hom j x) = Pincl x) + (y : colimit D), P y + + definition comp_incl [D : diagram] {P : colimit D → Type} + (Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x)) + (Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▹ Pincl (hom j x) = Pincl x) + {i : Iob} (x : ob i) : rec Pincl Pglue (ι x) = Pincl x := + sorry --idp + + definition comp_cglue [D : diagram] {P : colimit D → Type} + (Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x)) + (Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▹ Pincl (hom j x) = Pincl x) + {j : Ihom} (x : ob (dom j)) : apD (rec Pincl Pglue) (cglue j x) = sorry ⬝ Pglue j x ⬝ sorry := + --the sorry's in the statement can be removed when comp_incl is definitional + sorry + + protected definition rec_on [D : diagram] {P : colimit D → Type} (y : colimit D) + (Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x)) + (Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▹ Pincl (hom j x) = Pincl x) : P y := + colimit.rec Pincl Pglue y + +end colimit + +exit +--ALTERNATIVE: COLIMIT without definition "diagram" +constant colimit.{u v w} : Π {I : Type.{u}} {J : Type.{v}} (ob : I → Type.{w}) {dom : J → I} + {cod : J → I} (hom : Π⦃j : J⦄, ob (dom j) → ob (cod j)), Type.{max u v w} + +namespace colimit + + constant inclusion : Π {I J : Type} {ob : I → Type} {dom : J → I} {cod : J → I} + (hom : Π⦃j : J⦄, ob (dom j) → ob (cod j)) {i : I}, ob i → colimit ob hom + abbreviation ι := @inclusion + + constant glue : Π {I J : Type} {ob : I → Type} {dom : J → I} {cod : J → I} + (hom : Π⦃j : J⦄, ob (dom j) → ob (cod j)) (j : J) (a : ob (dom j)), ι hom (hom a) = ι hom a + + /-protected-/ constant rec : Π {I J : Type} {ob : I → Type} {dom : J → I} {cod : J → I} + (hom : Π⦃j : J⦄, ob (dom j) → ob (cod j)) {P : colimit ob hom → Type} + -- ... +end colimit