update

GroundZero/Algebra/Category.lean

@@ -35,7 +35,7 @@ namespace Precategory
       | Arity.left    => λ (a, _), dom a
       | Arity.right   => λ (a, _), cod a
       | Arity.bottom  => λ _, bot,
-    λ z, Empty.elim z)⟩
+    λ z, explode z)⟩
 
   variable (𝒞 : Precategory.{u})
 

GroundZero/Algebra/EilenbergMacLane.lean

@@ -33,7 +33,7 @@ namespace K1
     (groupoidπ : Π x, groupoid (C x)) : Π x, C x :=
   λ x, Quot.withUseOf (loopπ, mulπ, groupoidπ) (Opaque.ind (λ ★, baseπ) x) x
 
-  attribute [eliminator] ind
+  attribute [induction_eliminator] ind
 
   hott axiom rec {C : Type v} (baseπ : C) (loopπ : G.carrier → baseπ = baseπ)
     (mulπ : Π x y, loopπ (G.φ x y) = loopπ x ⬝ loopπ y)

GroundZero/Algebra/Geometry.lean

@@ -9,7 +9,7 @@ namespace GroundZero.Algebra
   universe u v
 
   hott def Pregeometry : Type (max u v + 1) :=
-  @Alg.{0, 0, u, v} 𝟎 𝟐 (Coproduct.elim Empty.elim (Bool.rec 3 4))
+  @Alg.{0, 0, u, v} 𝟎 𝟐 (Coproduct.elim explode (Bool.rec 3 4))
 
   namespace Pregeometry
     def between (G : Pregeometry) (a b c : G.carrier) :=
@@ -77,4 +77,4 @@ namespace GroundZero.Algebra
       Ens.parallel (geodesic G a₂ b₂) (geodesic G a₃ b₃) →
       Ens.parallel (geodesic G a₁ b₁) (geodesic G a₂ b₂))
   end Pregeometry
-end GroundZero.Algebra
+end GroundZero.Algebra

GroundZero/Algebra/Group/Alternating.lean

@@ -28,7 +28,7 @@ namespace Group
   inductive D₃.carrier
   | R₀ | R₁ | R₂
   | S₀ | S₁ | S₂
-  attribute [eliminator] D₃.carrier.casesOn
+  attribute [induction_eliminator] D₃.carrier.casesOn
 
   open D₃.carrier
 

GroundZero/Algebra/Group/Finite.lean

@@ -4,6 +4,7 @@ import GroundZero.Theorems.Nat
 open GroundZero.Types.Equiv (transport)
 open GroundZero.Types.Id (ap)
 open GroundZero.Types
+open GroundZero.Proto
 
 namespace GroundZero
 universe u v w
@@ -28,7 +29,7 @@ namespace Types.Coproduct
   Σ (x : A), Π y, ¬(x = f y)
 
   hott def Diff.inl : Diff (@Sum.inl A B) → B :=
-  λ | ⟨Sum.inl x, p⟩ => Proto.Empty.elim (p x Id.refl)
+  λ | ⟨Sum.inl x, p⟩ => explode (p x Id.refl)
     | ⟨Sum.inr x, p⟩ => x
 
   hott def Empty.lift : Proto.Empty.{u} → Proto.Empty.{v} :=
@@ -41,7 +42,7 @@ namespace Types.Coproduct
   begin
     existsi Diff.inl; apply Prod.mk <;> existsi Diff.inr;
     { intro ⟨x, p⟩; induction x using Sum.casesOn;
-      { apply Proto.Empty.elim; fapply p; assumption; reflexivity };
+      { apply explode; fapply p; assumption; reflexivity };
       { fapply Types.Sigma.prod; reflexivity;
         { apply Structures.piProp; intro;
           apply Structures.notIsProp } } };
@@ -78,7 +79,7 @@ namespace Types.Coproduct
   begin
     existsi zero; apply Prod.mk <;> existsi Sum.inr <;> intro x;
     { induction x using Sum.casesOn;
-      apply Proto.Empty.elim; assumption;
+      apply explode; assumption;
       reflexivity };
     { reflexivity }
   end
@@ -87,9 +88,9 @@ end Types.Coproduct
 namespace Types.Product
   hott def destroy : 𝟎 × A ≃ 𝟎 := begin
     existsi Prod.fst; apply Prod.mk <;>
-    existsi Proto.Empty.elim <;> intro x;
-    apply Proto.Empty.elim x.1;
-    apply Proto.Empty.elim x
+    existsi explode <;> intro x;
+    apply explode x.1;
+    apply explode x
   end
 
   hott def split : (A + B) × C → (A × C) + (B × C)

