feat(hott/types): add more about pathovers in type constructors, prove that double negation elimination doesn't hold universally

2015-08-07 18:37:05 +02:00 · 2015-08-07 18:37:05 +02:00 · c24fd508b6
commit c24fd508b6
parent cfddfdfa84
10 changed files with 187 additions and 34 deletions
--- 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.
--- 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]
--- 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')
--- 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 :=
--- 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'),
--- 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')
--- 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
  -/
--- 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
--- 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
--- 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))