From 51e87213d04b116b57a9d170016cdc7335715b0f Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Mon, 6 Apr 2015 21:01:08 -0400 Subject: [PATCH] feat(hit): define nondependent recursors for all hits, sequential colimit, and elaborate on spheres squash --- hott/hit/circle.hlean | 97 +++++++++++++++++++++++++++ hott/hit/colimit.hlean | 88 ++++++++++++++++++++++++ hott/hit/cylinder.hlean | 33 +++++++++ hott/hit/pushout.hlean | 81 ++++++++++++++--------- hott/hit/sphere.hlean | 85 ++++++++++++++++++++++++ hott/hit/suspension.hlean | 85 +++++++----------------- hott/hit/trunc.hlean | 136 ++++++++++++++++++++++++++++++++++++++ hott/init/hit.hlean | 66 +++++++++--------- 8 files changed, 543 insertions(+), 128 deletions(-) create mode 100644 hott/hit/circle.hlean create mode 100644 hott/hit/colimit.hlean create mode 100644 hott/hit/cylinder.hlean create mode 100644 hott/hit/sphere.hlean create mode 100644 hott/hit/trunc.hlean diff --git a/hott/hit/circle.hlean b/hott/hit/circle.hlean new file mode 100644 index 000000000..f63a5b992 --- /dev/null +++ b/hott/hit/circle.hlean @@ -0,0 +1,97 @@ +/- +Copyright (c) 2015 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: hit.circle +Authors: Floris van Doorn + +Declaration of the circle +-/ + +import .sphere + +open eq suspension bool sphere_index + +definition circle [reducible] := suspension bool --redefine this as sphere 1 + +namespace circle + + definition base1 : circle := !north + definition base2 : circle := !south + definition seg1 : base1 = base2 := merid tt + definition seg2 : base2 = base1 := (merid ff)⁻¹ + + definition base : circle := base1 + definition loop : base = base := seg1 ⬝ seg2 + + definition rec2 {P : circle → Type} (Pb1 : P base1) (Pb2 : P base2) + (Ps1 : seg1 ▹ Pb1 = Pb2) (Ps2 : seg2 ▹ Pb2 = Pb1) (x : circle) : P x := + begin + fapply (suspension.rec_on x), + { exact Pb1}, + { exact Pb2}, + { intro b, cases b, + apply tr_eq_of_eq_inv_tr, exact Ps2⁻¹, + exact Ps1}, + end + + definition rec2_on [reducible] {P : circle → Type} (x : circle) (Pb1 : P base1) (Pb2 : P base2) + (Ps1 : seg1 ▹ Pb1 = Pb2) (Ps2 : seg2 ▹ Pb2 = Pb1) : P x := + circle.rec2 Pb1 Pb2 Ps1 Ps2 x + + definition rec2_seg1 {P : circle → Type} (Pb1 : P base1) (Pb2 : P base2) + (Ps1 : seg1 ▹ Pb1 = Pb2) (Ps2 : seg2 ▹ Pb2 = Pb1) + : apD (rec2 Pb1 Pb2 Ps1 Ps2) seg1 = sorry ⬝ Ps1 ⬝ sorry := + sorry + + definition rec2_seg2 {P : circle → Type} (Pb1 : P base1) (Pb2 : P base2) + (Ps1 : seg1 ▹ Pb1 = Pb2) (Ps2 : seg2 ▹ Pb2 = Pb1) + : apD (rec2 Pb1 Pb2 Ps1 Ps2) seg2 = sorry ⬝ Ps2 ⬝ sorry := + sorry + + definition elim2 {P : Type} (Pb1 Pb2 : P) (Ps1 : Pb1 = Pb2) (Ps2 : Pb2 = Pb1) (x : circle) : P := + rec2 Pb1 Pb2 (!tr_constant ⬝ Ps1) (!tr_constant ⬝ Ps2) x + + definition elim2_on [reducible] {P : Type} (x : circle) (Pb1 Pb2 : P) + (Ps1 : Pb1 = Pb2) (Ps2 : Pb2 = Pb1) : P := + elim2 Pb1 Pb2 Ps1 Ps2 x + + definition elim2_seg1 {P : Type} (Pb1 Pb2 : P) (Ps1 : Pb1 = Pb2) (Ps2 : Pb2 = Pb1) + : ap (elim2 Pb1 Pb2 Ps1 Ps2) seg1 = sorry ⬝ Ps1 ⬝ sorry := + sorry + + definition elim2_seg2 {P : Type} (Pb1 Pb2 : P) (Ps1 : Pb1 = Pb2) (Ps2 : Pb2 = Pb1) + : ap (elim2 Pb1 Pb2 Ps1 Ps2) seg2 = sorry ⬝ Ps2 ⬝ sorry := + sorry + + protected definition rec {P : circle → Type} (Pbase : P base) (Ploop : loop ▹ Pbase = Pbase) + (x : circle) : P x := + begin + fapply (rec2_on x), + { exact Pbase}, + { exact (transport P seg1 Pbase)}, + { apply idp}, + { apply eq_tr_of_inv_tr_eq, rewrite -tr_con, apply Ploop}, + end + + protected definition rec_on [reducible] {P : circle → Type} (x : circle) (Pbase : P base) + (Ploop : loop ▹ Pbase = Pbase) : P x := + circle.rec Pbase Ploop x + + protected definition elim {P : Type} (Pbase : P) (Ploop : Pbase = Pbase) + (x : circle) : P := + circle.rec Pbase (tr_constant loop Pbase ⬝ Ploop) x + + protected definition elim_on [reducible] {P : Type} (x : circle) (Pbase : P) + (Ploop : Pbase = Pbase) : P := + elim Pbase Ploop x + + definition rec_loop {P : circle → Type} (Pbase : P base) (Ploop : loop ▹ Pbase = Pbase) : + ap (circle.rec Pbase Ploop) loop = sorry ⬝ Ploop ⬝ sorry := + sorry + + definition elim_loop {P : Type} (Pbase : P) (Ploop : Pbase = Pbase) : + ap (circle.elim Pbase Ploop) loop = sorry ⬝ Ploop ⬝ sorry := + sorry + +end circle diff --git a/hott/hit/colimit.hlean b/hott/hit/colimit.hlean new file mode 100644 index 000000000..ac8570047 --- /dev/null +++ b/hott/hit/colimit.hlean @@ -0,0 +1,88 @@ +/- +Copyright (c) 2015 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: hit.colimit +Authors: Floris van Doorn + +Colimits. +-/ + +/- The hit colimit is primitive, declared in init.hit. -/ + +open eq colimit colimit.diagram function + +namespace colimit + + protected definition elim [D : diagram] {P : Type} (Pincl : Π⦃i : Iob⦄ (x : ob i), P) + (Pglue : Π(j : Ihom) (x : ob (dom j)), Pincl (hom j x) = Pincl x) : colimit D → P := + rec Pincl (λj x, !tr_constant ⬝ Pglue j x) + + protected definition elim_on [reducible] [D : diagram] {P : Type} (y : colimit D) + (Pincl : Π⦃i : Iob⦄ (x : ob i), P) + (Pglue : Π(j : Ihom) (x : ob (dom j)), Pincl (hom j x) = Pincl x) : P := + elim Pincl Pglue y + + definition elim_cglue [D : diagram] {P : Type} (Pincl : Π⦃i : Iob⦄ (x : ob i), P) + (Pglue : Π(j : Ihom) (x : ob (dom j)), Pincl (hom j x) = Pincl x) {j : Ihom} (x : ob (dom j)) : + ap (elim Pincl Pglue) (cglue j x) = sorry ⬝ Pglue j x ⬝ sorry := + sorry + +end colimit + +/- definition of a sequential colimit -/ +open nat + +namespace seq_colimit +context + parameters {A : ℕ → Type} (f : Π⦃n⦄, A n → A (succ n)) + variables {n : ℕ} (a : A n) + + definition seq_diagram : diagram := + diagram.mk ℕ ℕ A id succ f + local attribute seq_diagram [instance] + + -- TODO: define this in root namespace + definition seq_colim {A : ℕ → Type} (f : Π⦃n⦄, A n → A (succ n)) : Type := + colimit seq_diagram + + definition inclusion : seq_colim f := + @colimit.inclusion _ _ a + + abbreviation sι := @inclusion + + definition glue : sι (f a) = sι a := + @cglue _ _ a + + protected definition rec [reducible] {P : seq_colim f → Type} + (Pincl : Π⦃n : ℕ⦄ (a : A n), P (sι a)) + (Pglue : Π(n : ℕ) (a : A n), glue a ▹ Pincl (f a) = Pincl a) : Πaa, P aa := + @colimit.rec _ _ Pincl Pglue + + protected definition rec_on [reducible] {P : seq_colim f → Type} (aa : seq_colim f) + (Pincl : Π⦃n : ℕ⦄ (a : A n), P (sι a)) + (Pglue : Π⦃n : ℕ⦄ (a : A n), glue a ▹ Pincl (f a) = Pincl a) + : P aa := + rec Pincl Pglue aa + + protected definition elim {P : Type} (Pincl : Π⦃n : ℕ⦄ (a : A n), P) + (Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) = Pincl a) : seq_colim f → P := + @colimit.elim _ _ Pincl Pglue + + protected definition elim_on [reducible] {P : Type} (aa : seq_colim f) + (Pincl : Π⦃n : ℕ⦄ (a : A n), P) + (Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) = Pincl a) : P := + elim Pincl Pglue aa + + definition rec_glue {P : seq_colim f → Type} (Pincl : Π⦃n : ℕ⦄ (a : A n), P (sι a)) + (Pglue : Π⦃n : ℕ⦄ (a : A n), glue a ▹ Pincl (f a) = Pincl a) {n : ℕ} (a : A n) + : apD (rec Pincl Pglue) (glue a) = sorry ⬝ Pglue a ⬝ sorry := + sorry + + definition elim_glue {P : Type} (Pincl : Π⦃n : ℕ⦄ (a : A n), P) + (Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) = Pincl a) {n : ℕ} (a : A n) + : ap (elim Pincl Pglue) (glue a) = sorry ⬝ Pglue a ⬝ sorry := + sorry + +end +end seq_colimit diff --git a/hott/hit/cylinder.hlean b/hott/hit/cylinder.hlean new file mode 100644 index 000000000..1f0dd963e --- /dev/null +++ b/hott/hit/cylinder.hlean @@ -0,0 +1,33 @@ +/- +Copyright (c) 2015 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: hit.cylinder +Authors: Floris van Doorn + +Mapping cylinders +-/ + +/- The hit mapping cylinder is primitive, declared in init.hit. -/ + +open eq + +namespace cylinder + + variables {A B : Type} {f : A → B} + + protected definition elim {P : Type} (Pbase : B → P) (Ptop : A → P) + (Pseg : Π(a : A), Ptop a = Pbase (f a)) {b : B} (x : cylinder f b) : P := + cylinder.rec Pbase Ptop (λa, !tr_constant ⬝ Pseg a) x + + protected definition elim_on [reducible] {P : Type} {b : B} (x : cylinder f b) + (Pbase : B → P) (Ptop : A → P) + (Pseg : Π(a : A), Ptop a = Pbase (f a)) : P := + cylinder.elim Pbase Ptop Pseg x + + definition elim_seg {P : Type} (Pbase : B → P) (Ptop : A → P) + (Pseg : Π(a : A), Ptop a = Pbase (f a)) {b : B} (x : cylinder f b) (a : A) : + ap (elim Pbase Ptop Pseg) (seg f a) = sorry ⬝ Pseg a ⬝ sorry := + sorry + +end cylinder diff --git a/hott/hit/pushout.hlean b/hott/hit/pushout.hlean index d6fbc72b1..85f6a9eac 100644 --- a/hott/hit/pushout.hlean +++ b/hott/hit/pushout.hlean @@ -8,6 +8,8 @@ Authors: Floris van Doorn Declaration of pushout -/ +import .colimit + open colimit bool eq namespace pushout @@ -41,7 +43,7 @@ parameters {TL BL TR : Type.{u}} (f : TL → BL) (g : TL → TR) -- (λj, match j with | tt := bl | ff := tr end) -- (λj, match j with | tt := f | ff := g end) - definition pushout := colimit pushout_diag + definition pushout := colimit pushout_diag -- TODO: define this in root namespace local attribute pushout_diag [instance] definition inl (x : BL) : pushout := @@ -77,48 +79,63 @@ parameters {TL BL TR : Type.{u}} (f : TL → BL) (g : TL → TR) 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 := + protected definition rec_on [reducible] {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)) + definition rec_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 + @colimit.rec_incl _ _ _ _ _ _ --idp - definition comp_inr {P : pushout → Type} (Pinl : Π(x : BL), P (inl x)) + definition rec_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 + @colimit.rec_incl _ _ _ _ _ _ --idp - definition comp_glue {P : pushout → Type} (Pinl : Π(x : BL), P (inl x)) + protected definition elim {P : Type} (Pinl : BL → P) (Pinr : TR → P) + (Pglue : Π(x : TL), Pinl (f x) = Pinr (g x)) (y : pushout) : P := + rec Pinl Pinr (λx, !tr_constant ⬝ Pglue x) y + + protected definition elim_on [reducible] {P : Type} (Pinl : BL → P) (y : pushout) + (Pinr : TR → P) (Pglue : Π(x : TL), Pinl (f x) = Pinr (g x)) : P := + elim Pinl Pinr Pglue y + + definition rec_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 + definition elim_glue {P : Type} (Pinl : BL → P) (Pinr : TR → P) + (Pglue : Π(x : TL), Pinl (f x) = Pinr (g x)) (y : pushout) (x : TL) + : ap (elim Pinl Pinr Pglue) (glue x) = sorry ⬝ Pglue x ⬝ sorry := + sorry + + end + + open pushout equiv is_equiv unit + + namespace test + definition unit_of_empty (u : empty) : unit := star + + example : pushout unit_of_empty unit_of_empty ≃ 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 rec_inl, apply rec_inr}, + { intro x, fapply (pushout.rec_on _ _ x), + intro u, cases u, rewrite [↑function.compose,↑pushout.rec_on,rec_inl], + intro u, cases u, rewrite [↑function.compose,↑pushout.rec_on,rec_inr], + intro c, cases c}, + end + + end test 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/sphere.hlean b/hott/hit/sphere.hlean new file mode 100644 index 000000000..24fe55c61 --- /dev/null +++ b/hott/hit/sphere.hlean @@ -0,0 +1,85 @@ +/- +Copyright (c) 2015 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: hit.circle +Authors: Floris van Doorn + +Declaration of the n-spheres +-/ + +import .suspension + +open eq nat suspension bool is_trunc unit + +/- We can define spheres with the following possible indices: +- trunc_index +- nat +- nat, but counting wrong (S^0 = empty, S^1 = bool, ...) +- some new type "integers >= 1" +-/ + + /- Sphere levels -/ + +inductive sphere_index : Type₀ := +| minus_one : sphere_index +| succ : sphere_index → sphere_index + +namespace sphere_index + /- + notation for sphere_index is -1, 0, 1, ... + from 0 and up this comes from a coercion from num to sphere_index (via nat) + -/ + postfix `.+1`:(max+1) := sphere_index.succ + postfix `.+2`:(max+1) := λ(n : sphere_index), (n .+1 .+1) + notation `-1` := minus_one + export [coercions] nat + + definition add (n m : sphere_index) : sphere_index := + sphere_index.rec_on m n (λ k l, l .+1) + + definition leq (n m : sphere_index) : Type₁ := + sphere_index.rec_on n (λm, unit) (λ n p m, sphere_index.rec_on m (λ p, empty) (λ m q p, p m) p) m + + infix `+1+`:65 := sphere_index.add + + notation x <= y := sphere_index.leq x y + notation x ≤ y := sphere_index.leq x y + + definition succ_le_succ {n m : sphere_index} (H : n ≤ m) : n.+1 ≤ m.+1 := H + definition le_of_succ_le_succ {n m : sphere_index} (H : n.+1 ≤ m.+1) : n ≤ m := H + definition minus_two_le (n : sphere_index) : -1 ≤ n := star + definition empty_of_succ_le_minus_two {n : sphere_index} (H : n .+1 ≤ -1) : empty := H + + definition of_nat [coercion] [reducible] (n : nat) : sphere_index := + nat.rec_on n (-1.+1) (λ n k, k.+1) + + definition trunc_index_of_sphere_index [coercion] [reducible] (n : sphere_index) : trunc_index := + sphere_index.rec_on n -1 (λ n k, k.+1) +end sphere_index + +open sphere_index equiv + +definition sphere : sphere_index → Type₀ +| -1 := empty +| n.+1 := suspension (sphere n) + +namespace sphere + namespace ops + abbreviation S := sphere + end ops + + definition bool_of_sphere [reducible] : sphere 0 → bool := + suspension.rec tt ff (λx, empty.elim _ x) + + definition sphere_of_bool [reducible] : bool → sphere 0 + | tt := !north + | ff := !south + + definition sphere_equiv_bool : sphere 0 ≃ bool := + equiv.MK bool_of_sphere + sphere_of_bool + sorry --idp + sorry --idp + +end sphere diff --git a/hott/hit/suspension.hlean b/hott/hit/suspension.hlean index ebd67e6f4..e2215dcaa 100644 --- a/hott/hit/suspension.hlean +++ b/hott/hit/suspension.hlean @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Module: hit.suspension Authors: Floris van Doorn -Declaration of suspension and spheres +Declaration of suspension -/ import .pushout @@ -26,72 +26,33 @@ namespace suspension glue _ _ a protected definition rec {A : Type} {P : suspension A → Type} (PN : P !north) (PS : P !south) - (Pmerid : Π(a : A), merid a ▹ PN = PS) (x : suspension A) : P x := + (Pm : Π(a : A), merid a ▹ PN = PS) (x : suspension A) : P x := begin fapply (pushout.rec_on _ _ x), { intro u, cases u, exact PN}, { intro u, cases u, exact PS}, - { exact Pmerid}, + { exact Pm}, 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 + protected definition rec_on [reducible] {A : Type} {P : suspension A → Type} (y : suspension A) + (PN : P !north) (PS : P !south) (Pm : Π(a : A), merid a ▹ PN = PS) : P y := + rec PN PS Pm y + + definition rec_merid {A : Type} {P : suspension A → Type} (PN : P !north) (PS : P !south) + (Pm : Π(a : A), merid a ▹ PN = PS) (a : A) + : apD (rec PN PS Pm) (merid a) = sorry ⬝ Pm a ⬝ sorry := + sorry + + protected definition elim {A : Type} {P : Type} (PN : P) (PS : P) (Pm : A → PN = PS) + (x : suspension A) : P := + rec PN PS (λa, !tr_constant ⬝ Pm a) x + + protected definition elim_on [reducible] {A : Type} {P : Type} (x : suspension A) + (PN : P) (PS : P) (Pm : A → PN = PS) : P := + rec PN PS (λa, !tr_constant ⬝ Pm a) x + + protected definition elim_merid {A : Type} {P : Type} (PN : P) (PS : P) (Pm : A → PN = PS) + (x : suspension A) (a : A) : ap (elim PN PS Pm) (merid a) = sorry ⬝ Pm a ⬝ sorry := + sorry end suspension - -open nat suspension bool - -definition sphere (n : ℕ) := nat.rec_on n bool (λk Sk, suspension Sk) -definition circle [reducible] := sphere 1 - -namespace circle - - definition base : circle := !north - definition loop : base = base := merid tt ⬝ (merid ff)⁻¹ - - protected definition rec2 {P : circle → Type} (PN : P !north) (PS : P !south) - (Pff : merid ff ▹ PN = PS) (Ptt : merid tt ▹ PN = PS) (x : circle) : P x := - begin - fapply (suspension.rec_on x), - { exact PN}, - { exact PS}, - { intro b, cases b, exact Pff, exact Ptt}, - end - - protected definition rec2_on {P : circle → Type} (x : circle) (PN : P !north) (PS : P !south) - (Pff : merid ff ▹ PN = PS) (Ptt : merid tt ▹ PN = PS) : P x := - circle.rec2 PN PS Pff Ptt x - - protected definition rec {P : circle → Type} (Pbase : P base) (Ploop : loop ▹ Pbase = Pbase) - (x : circle) : P x := - begin - fapply (rec2_on x), - { exact Pbase}, - { sexact (merid ff ▹ Pbase)}, - { apply idp}, - { apply eq_tr_of_inv_tr_eq, rewrite -tr_con, apply Ploop}, - end - - protected definition rec_on {P : circle → Type} (x : circle) (Pbase : P base) - (Ploop : loop ▹ Pbase = Pbase) : P x := - circle.rec Pbase Ploop x - - protected definition rec_constant {P : Type} (Pbase : P) (Ploop : Pbase = Pbase) - (x : circle) : P := - circle.rec Pbase (tr_constant loop Pbase ⬝ Ploop) x - - definition comp_loop {P : circle → Type} (Pbase : P base) (Ploop : loop ▹ Pbase = Pbase) : - ap (circle.rec Pbase Ploop) loop = sorry ⬝ Ploop ⬝ sorry := - sorry - - definition comp_constant_loop {P : Type} (Pbase : P) (Ploop : Pbase = Pbase) : - ap (circle.rec_constant Pbase Ploop) loop = sorry ⬝ Ploop ⬝ sorry := - sorry - - - protected definition rec_on_constant {P : Type} (x : circle) (Pbase : P) (Ploop : Pbase = Pbase) - : P := - rec_constant Pbase Ploop x - -end circle diff --git a/hott/hit/trunc.hlean b/hott/hit/trunc.hlean new file mode 100644 index 000000000..4fb21b3e1 --- /dev/null +++ b/hott/hit/trunc.hlean @@ -0,0 +1,136 @@ +/- +Copyright (c) 2015 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: hit.trunc +Authors: Floris van Doorn + +n-truncation of types. + +Ported from Coq HoTT +-/ + +/- The hit n-truncation is primitive, declared in init.hit. -/ + +import types.sigma + +open is_trunc eq equiv is_equiv function prod sum sigma + +namespace trunc + + protected definition elim {n : trunc_index} {A : Type} {P : Type} + [Pt : is_trunc n P] (H : A → P) : trunc n A → P := + rec H + + protected definition elim_on {n : trunc_index} {A : Type} {P : Type} (aa : trunc n A) + [Pt : is_trunc n P] (H : A → P) : P := + elim H aa + +exit + + variables {X Y Z : Type} {P : X → Type} (A B : Type) (n : trunc_index) + + local attribute is_trunc_eq [instance] + + definition is_equiv_tr [instance] [H : is_trunc n A] : is_equiv (@tr n A) := + adjointify _ + (trunc.rec id) + (λaa, trunc.rec_on aa (λa, idp)) + (λa, idp) + + definition equiv_trunc [H : is_trunc n A] : A ≃ trunc n A := + equiv.mk tr _ + + definition is_trunc_of_is_equiv_tr [H : is_equiv (@tr n A)] : is_trunc n A := + is_trunc_is_equiv_closed n tr⁻¹ + + definition untrunc_of_is_trunc [reducible] [H : is_trunc n A] : trunc n A → A := + tr⁻¹ + + /- Functoriality -/ + definition trunc_functor (f : X → Y) : trunc n X → trunc n Y := + λxx, trunc_rec_on xx (λx, tr (f x)) +-- by intro xx; apply (trunc_rec_on xx); intro x; exact (tr (f x)) +-- by intro xx; fapply (trunc_rec_on xx); intro x; exact (tr (f x)) +-- by intro xx; exact (trunc_rec_on xx (λx, (tr (f x)))) + + definition trunc_functor_compose (f : X → Y) (g : Y → Z) + : trunc_functor n (g ∘ f) ∼ trunc_functor n g ∘ trunc_functor n f := + λxx, trunc_rec_on xx (λx, idp) + + definition trunc_functor_id : trunc_functor n (@id A) ∼ id := + λxx, trunc_rec_on xx (λx, idp) + + definition is_equiv_trunc_functor (f : X → Y) [H : is_equiv f] : is_equiv (trunc_functor n f) := + adjointify _ + (trunc_functor n f⁻¹) + (λyy, trunc_rec_on yy (λy, ap tr !retr)) + (λxx, trunc_rec_on xx (λx, ap tr !sect)) + + 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 + end + + /- Propositional truncation -/ + + -- should this live in hprop? + definition merely [reducible] (A : Type) : Type := trunc -1 A + + notation `||`:max A `||`:0 := merely A + notation `∥`:max A `∥`:0 := merely A + + definition Exists [reducible] (P : X → Type) : Type := ∥ sigma P ∥ + definition or [reducible] (A B : Type) : Type := ∥ A ⊎ B ∥ + + notation `exists` binders `,` r:(scoped P, Exists P) := r + notation `∃` binders `,` r:(scoped P, Exists P) := r + notation A `\/` B := or A B + notation A ∨ B := or A B + + definition merely.intro [reducible] (a : A) : ∥ A ∥ := tr a + definition exists.intro [reducible] (x : X) (p : P x) : ∃x, P x := tr ⟨x, p⟩ + definition or.intro_left [reducible] (x : X) : X ∨ Y := tr (inl x) + definition or.intro_right [reducible] (y : Y) : X ∨ Y := tr (inr y) + + definition is_contr_of_merely_hprop [H : is_hprop A] (aa : merely A) : is_contr A := + is_contr_of_inhabited_hprop (trunc_rec_on aa id) + + section + open sigma.ops + definition trunc_sigma_equiv : trunc n (Σ x, P x) ≃ trunc n (Σ x, trunc n (P x)) := + equiv.MK (λpp, trunc_rec_on pp (λp, tr ⟨p.1, tr p.2⟩)) + (λpp, trunc_rec_on pp (λp, trunc_rec_on p.2 (λb, tr ⟨p.1, b⟩))) + (λpp, trunc_rec_on pp (λp, sigma.rec_on p (λa bb, trunc_rec_on bb (λb, idp)))) + (λpp, trunc_rec_on pp (λp, sigma.rec_on p (λa b, idp))) + + definition trunc_sigma_equiv_of_is_trunc [H : is_trunc n X] + : trunc n (Σ x, P x) ≃ Σ x, trunc n (P x) := + calc + trunc n (Σ x, P x) ≃ trunc n (Σ x, trunc n (P x)) : trunc_sigma_equiv + ... ≃ Σ x, trunc n (P x) : equiv.symm !equiv_trunc + end + +end trunc + + + 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 diff --git a/hott/init/hit.hlean b/hott/init/hit.hlean index e1e0983ad..2f784f5aa 100644 --- a/hott/init/hit.hlean +++ b/hott/init/hit.hlean @@ -14,6 +14,23 @@ import .trunc open is_trunc eq +/- + We take three higher inductive types (hits) as primitive notions in Lean. We define all other hits + in terms of these three hits. The hits which are primitive are + - n-truncation + - the mapping cylinder + - general colimits + For each of the hits we add the following constants: + - the type formation + - the term and path constructors + - the dependent recursor + We add the computation rule for point constructors judgmentally to the kernel of Lean, and for the + path constructors (undecided). + + In this file we only define the dependent recursor. For the nondependent recursor and all other + uses of these hits, see the folder /hott/hit/ +-/ + constant trunc.{u} (n : trunc_index) (A : Type.{u}) : Type.{u} namespace trunc @@ -26,11 +43,11 @@ namespace trunc /-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 := + protected definition rec_on [reducible] {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} + definition rec_tr [reducible] {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 @@ -53,28 +70,28 @@ namespace cylinder (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 := + protected definition rec_on [reducible] {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} + definition rec_base [reducible] {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} + definition rec_top [reducible] {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} + definition rec_seg [reducible] {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 + --the sorry's in the statement can be removed when rec_base/rec_top are definitional sorry end cylinder @@ -88,7 +105,7 @@ structure diagram [class] := (dom cod : Ihom → Iob) (hom : Π(j : Ihom), ob (dom j) → ob (cod j)) end colimit -open eq colimit colimit.diagram +open colimit colimit.diagram constant colimit.{u v w} : diagram.{u v w} → Type.{max u v w} @@ -104,41 +121,22 @@ namespace colimit (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} + definition rec_incl [reducible] [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} + definition rec_cglue [reducible] [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 + --the sorry's in the statement can be removed when rec_incl is definitional sorry - protected definition rec_on [D : diagram] {P : colimit D → Type} (y : colimit D) + protected definition rec_on [reducible] [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