GroundZero/Algebra/Group/Free.lean

@@ -61,7 +61,7 @@ namespace Group
     def rec (G : Group) (f : ε → G.carrier) (x : F.carrier ε) : G.carrier :=
     Exp.eval G f x.value
 
-    @[eliminator] def ind {π : F.carrier ε → Type v}
+    @[induction_eliminator] def ind {π : F.carrier ε → Type v}
       (setπ : Π x, Structures.hset (π x))
       (u : π unit) (η : Π x, π (elem x))
       (m : Π {x y}, π x → π y → π (mul x y))

GroundZero/Algebra/Group/Isomorphism.lean

@@ -60,11 +60,10 @@ namespace Group
     noncomputable hott def ker.decodeSigma {φ : Hom G H} :
       Π (x : im.carrier φ), fib ker.encode x :=
     begin
-      intro ⟨x, (p : ∥_∥)⟩; induction p; case elemπ z =>
-      { existsi ker.incl z.1; fapply Types.Sigma.prod;
+      apply Sigma.Ind; intro x; fapply Merely.ind;
+      { intro z; existsi ker.incl z.1; fapply Types.Sigma.prod;
         apply z.2; apply HITs.Merely.uniq };
-      case uniqπ p q =>
-      { fapply Types.Sigma.prod;
+      { intro w p q; fapply Types.Sigma.prod;
         { apply ker.encodeInj; transitivity;
           exact p.2; symmetry; exact q.2 };
         { apply Ens.hset; apply H.hset } }

GroundZero/Algebra/Orgraph.lean

@@ -39,7 +39,7 @@ namespace GroundZero.Algebra
   class order (Γ : Orgraph) extends reflexive Γ, antisymmetric Γ, transitive Γ
 
   def Overring.κ (T : Overring) : Orgraph :=
-  ⟨T.1, (λ z, nomatch z, T.2.2)⟩
+  ⟨T.1, (λ z, explode z, T.2.2)⟩
 
   class connected (Γ : Orgraph) :=
   (total : Π x y, ∥Γ.ρ x y + Γ.ρ y x∥)
@@ -91,7 +91,7 @@ namespace GroundZero.Algebra
   begin
     fapply GroundZero.HITs.Merely.rec _ _ (@connected.total T.κ _ _ _);
     change T.carrier; exact 0; change T.carrier; exact 1; apply T.κ.prop;
-    { intro z; induction z using Sum.casesOn; assumption; apply Empty.elim;
+    { intro z; induction z using Sum.casesOn; assumption; apply explode;
       apply @field.nontrivial T.τ _; apply @antisymmetric.asymm T.κ;
       assumption; apply Equiv.transport; apply ring.minusOneSqr;
       apply orfield.leOverMul <;>
@@ -198,7 +198,7 @@ namespace GroundZero.Algebra
     { intro ih; induction ih; assumption;
       match @Classical.lem _ (a = b) (T.hset _ _) with | Sum.inl r₁ => _ | Sum.inr r₂ => _;
       apply eqImplReflRel T.κ; symmetry; apply ap T.τ.neg r₁;
-      apply Empty.elim; apply (_ : T.σ 0 0).1; reflexivity;
+      apply explode; apply (_ : T.σ 0 0).1; reflexivity;
       apply Equiv.transportconst; apply Equiv.bimap;
       apply @Group.mulRightInv T.τ⁺; exact a;
       apply @Group.mulRightInv T.τ⁺; exact b;

GroundZero/Algebra/Reals.lean

@@ -4,6 +4,7 @@ import GroundZero.Theorems.Nat
 open GroundZero.Types.Id (ap)
 open GroundZero.Structures
 open GroundZero.Theorems
+open GroundZero.Proto
 open GroundZero.Types
 open GroundZero.HITs
 
@@ -69,7 +70,7 @@ namespace GroundZero.Algebra
   noncomputable hott def N.incl.lt : Π (n m : ℕ), (n ≤ m : Type) → R.ρ (N.incl n) (N.incl m)
   | Nat.zero,   Nat.zero   => λ _, @reflexive.refl R.κ _ (N.incl 0)
   | Nat.zero,   Nat.succ m => λ _, @transitive.trans R.κ _ (N.incl 0) (N.incl m) (N.incl (m + 1)) (lt 0 m (Nat.max.zeroLeft m)) (leAddOne (N.incl m))
-  | Nat.succ n, Nat.zero   => λ p, GroundZero.Proto.Empty.elim (Nat.max.neZero p)
+  | Nat.succ n, Nat.zero   => λ p, explode (Nat.max.neZero p)
   | Nat.succ n, Nat.succ m => λ p, orfield.leOverAdd (N.incl n) (N.incl m) 1 (lt n m (ap Nat.pred p))
 
   noncomputable hott def R.complete (φ : R.subset) (H : φ.inh) (G : @majorized R.κ φ) :
@@ -138,8 +139,8 @@ namespace GroundZero.Algebra
   begin
     intros p q; match p, q with
     | Sum.inl p₁,      Sum.inl q₁      => { apply ap; apply R.κ.prop }
-    | Sum.inl p₁,      Sum.inr q₂      => { apply GroundZero.Proto.Empty.elim; apply R.notNotTotal x y <;> assumption }
-    | Sum.inr p₂,      Sum.inl q₁      => { apply GroundZero.Proto.Empty.elim; apply R.notNotTotal x y <;> assumption }
+    | Sum.inl p₁,      Sum.inr q₂      => { apply explode; apply R.notNotTotal x y <;> assumption }
+    | Sum.inr p₂,      Sum.inl q₁      => { apply explode; apply R.notNotTotal x y <;> assumption }
     | Sum.inr (p, p'), Sum.inr (q, q') => { apply ap; apply Product.prod; apply notIsProp; apply R.κ.prop }
   end
 
@@ -162,7 +163,7 @@ namespace GroundZero.Algebra
   noncomputable hott def abs.pos {x : ℝ} (p : R.ρ 0 x) : abs x = x :=
   begin
     change Coproduct.elim _ _ _ = _; induction R.total 0 x;
-    reflexivity; apply GroundZero.Proto.Empty.elim;
+    reflexivity; apply explode;
     apply R.notNotTotal 0 x <;> assumption
   end
 
@@ -307,7 +308,7 @@ namespace GroundZero.Algebra
     intro p; induction R.total 0 x;
     case inl q₁ => { apply q₁ };
     case inr q₂ =>
-    { apply GroundZero.Proto.Empty.elim; apply (strictIneqAdd R q₂ q₂).1;
+    { apply explode; apply (strictIneqAdd R q₂ q₂).1;
       apply @antisymmetric.asymm R.κ; apply ineqAdd <;> exact q₂.2;
       apply Equiv.transport (R.ρ · (x + x)); symmetry; apply R.τ⁺.mulOne; exact p }
   end

GroundZero/Exercises/Chap2.lean

@@ -133,8 +133,8 @@ namespace «2.8»
 
   hott definition ρ : Π {x y : A + B}, Coproduct.code x y → Coproduct.code (φ g h x) (φ g h y)
   | Sum.inl _, Sum.inl _, p => ap _ p
-  | Sum.inr _, Sum.inl _, p => Empty.elim p
-  | Sum.inl _, Sum.inr _, p => Empty.elim p
+  | Sum.inr _, Sum.inl _, p => explode p
+  | Sum.inl _, Sum.inr _, p => explode p
   | Sum.inr _, Sum.inr _, p => ap _ p
 
   hott definition mapPathSum (x y : A + B) : Π p,
@@ -148,8 +148,8 @@ namespace «2.8»
     | Sum.inr x, Sum.inr y => _;
 
     { intro (p : x = y); induction p; reflexivity };
-    { intro; apply Empty.elim; assumption };
-    { intro; apply Empty.elim; assumption };
+    { intro; apply explode; assumption };
+    { intro; apply explode; assumption };
     { intro (p : x = y); induction p; reflexivity }
   end
 end «2.8»

GroundZero/Exercises/Chap3.lean

@@ -96,11 +96,11 @@ namespace «3.9»
     hott definition lemTrue (x : A) : lem A H = Sum.inl x :=
     match lem A H with
     | Sum.inl y => ap Sum.inl (H y x)
-    | Sum.inr φ => Empty.elim (φ x)
+    | Sum.inr φ => explode (φ x)
 
     hott definition lemFalse (φ : ¬A) : lem A H = Sum.inr φ :=
     match lem A H with
-    | Sum.inl x => Empty.elim (φ x)
+    | Sum.inl x => explode (φ x)
     | Sum.inr ψ => ap Sum.inr (Structures.notIsProp ψ φ)
   end
 
@@ -113,7 +113,7 @@ namespace «3.9»
   hott lemma propsetInhIsProp (A : Prop) : prop A.1 := A.2
 
   hott lemma Ωlinv (lem : LEM₋₁) : Ωelim lem ∘ Ωintro ~ idfun
-  | false => ap (Coproduct.elim _ _) (lemFalse Empty.elim)
+  | false => ap (Coproduct.elim _ _) (lemFalse explode)
   | true  => ap (Coproduct.elim _ _) (lemTrue ★)
 
   noncomputable hott lemma Ωrinv (lem : LEM₋₁) : Ωintro ∘ Ωelim lem ~ idfun :=
@@ -125,7 +125,7 @@ namespace «3.9»
     fapply Sigma.mk; exact x; intro y; apply w.2;
 
     transitivity; apply ap; apply ap (Bool.elim _ _); apply ap (Coproduct.elim _ _);
-    apply lemFalse φ; symmetry; apply ua; apply uninhabitedType; exact Empty.elim ∘ φ
+    apply lemFalse φ; symmetry; apply ua; apply uninhabitedType; exact explode ∘ φ
   end
 
   noncomputable hott theorem lemImplPropEqvBool (lem : LEM₋₁) : Prop u ≃ 𝟐 :=
@@ -159,7 +159,7 @@ namespace «3.10»
   begin
     intro b; transitivity; apply ap Ωintro; apply Ωlinv; apply Equiv.propset.Id;
     symmetry; apply ua; induction b using Bool.casesOn;
-    { apply uninhabitedType; exact Empty.elim ∘ Resize.elim };
+    { apply uninhabitedType; exact explode ∘ Resize.elim };
     { apply Structures.contrEquivUnit; existsi Resize.intro ★;
       intro (Resize.intro b); apply ap; apply Structures.unitIsProp }
   end
@@ -212,7 +212,7 @@ end «3.11»
 
 namespace «3.12»
   hott lemma implOfSum {A : Type u} {B : Type v} : (¬A) + B → A → B
-  | Sum.inl φ => Empty.elim ∘ φ
+  | Sum.inl φ => explode ∘ φ
   | Sum.inr b => λ _, b
 
   hott theorem WC (lem : LEM₋₁ u) : Π (A : Type u), ∥(∥A∥ → A)∥ :=
@@ -233,7 +233,7 @@ namespace «3.13»
   hott lemma LEMinfImplDNInf (lem : LEM∞ u) {A : Type u} : ∥A∥ → A :=
   match lem A with
   | Sum.inl a => λ _, a
-  | Sum.inr φ => λ w, Empty.elim (@merelyImplDn A w φ)
+  | Sum.inr φ => λ w, explode (@merelyImplDn A w φ)
 
   -- see lemma 3.8.2
   hott theorem LEMinfImplCartesian (lem : LEM∞ v) (A : Type u) (B : A → Type v) :
@@ -251,7 +251,7 @@ namespace «3.13»
   hott lemma LEMinfDual (lem : LEM∞ v) {A : Type u} {B : A → Type v} : ¬(Σ x, ¬B x) → Π x, B x :=
   λ φ x, match lem (B x) with
   | Sum.inl b => b
-  | Sum.inr ψ => Empty.elim (φ ⟨x, ψ⟩)
+  | Sum.inr ψ => explode (φ ⟨x, ψ⟩)
 end «3.13»
 
 -- exercise 3.14
@@ -265,7 +265,7 @@ namespace «3.14»
   λ x φ, φ x
 
   hott definition dn.rec (lem : LEM₋₁ v) {A : Type u} {B : Type v} : prop B → (A → B) → (¬¬A → B) :=
-  λ H f, Coproduct.elim (λ b _, b) (λ φ g, Empty.elim (g (φ ∘ f))) (lem B H)
+  λ H f, Coproduct.elim (λ b _, b) (λ φ g, explode (g (φ ∘ f))) (lem B H)
 
   hott definition dn.recβrule (lem : LEM₋₁ v) {A : Type u} {B : Type v} {H : prop B}
     {f : A → B} (x : A) : dn.rec lem H f (dn.intro x) = f x :=
@@ -321,7 +321,7 @@ namespace «3.16.1»
   hott lemma dn.intro (lem : LEM₋₁ v) : (Π x, ¬¬(Y x)) → ¬¬(Π x, Y x) :=
   λ φ f, f (λ x, match lem (Y x) (G x) with
   | Sum.inl y => y
-  | Sum.inr g => Empty.elim (φ x g))
+  | Sum.inr g => explode (φ x g))
 
   hott theorem dn.comm (lem : LEM₋₁ v) : ¬¬(Π x, Y x) ≃ (Π x, ¬¬(Y x)) :=
   begin
@@ -387,7 +387,7 @@ namespace «3.18»
     apply Prod.mk; intro lem P H nnp;
     induction lem P H using Sum.casesOn;
     case inl p  => { exact p };
-    case inr np => { apply Empty.elim (nnp np) };
+    case inr np => { apply explode (nnp np) };
 
     intro dneg P H; apply dneg; apply propEM H; intro npnp;
     apply npnp; right; intro p; apply npnp; left; exact p
@@ -502,7 +502,7 @@ namespace «3.22»
                  @transport _ Y (fin.fsuc m') m (Sigma.prod (idp m.1) (Nat.le.prop _ _ _ _)) (prev m')
 
   hott theorem finAC : Π (n : ℕ) (Y : fin n → Type u), (Π x, ∥Y x∥) → ∥Π x, Y x∥
-  | Nat.zero,   Y, _ => Merely.elem (λ k, Empty.elim (Nat.max.neZero k.2))
+  | Nat.zero,   Y, _ => Merely.elem (λ k, explode (Nat.max.neZero k.2))
   | Nat.succ n, Y, H => Merely.lift₂ (step n Y) (finAC n (Y ∘ fin.fsuc) (λ m, H (fin.fsuc m))) (H (fin.fmax n))
 end «3.22»
 
@@ -513,7 +513,7 @@ namespace «3.23»
   open GroundZero.HITs
 
   hott definition choice {A : Type u} (G : dec A) : A → Type u :=
-  λ x, Coproduct.elim (x = ·) (λ φ, Empty.elim (φ x)) G
+  λ x, Coproduct.elim (x = ·) (λ φ, explode (φ x)) G
 
   hott definition decMerely {A : Type u} (G : dec A) : Type u :=
   Σ x, choice G x
@@ -522,7 +522,7 @@ namespace «3.23»
   begin
     intro x; induction G using Sum.casesOn;
     case inl y => { existsi y; apply idp };
-    case inr φ => { apply Empty.elim (φ x) }
+    case inr φ => { apply explode (φ x) }
   end
 
   hott definition decMerely.uniq {A : Type u} (G : dec A) : prop (decMerely G) :=
@@ -533,7 +533,7 @@ namespace «3.23»
                     { transitivity; apply transportCompositionRev;
                       apply Equiv.rewriteComp; symmetry;
                       apply Id.cancelInvComp } };
-    case inr φ => { intro w₁ w₂; apply Empty.elim (φ w₁.1) }
+    case inr φ => { intro w₁ w₂; apply explode (φ w₁.1) }
   end
 
   hott definition decMerely.dec {A : Type u} (G : dec A) : dec (@decMerely A G) :=

GroundZero/Exercises/Chap4.lean

@@ -443,8 +443,8 @@ namespace «4.8»
     { intro w; existsi Bool.elim w.1.1 w.1.2;
       intro b₁ b₂ p; match b₁, b₂ with
       | false, false => { reflexivity }
-      | false, true  => { apply Empty.elim; apply w.2; exact p }
-      | true,  false => { apply Empty.elim; apply w.2; exact p⁻¹ }
+      | false, true  => { apply explode; apply w.2; exact p }
+      | true,  false => { apply explode; apply w.2; exact p⁻¹ }
       | true,  true  => { reflexivity } };
     apply Prod.mk;
     { intro w; apply Sigma.prod; apply notIsProp; reflexivity };
@@ -469,12 +469,12 @@ namespace «4.8»
       | false, false => { fapply Sigma.mk; intro; reflexivity; apply Prod.mk;
                           { intro; apply contrImplProp; apply w.2.2.1 };
                           { intro; apply boolIsSet } }
-      | false, true  => { fapply Sigma.mk; intro p; apply Empty.elim; apply w.2.1 p; apply Prod.mk;
-                          { intro p; apply Empty.elim; apply w.2.1 p };
-                          { intro; apply Empty.elim; apply ffNeqTt; assumption } }
-      | true,  false => { fapply Sigma.mk; intro p; apply Empty.elim; apply w.2.1 p⁻¹; apply Prod.mk;
-                          { intro p; apply Empty.elim; apply w.2.1 p⁻¹ };
-                          { intro; apply Empty.elim; apply ffNeqTt; symmetry; assumption } }
+      | false, true  => { fapply Sigma.mk; intro p; apply explode; apply w.2.1 p; apply Prod.mk;
+                          { intro p; apply explode; apply w.2.1 p };
+                          { intro; apply explode; apply ffNeqTt; assumption } }
+      | true,  false => { fapply Sigma.mk; intro p; apply explode; apply w.2.1 p⁻¹; apply Prod.mk;
+                          { intro p; apply explode; apply w.2.1 p⁻¹ };
+                          { intro; apply explode; apply ffNeqTt; symmetry; assumption } }
       | true,  true  => { fapply Sigma.mk; intro; reflexivity; apply Prod.mk;
                           { intro; apply contrImplProp; apply w.2.2.2 };
                           { intro; apply boolIsSet } } };