diff --git a/hott/book.md b/hott/book.md index ab946b6fa..e1dc967ec 100644 --- a/hott/book.md +++ b/hott/book.md @@ -17,7 +17,7 @@ The rows indicate the chapters, the columns the sections. |-------|---|---|---|---|---|---|---|---|---|----|----|----|----|----|----| | Ch 1 | . | . | . | . | + | + | + | + | + | . | + | + | | | | | Ch 2 | + | + | + | + | . | + | + | + | + | + | + | + | + | + | + | -| Ch 3 | + | - | + | + | ½ | + | + | - | ½ | . | + | | | | | +| Ch 3 | + | + | + | + | ½ | + | + | - | ½ | . | + | | | | | | Ch 4 | - | + | - | + | . | + | - | - | + | | | | | | | | Ch 5 | - | . | - | - | - | . | . | ½ | | | | | | | | | Ch 6 | . | + | + | + | + | ½ | ½ | ¼ | ¼ | ¼ | ¾ | - | . | | | @@ -69,8 +69,8 @@ Chapter 2: Homotopy type theory Chapter 3: Sets and logic --------- -- 3.1 (Sets and n-types): [init.trunc](init/trunc.hlean) -- 3.2 (Propositions as types?): not formalized +- 3.1 (Sets and n-types): [init.trunc](init/trunc.hlean). Example 3.1.9 in [types.univ](types/univ.hlean) +- 3.2 (Propositions as types?): [types.univ](types/univ.hlean) - 3.3 (Mere propositions): [init.trunc](init/trunc.hlean) and [hprop_trunc](hprop_trunc.hlean) (Lemma 3.3.5). - 3.4 (Classical vs. intuitionistic logic): decidable is defined in [init.logic](init/logic.hlean) - 3.5 (Subsets and propositional resizing): Lemma 3.5.1 is subtype_eq in [types.sigma](types/sigma.hlean), we don't have propositional resizing as axiom yet. diff --git a/hott/function.hlean b/hott/function.hlean index bf0bace4e..84429c647 100644 --- a/hott/function.hlean +++ b/hott/function.hlean @@ -26,6 +26,16 @@ structure is_retraction [class] (f : A → B) := (sect : B → A) (right_inverse : Π(b : B), f (sect b) = b) +definition is_weakly_constant [class] (f : A → B) (a a' : A) := f a = f a' + +structure is_constant [class] (f : A → B) := + (pt : B) + (eq : Π(a : A), f a = pt) + +structure conditionally_constant [class] (f : A → B) := + (g : ∥A∥ → B) + (eq : Π(a : A), f a = g (tr a)) + namespace function attribute is_embedding.elim [instance] diff --git a/hott/init/pathover.hlean b/hott/init/pathover.hlean index 4454334f4..1743cf300 100644 --- a/hott/init/pathover.hlean +++ b/hott/init/pathover.hlean @@ -205,6 +205,10 @@ namespace eq definition tr_pathover_of_eq (q : b₂ = b₂') : p⁻¹ ▸ b₂ =[p] b₂' := by cases q;apply tr_pathover + definition apo (f : Πa, B a → B' a) (Ha : a = a₂) (Hb : b =[Ha] b₂) + : f a b =[Ha] f a₂ b₂ := + by induction Hb; exact idpo + definition apo011 (f : Πa, B a → A') (Ha : a = a₂) (Hb : b =[Ha] b₂) : f a b = f a₂ b₂ := by cases Hb; exact idp @@ -217,8 +221,12 @@ namespace eq {b : B a} {b₂ : B a₂} (q : b =[p] b₂) : f b =[apo011 C p q] g b₂ := by cases r; apply (idp_rec_on q); exact idpo - definition apo10 {f : Πb, C a b} {g : Πb₂, C a₂ b₂} (r : f =[p] g) - {b : B a} : f b =[apo011 C p !pathover_tr] g (p ▸ b) := + definition apdo10 {f : Πb, C a b} {g : Πb₂, C a₂ b₂} (r : f =[p] g) + (b : B a) : f b =[apo011 C p !pathover_tr] g (p ▸ b) := + by cases r; exact idpo + + definition apo10 {f : B a → B' a} {g : B a₂ → B' a₂} (r : f =[p] g) + (b : B a) : f b =[p] g (p ▸ b) := by cases r; exact idpo definition cono.right_inv_eq (q : b = b') diff --git a/hott/types/bool.hlean b/hott/types/bool.hlean index bcc0d41bf..941672e55 100644 --- a/hott/types/bool.hlean +++ b/hott/types/bool.hlean @@ -13,7 +13,7 @@ namespace bool definition ff_ne_tt : ff = tt → empty | [none] - definition is_equiv_bnot [instance] [priority 500] : is_equiv bnot := + definition is_equiv_bnot [constructor] [instance] [priority 500] : is_equiv bnot := begin fapply is_equiv.mk, exact bnot, @@ -21,7 +21,11 @@ namespace bool -- all_goals (focus (intro b;cases b;all_goals reflexivity)), end - definition equiv_bnot : bool ≃ bool := equiv.mk bnot _ + definition bnot_ne : Π(b : bool), bnot b ≠ b + | bnot_ne tt := ff_ne_tt + | bnot_ne ff := ne.symm ff_ne_tt + + definition equiv_bnot [constructor] : bool ≃ bool := equiv.mk bnot _ definition eq_bnot : bool = bool := ua equiv_bnot definition eq_bnot_ne_idp : eq_bnot ≠ idp := diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean index a3841426d..eb7eb1fa4 100644 --- a/hott/types/pi.hlean +++ b/hott/types/pi.hlean @@ -228,6 +228,9 @@ namespace pi apply eq_equiv_homotopy end + definition is_trunc_not [instance] (n : trunc_index) (A : Type) : is_trunc (n.+1) ¬A := + by unfold not;exact _ + definition is_hprop_pi_eq [instance] [priority 490] (a : A) : is_hprop (Π(a' : A), a = a') := is_hprop_of_imp_is_contr ( assume (f : Πa', a = a'), diff --git a/hott/types/prod.hlean b/hott/types/prod.hlean index 696d4ab04..d9dc2dd70 100644 --- a/hott/types/prod.hlean +++ b/hott/types/prod.hlean @@ -9,11 +9,13 @@ Theorems about products open eq equiv is_equiv is_trunc prod prod.ops unit equiv.ops -variables {A A' B B' C D : Type} +variables {A A' B B' C D : Type} {P Q : A → Type} {a a' a'' : A} {b b₁ b₂ b' b'' : B} {u v w : A × B} namespace prod + /- Paths in a product space -/ + protected definition eta (u : A × B) : (pr₁ u, pr₂ u) = u := by cases u; apply idp @@ -23,8 +25,6 @@ namespace prod definition prod_eq [unfold 3 4 5 6] (H₁ : u.1 = v.1) (H₂ : u.2 = v.2) : u = v := by cases u; cases v; exact pair_eq H₁ H₂ - /- Projections of paths from a total space -/ - definition eq_pr1 (p : u = v) : u.1 = v.1 := ap pr1 p @@ -50,8 +50,7 @@ namespace prod definition prod_eq_eta (p : u = v) : prod_eq (p..1) (p..2) = p := by induction p; induction u; reflexivity - /- the uncurried version of prod_eq. We will prove that this is an equivalence -/ - + -- the uncurried version of prod_eq. We will prove that this is an equivalence definition prod_eq_unc (H : u.1 = v.1 × u.2 = v.2) : u = v := by cases H with H₁ H₂;exact prod_eq H₁ H₂ @@ -80,10 +79,29 @@ namespace prod /- Transport -/ - definition prod_transport {P Q : A → Type} {a a' : A} (p : a = a') (u : P a × Q a) + definition prod_transport (p : a = a') (u : P a × Q a) : p ▸ u = (p ▸ u.1, p ▸ u.2) := by induction p; induction u; reflexivity + /- Pathovers -/ + + definition etao (p : a = a') (bc : P a × Q a) : bc =[p] (p ▸ bc.1, p ▸ bc.2) := + by induction p; induction bc; apply idpo + + definition prod_pathover (p : a = a') (u : P a × Q a) (v : P a' × Q a') + (r : u.1 =[p] v.1) (s : u.2 =[p] v.2) : u =[p] v := + begin + induction u, induction v, esimp at *, induction r, + induction s using idp_rec_on, + apply idpo + end + + /- + TODO: + * define the projections from the type u =[p] v + * show that the uncurried version of prod_pathover is an equivalence + -/ + /- Functorial action -/ variables (f : A → A') (g : B → B') diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean index 75cc004c2..2ffb6e3c5 100644 --- a/hott/types/sigma.hlean +++ b/hott/types/sigma.hlean @@ -18,6 +18,8 @@ namespace sigma definition destruct := @sigma.cases_on + /- Paths in a sigma-type -/ + protected definition eta : Π (u : Σa, B a), ⟨u.1 , u.2⟩ = u | eta ⟨u₁, u₂⟩ := idp @@ -33,8 +35,6 @@ namespace sigma definition sigma_eq (p : u.1 = v.1) (q : u.2 =[p] v.2) : u = v := by induction u; induction v; exact (dpair_eq_dpair p q) - /- Projections of paths from a total space -/ - definition eq_pr1 (p : u = v) : u.1 = v.1 := ap pr1 p @@ -176,7 +176,7 @@ namespace sigma /- Pathovers -/ - definition eta_pathover (p : a = a') (bc : Σ(b : B a), C a b) + definition etao (p : a = a') (bc : Σ(b : B a), C a b) : bc =[p] ⟨p ▸ bc.1, p ▸D bc.2⟩ := by induction p; induction bc; apply idpo @@ -187,7 +187,8 @@ namespace sigma esimp [apo011] at s, induction s using idp_rec_on, apply idpo end - /- TODO: + /- + TODO: * define the projections from the type u =[p] v * show that the uncurried version of sigma_pathover is an equivalence -/ diff --git a/hott/types/sum.hlean b/hott/types/sum.hlean index 7f64c4b9b..eab5f15e2 100644 --- a/hott/types/sum.hlean +++ b/hott/types/sum.hlean @@ -9,8 +9,8 @@ Theorems about sums/coproducts/disjoint unions open lift eq is_equiv equiv equiv.ops prod prod.ops is_trunc sigma bool namespace sum - universe variables u v - variables {A : Type.{u}} {B : Type.{v}} (z z' : A + B) + universe variables u v u' v' + variables {A : Type.{u}} {B : Type.{v}} (z z' : A + B) {P : A → Type.{u'}} {Q : A → Type.{v'}} protected definition eta : sum.rec inl inr z = z := by induction z; all_goals reflexivity @@ -53,16 +53,60 @@ namespace sum definition empty_of_inl_eq_inr (p : inl a = inr b) : empty := down (sum.encode p) definition empty_of_inr_eq_inl (p : inr b = inl a) : empty := down (sum.encode p) - definition sum_transport {P Q : A → Type} (p : a = a') (z : P a + Q a) + /- Transport -/ + + definition sum_transport (p : a = a') (z : P a + Q a) : p ▸ z = sum.rec (λa, inl (p ▸ a)) (λb, inr (p ▸ b)) z := by induction p; induction z; all_goals reflexivity + + /- Pathovers -/ + + definition etao (p : a = a') (z : P a + Q a) + : z =[p] sum.rec (λa, inl (p ▸ a)) (λb, inr (p ▸ b)) z := + by induction p; induction z; all_goals constructor + + protected definition codeo (p : a = a') : P a + Q a → P a' + Q a' → Type.{max u' v'} + | codeo (inl x) (inl x') := lift.{u' v'} (x =[p] x') + | codeo (inr y) (inr y') := lift.{v' u'} (y =[p] y') + | codeo _ _ := lift empty + + protected definition decodeo (p : a = a') : Π(z : P a + Q a) (z' : P a' + Q a'), + sum.codeo p z z' → z =[p] z' + | decodeo (inl x) (inl x') := λc, apo (λa, inl) p (down c) + | decodeo (inl x) (inr y') := λc, empty.elim (down c) _ + | decodeo (inr y) (inl x') := λc, empty.elim (down c) _ + | decodeo (inr y) (inr y') := λc, apo (λa, inr) p (down c) + + variables {z z'} + protected definition encodeo {p : a = a'} {z : P a + Q a} {z' : P a' + Q a'} (q : z =[p] z') + : sum.codeo p z z' := + by induction q; induction z; all_goals exact up idpo + + variables (z z') + definition sum_pathover_equiv [constructor] (p : a = a') (z : P a + Q a) (z' : P a' + Q a') + : (z =[p] z') ≃ sum.codeo p z z' := + equiv.MK sum.encodeo + !sum.decodeo + abstract begin + intro c, induction z with a b, all_goals induction z' with a' b', + all_goals (esimp at *; induction c with c), + all_goals induction c, -- c either has type empty or a pathover + all_goals reflexivity + end end + abstract begin + intro q, induction q, induction z, all_goals reflexivity + end end end + /- Functorial action -/ + variables {A' B' : Type} (f : A → A') (g : B → B') definition sum_functor [unfold 7] : A + B → A' + B' | sum_functor (inl a) := inl (f a) | sum_functor (inr b) := inr (g b) + /- Equivalences -/ + definition is_equiv_sum_functor [constructor] [Hf : is_equiv f] [Hg : is_equiv g] : is_equiv (sum_functor f g) := adjointify (sum_functor f g) @@ -101,13 +145,14 @@ namespace sum all_goals (intro z; induction z; all_goals reflexivity) end - -- definition sum_assoc_equiv (A B C : Type) : A + (B + C) ≃ (A + B) + C := - -- begin - -- fapply equiv.MK, - -- all_goals try (intro z; induction z with u v; - -- all_goals try induction u; all_goals try induction v), - -- all_goals try (repeat (apply inl | apply inr | assumption); now), - -- end + definition sum_assoc_equiv (A B C : Type) : A + (B + C) ≃ (A + B) + C := + begin + fapply equiv.MK, + all_goals try (intro z; induction z with u v; + all_goals try induction u; all_goals try induction v), + all_goals try (repeat append (append (apply inl) (apply inr)) assumption; now), + all_goals reflexivity + end definition sum_empty_equiv [constructor] (A : Type) : A + empty ≃ A := begin @@ -146,15 +191,21 @@ namespace sum all_goals exact _, end - /- Sums are equivalent to dependent sigmas where the first component is a bool. -/ + /- + Sums are equivalent to dependent sigmas where the first component is a bool. - definition sum_of_sigma_bool {A B : Type} (v : Σ(b : bool), bool.rec A B b) : A + B := + The current construction only works for A and B in the same universe. + If we need it for A and B in different universes, we need to insert some lifts. + -/ + + + definition sum_of_sigma_bool {A B : Type.{u}} (v : Σ(b : bool), bool.rec A B b) : A + B := by induction v with b x; induction b; exact inl x; exact inr x - definition sigma_bool_of_sum {A B : Type} (z : A + B) : Σ(b : bool), bool.rec A B b := + definition sigma_bool_of_sum {A B : Type.{u}} (z : A + B) : Σ(b : bool), bool.rec A B b := by induction z with a b; exact ⟨ff, a⟩; exact ⟨tt, b⟩ - definition sum_equiv_sigma_bool [constructor] (A B : Type) + definition sum_equiv_sigma_bool [constructor] (A B : Type.{u}) : A + B ≃ Σ(b : bool), bool.rec A B b := equiv.MK sigma_bool_of_sum sum_of_sigma_bool diff --git a/hott/types/univ.hlean b/hott/types/univ.hlean index 86cf8f7b4..f4771b9bc 100644 --- a/hott/types/univ.hlean +++ b/hott/types/univ.hlean @@ -10,17 +10,75 @@ Theorems about the universe import .bool .trunc .lift -open is_trunc bool lift unit +open is_trunc bool lift unit eq pi equiv equiv.ops sum namespace univ + universe variable u + variables {A B : Type.{u}} {a : A} {b : B} + + /- Pathovers -/ + + definition eq_of_pathover_ua {f : A ≃ B} (p : a =[ua f] b) : f a = b := + !cast_ua⁻¹ ⬝ tr_eq_of_pathover p + + definition pathover_ua {f : A ≃ B} (p : f a = b) : a =[ua f] b := + pathover_of_tr_eq (!cast_ua ⬝ p) + + definition pathover_ua_equiv (f : A ≃ B) : (a =[ua f] b) ≃ (f a = b) := + equiv.MK eq_of_pathover_ua + pathover_ua + abstract begin + intro p, unfold [pathover_ua,eq_of_pathover_ua], + rewrite [to_right_inv !pathover_equiv_tr_eq, inv_con_cancel_left] + end end + abstract begin + intro p, unfold [pathover_ua,eq_of_pathover_ua], + rewrite [con_inv_cancel_left, to_left_inv !pathover_equiv_tr_eq] + end end + + /- Properties which can be disproven for the universe -/ + definition not_is_hset_type0 : ¬is_hset Type₀ := assume H : is_hset Type₀, absurd !is_hset.elim eq_bnot_ne_idp - definition not_is_hset_type.{u} : ¬is_hset Type.{u} := + definition not_is_hset_type.{v} : ¬is_hset Type.{v} := assume H : is_hset Type, absurd (is_trunc_is_embedding_closed lift star) not_is_hset_type0 + --set_option pp.notation false + definition not_double_negation_elimination0 : ¬Π(A : Type₀), ¬¬A → A := + begin + intro f, + have u : ¬¬bool, by exact (λg, g tt), + let H1 := apdo f eq_bnot, + let H2 := apo10 H1 u, + have p : eq_bnot ▸ u = u, from !is_hprop.elim, + rewrite p at H2, + let H3 := eq_of_pathover_ua H2, esimp at H3, --TODO: use apply ... at after #700 + exact absurd H3 (bnot_ne (f bool u)), + end + + definition not_double_negation_elimination : ¬Π(A : Type), ¬¬A → A := + begin + intro f, + apply not_double_negation_elimination0, + intro A nna, refine down (f _ _), + intro na, + have ¬A, begin intro a, exact absurd (up a) na end, + exact absurd this nna + end + + definition not_excluded_middle : ¬Π(A : Type), A + ¬A := + begin + intro f, + apply not_double_negation_elimination, + intro A nna, + induction (f A) with a na, + exact a, + exact absurd na nna + end + end univ diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 0cd69dde3..ef5ebe1d6 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -160,7 +160,7 @@ "refine" "repeat" "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "rewrite" "xrewrite" "krewrite" "simp" "esimp" "unfold" "change" "check_expr" "contradiction" "exfalso" "split" "existsi" "constructor" "fconstructor" "left" "right" "injection" "congruence" "reflexivity" - "symmetry" "transitivity" "state" "induction" "induction_using" + "symmetry" "transitivity" "state" "induction" "induction_using" "fail" "append" "substvars" "now" "with_options")) word-end) (1 'font-lock-constant-face))