feat(hott): small changes, mostly in pointed2
This commit is contained in:
Floris van Doorn
Leonardo de Moura
parent
5810a4de8f
commit
b1ed69f621
15 changed files with 208 additions and 103 deletions
|
|
@ -23,18 +23,18 @@ namespace e_closure
|
|||
postfix `⁻¹ʳ`:(max+10) := e_closure.symm
|
||||
notation `[`:max a `]`:0 := e_closure.of_rel a
|
||||
notation `<`:max p `>`:0 := e_closure.of_path _ p
|
||||
abbreviation rfl {A : Type} {R : A → A → Type} {a : A} := of_path R (idpath a)
|
||||
abbreviation rfl [constructor] {A : Type} {R : A → A → Type} {a : A} := of_path R (idpath a)
|
||||
end e_closure
|
||||
open e_closure
|
||||
namespace relation
|
||||
|
||||
section
|
||||
parameters {A : Type}
|
||||
(R : A → A → Type)
|
||||
{R : A → A → Type}
|
||||
local abbreviation T := e_closure R
|
||||
|
||||
variables ⦃a a' a'' : A⦄ {s : R a a'} {r : T a a} {B C : Type}
|
||||
parameter {R}
|
||||
|
||||
protected definition e_closure.elim [unfold 8] {f : A → B}
|
||||
(e : Π⦃a a' : A⦄, R a a' → f a = f a') (t : T a a') : f a = f a' :=
|
||||
begin
|
||||
|
|
|
|||
|
|
@ -47,7 +47,7 @@ namespace eq
|
|||
|
||||
definition phomotopy_group_pequiv [constructor] (n : ℕ) {A B : Type*} (H : A ≃* B)
|
||||
: π*[n] A ≃* π*[n] B :=
|
||||
ptrunc_pequiv_ptrunc 0 (iterated_loop_space_pequiv n H)
|
||||
ptrunc_pequiv_ptrunc 0 (loopn_pequiv_loopn n H)
|
||||
|
||||
definition phomotopy_group_pequiv_loop_ptrunc [constructor] (k : ℕ) (A : Type*) :
|
||||
π*[k] A ≃* Ω[k] (ptrunc k A) :=
|
||||
|
|
|
|||
16
hott/book.md
16
hott/book.md
|
|
@ -20,9 +20,9 @@ The rows indicate the chapters, the columns the sections.
|
|||
| Ch 3 | + | + | + | + | ½ | + | + | + | + | . | + | | | | |
|
||||
| Ch 4 | - | + | + | + | . | + | + | + | + | | | | | | |
|
||||
| Ch 5 | - | . | ½ | - | - | . | . | ½ | | | | | | | |
|
||||
| Ch 6 | . | + | + | + | + | ½ | ½ | + | ¾ | ¼ | ¾ | + | . | | |
|
||||
| Ch 6 | . | + | + | + | + | + | + | + | ¾ | ¼ | ¾ | + | . | | |
|
||||
| Ch 7 | + | + | + | - | ¾ | - | - | | | | | | | | |
|
||||
| Ch 8 | + | + | + | - | ¾ | ¼ | - | - | - | - | | | | | |
|
||||
| Ch 8 | + | + | + | - | ¾ | ¼ | - | - | ½ | - | | | | | |
|
||||
| Ch 9 | ¾ | + | + | ½ | ¾ | ½ | - | - | - | | | | | | |
|
||||
| Ch 10 | - | - | - | - | - | | | | | | | | | | |
|
||||
| Ch 11 | - | - | - | - | - | - | | | | | | | | | |
|
||||
|
|
@ -99,25 +99,29 @@ Chapter 4: Equivalences
|
|||
Chapter 5: Induction
|
||||
---------
|
||||
|
||||
Lean has support for inductive families, but not for induction-induction or induction-recursion.
|
||||
|
||||
- 5.1 (Introduction to inductive types): not formalized
|
||||
- 5.2 (Uniqueness of inductive types): no formalizable content
|
||||
- 5.3 (W-types): [types.W](types/W.hlean) defines W-types.
|
||||
- 5.4 (Inductive types are initial algebras): not formalized
|
||||
- 5.5 (Homotopy-inductive types): not formalized
|
||||
- 5.6 (The general syntax of inductive definitions): no formalizable content
|
||||
- 5.7 (Generalizations of inductive types): no formalizable content. Lean has inductive families and mutual induction, but no induction-induction or induction-recursion
|
||||
- 5.7 (Generalizations of inductive types): no formalizable content.
|
||||
- 5.8 (Identity types and identity systems): 5.8.1-5.8.4 not formalized, 5.8.5 in [init.ua](init/ua.hlean) and 5.8.6 in [init.funext](init/funext.hlean)
|
||||
|
||||
Chapter 6: Higher inductive types
|
||||
---------
|
||||
|
||||
We have two primitive HITs in Lean, the computation rules are manually added to the Lean-HoTT kernel. The primitive HITs are the n-truncation and the quotient (not to be confused with the set-quotient). See [init.hit](init/hit.hlean).
|
||||
|
||||
- 6.1 (Introduction): no formalizable content
|
||||
- 6.2 (Induction principles and dependent paths): dependent paths in [init.pathover](init/pathover.hlean), circle in [homotopy.circle](homotopy/circle.hlean)
|
||||
- 6.3 (The interval): [homotopy.interval](homotopy/interval.hlean)
|
||||
- 6.4 (Circles and spheres): [homotopy.sphere](homotopy/sphere.hlean) and [homotopy.circle](homotopy/circle.hlean)
|
||||
- 6.5 (Suspensions): [homotopy.suspension](homotopy/susp.hlean) (we define the circle to be the suspension of bool, but Lemma 6.5.1 is similar to proving the ordinary induction principle for the circle in [homotopy.circle](homotopy/circle.hlean)) and a bit in [homotopy.sphere](homotopy/sphere.hlean) and [types.pointed](types/pointed.hlean)
|
||||
- 6.6 (Cell complexes): we define the torus using the quotient, see [hit.two_quotient](hit/two_quotient.hlean) and [homotopy.torus](homotopy/torus.hlean) (no dependent eliminator defined yet)
|
||||
- 6.7 (Hubs and spokes): [hit.two_quotient](hit/two_quotient.hlean) and [homotopy.torus](homotopy/torus.hlean) (no dependent eliminator defined yet)
|
||||
- 6.6 (Cell complexes): We define the torus using a two quotient, which in turn is defined in terms of the quotient, see [homotopy.torus](homotopy/torus.hlean).
|
||||
- 6.7 (Hubs and spokes): We define the two quotient using only the quotient in [hit.two_quotient](hit/two_quotient.hlean). This is slightly different than what is done in section 6.7, because the HIT in section 6.7 is not a quotient.
|
||||
- 6.8 (Pushouts): [hit.pushout](hit/pushout.hlean). Some of the "standard homotopy-theoretic constructions" have separate files, although not all of them have been defined explicitly yet
|
||||
- 6.9 (Truncations): [hit.trunc](hit/trunc.hlean) (except Lemma 6.9.3)
|
||||
- 6.10 (Quotients): [hit.set_quotient](hit/set_quotient.hlean) (up to 6.10.3). We define integers differently, to make them compute, in the folder [types.int](types/int/int.md). 6.10.13 is in [types.int.hott](types/int/hott.hlean)
|
||||
|
|
@ -149,7 +153,7 @@ Every file is in the folder [homotopy](homotopy/homotopy.md)
|
|||
- 8.6 (The Freudenthal suspension theorem): [connectedness](homotopy/connectedness.hlean) (Lemma 8.6.1), [wedge](homotopy/wedge.hlean) (Wedge connectivity, Lemma 8.6.2), the rest is not formalized
|
||||
- 8.7 (The van Kampen theorem): not formalized
|
||||
- 8.8 (Whitehead’s theorem and Whitehead’s principle): not formalized
|
||||
- 8.9 (A general statement of the encode-decode method): not formalized
|
||||
- 8.9 (A general statement of the encode-decode method): One variation of the encode-decode method is in [types.eq](types/eq.hlean).
|
||||
- 8.10 (Additional Results): not formalized
|
||||
|
||||
Chapter 9: Category theory
|
||||
|
|
|
|||
|
|
@ -332,7 +332,7 @@ namespace simple_two_quotient
|
|||
end
|
||||
end simple_two_quotient
|
||||
|
||||
attribute simple_two_quotient.j [constructor]
|
||||
attribute simple_two_quotient.j simple_two_quotient.incl0 [constructor]
|
||||
attribute simple_two_quotient.rec simple_two_quotient.elim [unfold 8] [recursor 8]
|
||||
--attribute simple_two_quotient.elim_type [unfold 9] -- TODO
|
||||
attribute simple_two_quotient.rec_on simple_two_quotient.elim_on [unfold 5]
|
||||
|
|
|
|||
|
|
@ -164,7 +164,7 @@ namespace circle
|
|||
|
||||
theorem elim_type_loop (Pbase : Type) (Ploop : Pbase ≃ Pbase) :
|
||||
transport (circle.elim_type Pbase Ploop) loop = Ploop :=
|
||||
by rewrite [tr_eq_cast_ap_fn,↑circle.elim_type,circle.elim_loop];apply cast_ua_fn
|
||||
by rewrite [tr_eq_cast_ap_fn,↑circle.elim_type,elim_loop];apply cast_ua_fn
|
||||
|
||||
theorem elim_type_loop_inv (Pbase : Type) (Ploop : Pbase ≃ Pbase) :
|
||||
transport (circle.elim_type Pbase Ploop) loop⁻¹ = to_inv Ploop :=
|
||||
|
|
@ -182,6 +182,40 @@ attribute circle.rec_on circle.elim_on [unfold 2]
|
|||
attribute circle.elim_type_on [unfold 1]
|
||||
|
||||
namespace circle
|
||||
open sigma
|
||||
/- universal property of the circle -/
|
||||
definition circle_pi_equiv [constructor] (P : S¹ → Type)
|
||||
: (Π(x : S¹), P x) ≃ Σ(p : P base), p =[loop] p :=
|
||||
begin
|
||||
fapply equiv.MK,
|
||||
{ intro f, exact ⟨f base, apdo f loop⟩},
|
||||
{ intro v x, induction v with p q, induction x,
|
||||
{ exact p},
|
||||
{ exact q}},
|
||||
{ intro v, induction v with p q, fapply sigma_eq,
|
||||
{ reflexivity},
|
||||
{ esimp, apply pathover_idp_of_eq, apply rec_loop}},
|
||||
{ intro f, apply eq_of_homotopy, intro x, induction x,
|
||||
{ reflexivity},
|
||||
{ apply eq_pathover_dep, apply hdeg_squareover, esimp, apply rec_loop}}
|
||||
end
|
||||
|
||||
definition circle_arrow_equiv [constructor] (P : Type)
|
||||
: (S¹ → P) ≃ Σ(p : P), p = p :=
|
||||
begin
|
||||
fapply equiv.MK,
|
||||
{ intro f, exact ⟨f base, ap f loop⟩},
|
||||
{ intro v x, induction v with p q, induction x,
|
||||
{ exact p},
|
||||
{ exact q}},
|
||||
{ intro v, induction v with p q, fapply sigma_eq,
|
||||
{ reflexivity},
|
||||
{ esimp, apply pathover_idp_of_eq, apply elim_loop}},
|
||||
{ intro f, apply eq_of_homotopy, intro x, induction x,
|
||||
{ reflexivity},
|
||||
{ apply eq_pathover, apply hdeg_square, esimp, apply elim_loop}}
|
||||
end
|
||||
|
||||
definition pointed_circle [instance] [constructor] : pointed S¹ :=
|
||||
pointed.mk base
|
||||
|
||||
|
|
|
|||
|
|
@ -265,4 +265,17 @@ namespace is_conn
|
|||
[H : is_conn_fun n f] : trunc n A ≃ trunc n B :=
|
||||
equiv.mk (trunc_functor n f) (is_equiv_trunc_functor_of_is_conn_fun n f)
|
||||
|
||||
definition is_conn_fun_trunc_functor {n k : ℕ₋₂} {A B : Type} (f : A → B) (H : k ≤ n)
|
||||
[H2 : is_conn_fun k f] : is_conn_fun k (trunc_functor n f) :=
|
||||
begin
|
||||
apply is_conn_fun.intro,
|
||||
intro P, have Πb, is_trunc n (P b), from (λb, is_trunc_of_le _ H),
|
||||
fconstructor,
|
||||
{ intro f' b,
|
||||
induction b with b,
|
||||
refine is_conn_fun.elim k H2 _ _ b, intro a, exact f' (tr a)},
|
||||
{ intro f', apply eq_of_homotopy, intro a,
|
||||
induction a with a, esimp, rewrite [is_conn_fun.elim_β]}
|
||||
end
|
||||
|
||||
end is_conn
|
||||
|
|
|
|||
|
|
@ -68,10 +68,10 @@ namespace is_equiv
|
|||
parameters {A B : Type} (f : A → B) (g : B → A)
|
||||
(ret : Πb, f (g b) = b) (sec : Πa, g (f a) = a)
|
||||
|
||||
private definition adjointify_left_inv' (a : A) : g (f a) = a :=
|
||||
definition adjointify_left_inv' (a : A) : g (f a) = a :=
|
||||
ap g (ap f (inverse (sec a))) ⬝ ap g (ret (f a)) ⬝ sec a
|
||||
|
||||
private theorem adjointify_adj' (a : A) : ret (f a) = ap f (adjointify_left_inv' a) :=
|
||||
theorem adjointify_adj' (a : A) : ret (f a) = ap f (adjointify_left_inv' a) :=
|
||||
let fgretrfa := ap f (ap g (ret (f a))) in
|
||||
let fgfinvsect := ap f (ap g (ap f (sec a)⁻¹)) in
|
||||
let fgfa := f (g (f a)) in
|
||||
|
|
|
|||
|
|
@ -28,18 +28,18 @@ open is_trunc eq
|
|||
uses of these hits, see the folder ../hit/
|
||||
-/
|
||||
|
||||
constant trunc.{u} (n : trunc_index) (A : Type.{u}) : Type.{u}
|
||||
constant trunc.{u} (n : ℕ₋₂) (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)
|
||||
constant tr {n : ℕ₋₂} {A : Type} (a : A) : trunc n A
|
||||
constant is_trunc_trunc (n : ℕ₋₂) (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}
|
||||
protected constant rec {n : ℕ₋₂} {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 [reducible] {n : trunc_index} {A : Type}
|
||||
protected definition rec_on [reducible] {n : ℕ₋₂} {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
|
||||
|
|
@ -68,7 +68,7 @@ end quotient
|
|||
init_hits -- Initialize builtin computational rules for trunc and quotient
|
||||
|
||||
namespace trunc
|
||||
definition rec_tr [reducible] {n : trunc_index} {A : Type} {P : trunc n A → Type}
|
||||
definition rec_tr [reducible] {n : ℕ₋₂} {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 :=
|
||||
idp
|
||||
end trunc
|
||||
|
|
|
|||
|
|
@ -144,8 +144,8 @@ definition repeat1 (t : tactic) : tactic := and_then t (repeat t)
|
|||
definition focus (t : tactic) : tactic := focus_at t 0
|
||||
definition determ (t : tactic) : tactic := at_most t 1
|
||||
definition trivial : tactic := or_else (apply eq.refl) assumption
|
||||
definition do (n : num) (t : tactic) : tactic :=
|
||||
nat.rec id (λn t', and_then t t') (nat.of_num n)
|
||||
definition do (n : nat) (t : tactic) : tactic :=
|
||||
nat.rec id (λn t', and_then t t') n
|
||||
|
||||
end tactic
|
||||
tactic_infixl `;`:15 := tactic.and_then
|
||||
|
|
|
|||
|
|
@ -23,7 +23,8 @@ open trunc_index
|
|||
|
||||
/-
|
||||
notation for trunc_index is -2, -1, 0, 1, ...
|
||||
from 0 and up this comes from a coercion from num to trunc_index (via ℕ)
|
||||
from 0 and up this comes from the way numerals are parsed in Lean.
|
||||
Any structure with a 0, a 1, and a + have numerals defined in them.
|
||||
-/
|
||||
|
||||
notation `ℕ₋₂` := trunc_index -- input using \N-2
|
||||
|
|
|
|||
|
|
@ -539,6 +539,13 @@ namespace pointed
|
|||
{ refine ap1_phomotopy IH ⬝* _, apply ap1_compose}
|
||||
end
|
||||
|
||||
definition apn_pid [constructor] {A : Type*} (n : ℕ) : apn n (pid A) ~* pid (Ω[n] A) :=
|
||||
begin
|
||||
induction n with n IH,
|
||||
{ reflexivity},
|
||||
{ exact ap1_phomotopy IH ⬝* ap1_id}
|
||||
end
|
||||
|
||||
theorem apn_con (n : ℕ) (f : A →* B) (p q : Ω[n+1] A)
|
||||
: apn (n+1) f (p ⬝ q) = apn (n+1) f p ⬝ apn (n+1) f q :=
|
||||
by rewrite [+apn_succ, ap1_con]
|
||||
|
|
|
|||
|
|
@ -11,10 +11,6 @@ import .equiv cubical.square
|
|||
|
||||
open eq is_equiv equiv pointed is_trunc
|
||||
|
||||
-- structure pequiv (A B : Type*) :=
|
||||
-- (to_pmap : A →* B)
|
||||
-- (is_equiv_to_pmap : is_equiv to_pmap)
|
||||
|
||||
structure pequiv (A B : Type*) extends equiv A B, pmap A B
|
||||
|
||||
namespace pointed
|
||||
|
|
@ -36,7 +32,7 @@ namespace pointed
|
|||
definition pequiv_of_equiv [constructor] (f : A ≃ B) (H : f pt = pt) : A ≃* B :=
|
||||
pequiv.mk f _ H
|
||||
|
||||
protected definition pequiv.MK [constructor] (f : A →* B) (g : B →* A)
|
||||
protected definition pequiv.MK [constructor] (f : A →* B) (g : B → A)
|
||||
(gf : Πa, g (f a) = a) (fg : Πb, f (g b) = b) : A ≃* B :=
|
||||
pequiv.mk f (adjointify f g fg gf) (respect_pt f)
|
||||
|
||||
|
|
@ -44,7 +40,34 @@ namespace pointed
|
|||
equiv.mk f _
|
||||
|
||||
definition to_pinv [constructor] (f : A ≃* B) : B →* A :=
|
||||
pmap.mk f⁻¹ ((ap f⁻¹ (respect_pt f))⁻¹ ⬝ !left_inv)
|
||||
pmap.mk f⁻¹ ((ap f⁻¹ (respect_pt f))⁻¹ ⬝ left_inv f pt)
|
||||
|
||||
/- A version of pequiv.MK with stronger conditions.
|
||||
The advantage of defining a pointed equivalence with this definition is that there is a
|
||||
pointed homotopy between the inverse of the resulting equivalence and the given pointed map g.
|
||||
This is not the case when using `pequiv.MK` (if g is a pointed map),
|
||||
that will only give an ordinary homotopy.
|
||||
-/
|
||||
protected definition pequiv.MK2 [constructor] (f : A →* B) (g : B →* A)
|
||||
(gf : g ∘* f ~* !pid) (fg : f ∘* g ~* !pid) : A ≃* B :=
|
||||
pequiv.MK f g gf fg
|
||||
|
||||
definition to_pmap_pequiv_MK2 [constructor] (f : A →* B) (g : B →* A)
|
||||
(gf : g ∘* f ~* !pid) (fg : f ∘* g ~* !pid) : pequiv.MK2 f g gf fg ~* f :=
|
||||
phomotopy.mk (λb, idp) !idp_con
|
||||
|
||||
definition to_pinv_pequiv_MK2 [constructor] (f : A →* B) (g : B →* A)
|
||||
(gf : g ∘* f ~* !pid) (fg : f ∘* g ~* !pid) : to_pinv (pequiv.MK2 f g gf fg) ~* g :=
|
||||
phomotopy.mk (λb, idp)
|
||||
abstract [irreducible] begin
|
||||
esimp, unfold [adjointify_left_inv'],
|
||||
note H := to_homotopy_pt gf, note H2 := to_homotopy_pt fg,
|
||||
note H3 := eq_top_of_square (natural_square_tr (to_homotopy fg) (respect_pt f)),
|
||||
rewrite [▸* at *, H, H3, H2, ap_id, - +con.assoc, ap_compose' f g, con_inv,
|
||||
- ap_inv, - +ap_con g],
|
||||
apply whisker_right, apply ap02 g,
|
||||
rewrite [ap_con, - + con.assoc, +ap_inv, +inv_con_cancel_right, con.left_inv],
|
||||
end end
|
||||
|
||||
definition pua {A B : Type*} (f : A ≃* B) : A = B :=
|
||||
pType_eq (equiv_of_pequiv f) !respect_pt
|
||||
|
|
@ -64,6 +87,13 @@ namespace pointed
|
|||
postfix `⁻¹ᵉ*`:(max + 1) := pequiv.symm
|
||||
infix ` ⬝e* `:75 := pequiv.trans
|
||||
|
||||
definition pequiv_change_fun [constructor] (f : A ≃* B) (f' : A →* B) (Heq : f ~ f') : A ≃* B :=
|
||||
pequiv_of_pmap f' (is_equiv.homotopy_closed f Heq)
|
||||
|
||||
definition pequiv_change_inv [constructor] (f : A ≃* B) (f' : B →* A) (Heq : to_pinv f ~ f')
|
||||
: A ≃* B :=
|
||||
pequiv.MK f f' (to_left_inv (equiv_change_inv f Heq)) (to_right_inv (equiv_change_inv f Heq))
|
||||
|
||||
definition pequiv_rect' (f : A ≃* B) (P : A → B → Type)
|
||||
(g : Πb, P (f⁻¹ b) b) (a : A) : P a (f a) :=
|
||||
left_inv f a ▸ g (f a)
|
||||
|
|
@ -83,26 +113,12 @@ namespace pointed
|
|||
definition peap {A B : Type*} (F : Type* → Type*) (p : A ≃* B) : F A ≃* F B :=
|
||||
pequiv_of_pmap (pcast (ap F (eq_of_pequiv p))) begin cases eq_of_pequiv p, apply is_equiv_id end
|
||||
|
||||
definition loop_space_pequiv [constructor] (p : A ≃* B) : Ω A ≃* Ω B :=
|
||||
pequiv_of_pmap (ap1 p) (is_equiv_ap1 p)
|
||||
|
||||
definition iterated_loop_space_pequiv [constructor] (n : ℕ) (p : A ≃* B) : Ω[n] A ≃* Ω[n] B :=
|
||||
pequiv_of_pmap (apn n p) (is_equiv_apn n p)
|
||||
|
||||
definition pequiv_eq {p q : A ≃* B} (H : p = q :> (A →* B)) : p = q :=
|
||||
begin
|
||||
cases p with f Hf, cases q with g Hg, esimp at *,
|
||||
exact apd011 pequiv_of_pmap H !is_prop.elim
|
||||
end
|
||||
|
||||
definition loop_space_pequiv_rfl
|
||||
: loop_space_pequiv (@pequiv.refl A) = @pequiv.refl (Ω A) :=
|
||||
begin
|
||||
apply pequiv_eq, fapply pmap_eq: esimp,
|
||||
{ intro p, exact !idp_con ⬝ !ap_id},
|
||||
{ reflexivity}
|
||||
end
|
||||
|
||||
infix ` ⬝e*p `:75 := peconcat_eq
|
||||
infix ` ⬝pe* `:75 := eq_peconcat
|
||||
|
||||
|
|
@ -195,33 +211,50 @@ namespace pointed
|
|||
|
||||
/- pointed equivalences between particular pointed types -/
|
||||
|
||||
definition loop_pequiv_loop [constructor] (f : A ≃* B) : Ω A ≃* Ω B :=
|
||||
pequiv.MK (ap1 f) (ap1 f⁻¹ᵉ*)
|
||||
definition loopn_pequiv_loopn [constructor] (n : ℕ) (f : A ≃* B) : Ω[n] A ≃* Ω[n] B :=
|
||||
pequiv.MK2 (apn n f) (apn n f⁻¹ᵉ*)
|
||||
abstract begin
|
||||
intro p,
|
||||
refine ((ap1_compose f⁻¹ᵉ* f) p)⁻¹ ⬝ _,
|
||||
refine ap1_phomotopy (pleft_inv f) p ⬝ _,
|
||||
exact ap1_id p
|
||||
induction n with n IH,
|
||||
{ apply pleft_inv},
|
||||
{ replace nat.succ n with n + 1,
|
||||
rewrite [+apn_succ],
|
||||
refine !ap1_compose⁻¹* ⬝* _,
|
||||
refine ap1_phomotopy IH ⬝* _,
|
||||
apply ap1_id}
|
||||
end end
|
||||
abstract begin
|
||||
intro p,
|
||||
refine ((ap1_compose f f⁻¹ᵉ*) p)⁻¹ ⬝ _,
|
||||
refine ap1_phomotopy (pright_inv f) p ⬝ _,
|
||||
exact ap1_id p
|
||||
induction n with n IH,
|
||||
{ apply pright_inv},
|
||||
{ replace nat.succ n with n + 1,
|
||||
rewrite [+apn_succ],
|
||||
refine !ap1_compose⁻¹* ⬝* _,
|
||||
refine ap1_phomotopy IH ⬝* _,
|
||||
apply ap1_id}
|
||||
end end
|
||||
|
||||
definition loopn_pequiv_loopn (n : ℕ) (f : A ≃* B) : Ω[n] A ≃* Ω[n] B :=
|
||||
begin
|
||||
induction n with n IH,
|
||||
{ exact f},
|
||||
{ exact loop_pequiv_loop IH}
|
||||
end
|
||||
definition loop_pequiv_loop [constructor] (f : A ≃* B) : Ω A ≃* Ω B :=
|
||||
loopn_pequiv_loopn 1 f
|
||||
|
||||
definition to_pmap_loopn_pequiv_loopn [constructor] (n : ℕ) (f : A ≃* B)
|
||||
: loopn_pequiv_loopn n f ~* apn n f :=
|
||||
!to_pmap_pequiv_MK2
|
||||
|
||||
definition to_pinv_loopn_pequiv_loopn [constructor] (n : ℕ) (f : A ≃* B)
|
||||
: (loopn_pequiv_loopn n f)⁻¹ᵉ* ~* apn n f⁻¹ᵉ* :=
|
||||
!to_pinv_pequiv_MK2
|
||||
|
||||
definition loopn_pequiv_loopn_con (n : ℕ) (f : A ≃* B) (p q : Ω[n+1] A)
|
||||
: loopn_pequiv_loopn (n+1) f (p ⬝ q) =
|
||||
loopn_pequiv_loopn (n+1) f p ⬝ loopn_pequiv_loopn (n+1) f q :=
|
||||
ap1_con (loopn_pequiv_loopn n f) p q
|
||||
|
||||
definition loopn_pequiv_loopn_rfl (n : ℕ) :
|
||||
loopn_pequiv_loopn n (@pequiv.refl A) = @pequiv.refl (Ω[n] A) :=
|
||||
begin
|
||||
apply pequiv_eq, apply eq_of_phomotopy,
|
||||
exact !to_pmap_loopn_pequiv_loopn ⬝* apn_pid n,
|
||||
end
|
||||
|
||||
definition pmap_functor [constructor] {A A' B B' : Type*} (f : A' →* A) (g : B →* B') :
|
||||
ppmap A B →* ppmap A' B' :=
|
||||
pmap.mk (λh, g ∘* h ∘* f)
|
||||
|
|
|
|||
|
|
@ -393,6 +393,18 @@ namespace sigma
|
|||
{ intro v, induction v with a p, induction p: reflexivity},
|
||||
end
|
||||
|
||||
definition sigma_sigma_eq_right {A : Type} (a : A) (P : Π(b : A), a = b → Type)
|
||||
: (Σ(b : A) (p : a = b), P b p) ≃ P a idp :=
|
||||
calc
|
||||
(Σ(b : A) (p : a = b), P b p) ≃ (Σ(v : Σ(b : A), a = b), P v.1 v.2) : sigma_assoc_equiv
|
||||
... ≃ P a idp : !sigma_equiv_of_is_contr_left
|
||||
|
||||
definition sigma_sigma_eq_left {A : Type} (a : A) (P : Π(b : A), b = a → Type)
|
||||
: (Σ(b : A) (p : b = a), P b p) ≃ P a idp :=
|
||||
calc
|
||||
(Σ(b : A) (p : b = a), P b p) ≃ (Σ(v : Σ(b : A), b = a), P v.1 v.2) : sigma_assoc_equiv
|
||||
... ≃ P a idp : !sigma_equiv_of_is_contr_left
|
||||
|
||||
/- ** Universal mapping properties -/
|
||||
/- *** The positive universal property. -/
|
||||
|
||||
|
|
|
|||
|
|
@ -13,6 +13,7 @@ import .pointed2 ..function algebra.order types.nat.order
|
|||
open eq sigma sigma.ops pi function equiv trunctype
|
||||
is_equiv prod pointed nat is_trunc algebra
|
||||
|
||||
/- basic computation with ℕ₋₂, its operations and its order -/
|
||||
namespace trunc_index
|
||||
|
||||
definition minus_one_le_succ (n : ℕ₋₂) : -1 ≤ n.+1 :=
|
||||
|
|
@ -203,26 +204,7 @@ namespace is_trunc
|
|||
|
||||
variables {A B : Type} {n : ℕ₋₂}
|
||||
|
||||
/- theorems about trunctype -/
|
||||
protected definition trunctype.sigma_char.{l} [constructor] (n : ℕ₋₂) :
|
||||
(trunctype.{l} n) ≃ (Σ (A : Type.{l}), is_trunc n A) :=
|
||||
begin
|
||||
fapply equiv.MK,
|
||||
{ intro A, exact (⟨carrier A, struct A⟩)},
|
||||
{ intro S, exact (trunctype.mk S.1 S.2)},
|
||||
{ intro S, induction S with S1 S2, reflexivity},
|
||||
{ intro A, induction A with A1 A2, reflexivity},
|
||||
end
|
||||
|
||||
definition trunctype_eq_equiv [constructor] (n : ℕ₋₂) (A B : n-Type) :
|
||||
(A = B) ≃ (carrier A = carrier B) :=
|
||||
calc
|
||||
(A = B) ≃ (to_fun (trunctype.sigma_char n) A = to_fun (trunctype.sigma_char n) B)
|
||||
: eq_equiv_fn_eq_of_equiv
|
||||
... ≃ ((to_fun (trunctype.sigma_char n) A).1 = (to_fun (trunctype.sigma_char n) B).1)
|
||||
: equiv.symm (!equiv_subtype)
|
||||
... ≃ (carrier A = carrier B) : equiv.refl
|
||||
|
||||
/- closure properties of truncatedness -/
|
||||
theorem is_trunc_is_embedding_closed (f : A → B) [Hf : is_embedding f] [HB : is_trunc n B]
|
||||
(Hn : -1 ≤ n) : is_trunc n A :=
|
||||
begin
|
||||
|
|
@ -254,13 +236,31 @@ namespace is_trunc
|
|||
definition is_embedding_to_fun (A B : Type) : is_embedding (@to_fun A B) :=
|
||||
λf f', !is_equiv_ap_to_fun
|
||||
|
||||
/- theorems about trunctype -/
|
||||
protected definition trunctype.sigma_char.{l} [constructor] (n : ℕ₋₂) :
|
||||
(trunctype.{l} n) ≃ (Σ (A : Type.{l}), is_trunc n A) :=
|
||||
begin
|
||||
fapply equiv.MK,
|
||||
{ intro A, exact (⟨carrier A, struct A⟩)},
|
||||
{ intro S, exact (trunctype.mk S.1 S.2)},
|
||||
{ intro S, induction S with S1 S2, reflexivity},
|
||||
{ intro A, induction A with A1 A2, reflexivity},
|
||||
end
|
||||
|
||||
definition trunctype_eq_equiv [constructor] (n : ℕ₋₂) (A B : n-Type) :
|
||||
(A = B) ≃ (carrier A = carrier B) :=
|
||||
calc
|
||||
(A = B) ≃ (to_fun (trunctype.sigma_char n) A = to_fun (trunctype.sigma_char n) B)
|
||||
: eq_equiv_fn_eq_of_equiv
|
||||
... ≃ ((to_fun (trunctype.sigma_char n) A).1 = (to_fun (trunctype.sigma_char n) B).1)
|
||||
: equiv.symm (!equiv_subtype)
|
||||
... ≃ (carrier A = carrier B) : equiv.refl
|
||||
|
||||
theorem is_trunc_trunctype [instance] (n : ℕ₋₂) : is_trunc n.+1 (n-Type) :=
|
||||
begin
|
||||
apply is_trunc_succ_intro, intro X Y,
|
||||
fapply is_trunc_equiv_closed,
|
||||
{ apply equiv.symm, apply trunctype_eq_equiv},
|
||||
fapply is_trunc_equiv_closed,
|
||||
{ apply equiv.symm, apply eq_equiv_equiv},
|
||||
fapply is_trunc_equiv_closed_rev, { apply trunctype_eq_equiv},
|
||||
fapply is_trunc_equiv_closed_rev, { apply eq_equiv_equiv},
|
||||
induction n,
|
||||
{ apply @is_contr_of_inhabited_prop,
|
||||
{ apply is_trunc_is_embedding_closed,
|
||||
|
|
@ -272,7 +272,6 @@ namespace is_trunc
|
|||
{ apply minus_one_le_succ}}
|
||||
end
|
||||
|
||||
|
||||
/- theorems about decidable equality and axiom K -/
|
||||
theorem is_set_of_axiom_K {A : Type} (K : Π{a : A} (p : a = a), p = idp) : is_set A :=
|
||||
is_set.mk _ (λa b p q, eq.rec K q p)
|
||||
|
|
@ -413,6 +412,7 @@ namespace trunc
|
|||
: (tr a = tr a' :> trunc n.+1 A) ≃ trunc n (a = a') :=
|
||||
!trunc_eq_equiv
|
||||
|
||||
/- encode preserves concatenation -/
|
||||
definition trunc_functor2 [unfold 6 7] {n : ℕ₋₂} {A B C : Type} (f : A → B → C)
|
||||
(x : trunc n A) (y : trunc n B) : trunc n C :=
|
||||
by induction x with a; induction y with b; exact tr (f a b)
|
||||
|
|
@ -425,8 +425,7 @@ namespace trunc
|
|||
(g : trunc.code n aa₁ aa₂) (h : trunc.code n aa₂ aa₃) : trunc.code n aa₁ aa₃ :=
|
||||
begin
|
||||
induction aa₁ with a₁, induction aa₂ with a₂, induction aa₃ with a₃,
|
||||
esimp at *, induction g with p, induction h with q,
|
||||
exact tr (p ⬝ q)
|
||||
esimp at *, apply trunc_concat g h,
|
||||
end
|
||||
|
||||
definition encode_con' {n : ℕ₋₂} {aa₁ aa₂ aa₃ : trunc n.+1 A} (p : aa₁ = aa₂) (q : aa₂ = aa₃)
|
||||
|
|
@ -440,6 +439,22 @@ namespace trunc
|
|||
: trunc.encode (p ⬝ q) = trunc_concat (trunc.encode p) (trunc.encode q) :=
|
||||
encode_con' p q
|
||||
|
||||
/- the principle of unique choice -/
|
||||
definition unique_choice {P : A → Type} [H : Πa, is_prop (P a)] (f : Πa, ∥ P a ∥) (a : A)
|
||||
: P a :=
|
||||
!trunc_equiv (f a)
|
||||
|
||||
/- transport over a truncated family -/
|
||||
definition trunc_transport {a a' : A} {P : A → Type} (p : a = a') (n : ℕ₋₂) (x : P a)
|
||||
: transport (λa, trunc n (P a)) p (tr x) = tr (p ▸ x) :=
|
||||
by induction p; reflexivity
|
||||
|
||||
/- pathover over a truncated family -/
|
||||
definition trunc_pathover {A : Type} {B : A → Type} {n : ℕ₋₂} {a a' : A} {p : a = a'}
|
||||
{b : B a} {b' : B a'} (q : b =[p] b') : @tr n _ b =[p] @tr n _ b' :=
|
||||
by induction q; constructor
|
||||
|
||||
/- truncations preserve truncatedness -/
|
||||
definition is_trunc_trunc_of_is_trunc [instance] [priority 500] (A : Type)
|
||||
(n m : ℕ₋₂) [H : is_trunc n A] : is_trunc n (trunc m A) :=
|
||||
begin
|
||||
|
|
@ -456,20 +471,6 @@ namespace trunc
|
|||
{ exact (IH _ _ _)}}}
|
||||
end
|
||||
|
||||
definition unique_choice {P : A → Type} [H : Πa, is_prop (P a)] (f : Πa, ∥ P a ∥) (a : A)
|
||||
: P a :=
|
||||
!trunc_equiv (f a)
|
||||
|
||||
/- transport over a truncated family -/
|
||||
definition trunc_transport {a a' : A} {P : A → Type} (p : a = a') (n : ℕ₋₂) (x : P a)
|
||||
: transport (λa, trunc n (P a)) p (tr x) = tr (p ▸ x) :=
|
||||
by induction p; reflexivity
|
||||
|
||||
/- pathover over a truncated family -/
|
||||
definition trunc_pathover {A : Type} {B : A → Type} {n : ℕ₋₂} {a a' : A} {p : a = a'}
|
||||
{b : B a} {b' : B a'} (q : b =[p] b') : @tr n _ b =[p] @tr n _ b' :=
|
||||
by induction q; constructor
|
||||
|
||||
/- equivalences between truncated types (see also hit.trunc) -/
|
||||
definition trunc_trunc_equiv_left [constructor] (A : Type) (n m : ℕ₋₂) (H : n ≤ m)
|
||||
: trunc n (trunc m A) ≃ trunc n A :=
|
||||
|
|
@ -515,7 +516,6 @@ namespace trunc
|
|||
exact tr (fiber.mk (tr a) (ap tr p))}
|
||||
end
|
||||
|
||||
|
||||
/- the image of a map is the (-1)-truncated fiber -/
|
||||
definition image [constructor] {A B : Type} (f : A → B) (b : B) : Prop := ∥ fiber f b ∥
|
||||
|
||||
|
|
|
|||
|
|
@ -154,8 +154,9 @@ definition repeat1 (t : tactic) : tactic := and_then t (repeat t)
|
|||
definition focus (t : tactic) : tactic := focus_at t 0
|
||||
definition determ (t : tactic) : tactic := at_most t 1
|
||||
definition trivial : tactic := or_else (or_else (apply eq.refl) (apply true.intro)) assumption
|
||||
definition do (n : num) (t : tactic) : tactic :=
|
||||
nat.rec id (λn t', and_then t t') (nat.of_num n)
|
||||
definition do (n : nat) (t : tactic) : tactic :=
|
||||
nat.rec id (λn t', and_then t t') n
|
||||
|
||||
end tactic
|
||||
tactic_infixl `;`:15 := tactic.and_then
|
||||
tactic_notation T1 `:`:15 T2 := tactic.focus (tactic.and_then T1 (tactic.all_goals T2))
|
||||
|
|
|
|||
Loading…
Reference in a new issue