some macro tricks & bugfix for #success/#failure

GroundZero/Exercises/Chap5.lean

@@ -45,7 +45,7 @@ namespace «5.3»
   hott definition ez₂ : E         := e
   hott definition es₂ : ℕ → E → E := λ n _, e
 
-  #failure @es₁ E ≡ @es₂ E e : ℕ → E
+  #failure @es₁ E ≡ @es₂ E e : ℕ → E → E
 
   hott definition f : ℕ → E :=
   λ _, e

GroundZero/HITs/Merely.lean

@@ -21,62 +21,64 @@ universe u v w
   * https://arxiv.org/pdf/1512.02274
 -/
 
-def Merely (A : Type u) :=
+hott definition Merely (A : Type u) :=
 Colimit (Generalized.rep A) (Generalized.dep A)
 
 notation "∥" A "∥" => Merely A
 
 namespace Merely
-  def elem {A : Type u} (x : A) : ∥A∥ :=
+  hott definition elem {A : Type u} (x : A) : ∥A∥ :=
   Colimit.inclusion 0 x
 
+  -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/absolute.20value
+  macro:max atomic("|" noWs) x:term noWs "|" : term => `(Merely.elem $x)
+
   section
     variable {A : Type u} {B : ∥A∥ → Type v} (elemπ : Π x, B (elem x)) (uniqπ : Π x, prop (B x))
 
-    hott def resp : Π (n : ℕ) (x : Generalized.rep A n), B (Colimit.incl x)
+    hott definition resp : Π (n : ℕ) (x : Generalized.rep A n), B (Colimit.incl x)
     | Nat.zero,   x => elemπ x
     | Nat.succ n, w => @Generalized.ind _ (λ x, B (Colimit.inclusion (n + 1) x))
                          (λ x, transport B (Colimit.glue x)⁻¹ (resp n x))
                          (λ a b, uniqπ _ _ _) w
 
-    hott def ind : Π x, B x :=
-    begin intro x; fapply Colimit.ind; apply resp elemπ uniqπ; intros; apply uniqπ end
+    hott definition ind : Π x, B x :=
+    Colimit.ind (resp elemπ uniqπ) (λ _ _, uniqπ _ _ _)
   end
 
   attribute [eliminator] ind
 
-  hott def rec {A : Type u} {B : Type v} (H : prop B) (f : A → B) : ∥A∥ → B :=
+  hott definition rec {A : Type u} {B : Type v} (H : prop B) (f : A → B) : ∥A∥ → B :=
   ind f (λ _, H)
 
-  hott def weakUniq {A : Type u} (x y : A) : @Types.Id ∥A∥ (elem x) (elem y) :=
+  hott lemma weakUniq {A : Type u} (x y : A) : @Id ∥A∥ |x| |y| :=
   begin
     transitivity; { symmetry; apply Colimit.glue }; symmetry;
     transitivity; { symmetry; apply Colimit.glue };
     apply ap; apply Generalized.glue
   end
 
-  hott def incl {A : Type u} {n : ℕ} :=
+  hott definition incl {A : Type u} {n : ℕ} :=
   @Colimit.incl (Generalized.rep A) (Generalized.dep A) n
 
-  hott def glue {A : Type u} {n : ℕ} {x : Generalized.rep A n} :
+  hott definition glue {A : Type u} {n : ℕ} {x : Generalized.rep A n} :
     incl (Generalized.dep A n x) = incl x :=
   Colimit.glue x
 
-  hott def exactNth {A : Type u} (a : A) : Π n, Generalized.rep A n
+  hott definition exactNth {A : Type u} (a : A) : Π n, Generalized.rep A n
   | Nat.zero   => a
   | Nat.succ n => Generalized.dep A n (exactNth a n)
 
-  hott def nthGlue {A : Type u} (a : A) : Π n, incl (exactNth a n) = @incl A 0 a
+  hott definition nthGlue {A : Type u} (a : A) : Π n, incl (exactNth a n) = @incl A 0 a
   | Nat.zero   => idp _
   | Nat.succ n => Colimit.glue (exactNth a n) ⬝ nthGlue a n
 
-  hott lemma inclUniq {A : Type u} {n : ℕ} (a b : Generalized.rep A n) : incl a = incl b :=
+  hott lemma inclUniq {A : Type u} {n : ℕ} (a b : Generalized.rep A n) :=
   calc incl a = incl (Generalized.dep A n a) : glue⁻¹
           ... = incl (Generalized.dep A n b) : ap incl (Generalized.glue a b)
           ... = incl b                       : glue
 
-  hott lemma inclZeroEqIncl {A : Type u} {n : ℕ} (x : A)
-    (y : Generalized.rep A n) : @incl A 0 x = incl y :=
+  hott lemma inclZeroEqIncl {A : Type u} {n : ℕ} (x : A) (y : Generalized.rep A n) :=
   calc @incl A 0 x = incl (exactNth x n) : (nthGlue x n)⁻¹
                ... = incl y              : inclUniq (exactNth x n) y
 
@@ -88,7 +90,7 @@ namespace Merely
   hott lemma congClose {A : Type u} {n : ℕ} {a b : Generalized.rep A n} (p : a = b) :
     glue⁻¹ ⬝ ap incl (ap (Generalized.dep A n) p) ⬝ glue = ap incl p :=
   begin
-    induction p; transitivity; { symmetry; apply Id.assoc };
+    induction p; transitivity; symmetry; apply Id.assoc;
     apply Equiv.rewriteComp; symmetry; apply Id.rid
   end
 
@@ -125,27 +127,26 @@ namespace Merely
   hott corollary hprop {A : Type u} : is-(−1)-type ∥A∥ :=
   minusOneEqvProp.left uniq
 
-  hott def lift {A : Type u} {B : Type v} (f : A → B) : ∥A∥ → ∥B∥ :=
+  hott definition lift {A : Type u} {B : Type v} (f : A → B) : ∥A∥ → ∥B∥ :=
   rec uniq (elem ∘ f)
 
-  hott def rec₂ {A : Type u} {B : Type v} {γ : Type w} (H : prop γ)
+  hott definition rec₂ {A : Type u} {B : Type v} {γ : Type w} (H : prop γ)
     (φ : A → B → γ) : ∥A∥ → ∥B∥ → γ :=
   @rec A (∥B∥ → γ) (implProp H) (rec H ∘ φ)
 
-  hott def lift₂ {A : Type u} {B : Type v} {γ : Type w}
+  hott definition lift₂ {A : Type u} {B : Type v} {γ : Type w}
     (φ : A → B → γ) : ∥A∥ → ∥B∥ → ∥γ∥ :=
-  rec₂ uniq (λ a b, elem (φ a b))
+  rec₂ uniq (λ a b, |φ a b|)
 
-  hott def equivIffTrunc {A B : Type u}
-    (f : A → B) (g : B → A) : ∥A∥ ≃ ∥B∥ :=
+  hott theorem equivIffTrunc {A B : Type u} (f : A → B) (g : B → A) : ∥A∥ ≃ ∥B∥ :=
   ⟨lift f, (⟨lift g, λ _, uniq _ _⟩, ⟨lift g, λ _, uniq _ _⟩)⟩
 
-  def diag {A : Type u} (a : A) : A × A := ⟨a, a⟩
+  hott definition diag {A : Type u} (a : A) : A × A := ⟨a, a⟩
 
-  hott def productIdentity {A : Type u} : ∥A∥ ≃ ∥A × A∥ :=
+  hott corollary productIdentity {A : Type u} : ∥A∥ ≃ ∥A × A∥ :=
   equivIffTrunc diag Prod.fst
 
-  hott def uninhabitedImpliesTruncUninhabited {A : Type u} : ¬A → ¬∥A∥ :=
+  hott corollary uninhabitedImpliesTruncUninhabited {A : Type u} : ¬A → ¬∥A∥ :=
   rec Structures.emptyIsProp
 end Merely
 

GroundZero/HITs/Trunc.lean

@@ -33,8 +33,7 @@ namespace Trunc
   | −1            => Merely.hprop
   | succ (succ n) => λ _ _, propIsNType (λ _ _, trustCoherence) n
 
-  @[eliminator] def ind {B : Trunc n A → Type v} (elemπ : Π x, B (elem x))
-    (uniqπ : Π x, is-n-type (B x)) : Π x, B x :=
+  @[eliminator] def ind {B : Trunc n A → Type v} (elemπ : Π x, B (elem x)) (uniqπ : Π x, is-n-type (B x)) : Π x, B x :=
   match n with
   | −2            => λ x, (uniqπ x).1
   | −1            => Merely.ind elemπ (λ _, minusOneEqvProp.forward (uniqπ _))
@@ -50,10 +49,11 @@ namespace Trunc
   macro:max "∥" A:term "∥" n:subscript : term => do
     `(Trunc $(← Meta.Notation.parseSubscript n) $A)
 
-  macro "|" x:term "|" n:subscript : term => do
-    `(@Trunc.elem _ $(← Meta.Notation.parseSubscript n) $x)
+  -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/absolute.20value
+  macro:max atomic("|" noWs) x:term noWs "|" n:subscript : term =>
+    do `(@Trunc.elem _ $(← Meta.Notation.parseSubscript n) $x)
 
-  hott lemma indβrule {B : ∥A∥ₙ → Type v} (elemπ : Π x, B (elem x))
+  hott lemma indβrule {B : ∥A∥ₙ → Type v} (elemπ : Π x, B |x|ₙ)
     (uniqπ : Π x, is-n-type (B x)) (x : A) : ind elemπ uniqπ (elem x) = elemπ x :=
   begin
     match n with | −2 => _ | −1 => _ | succ (succ n) => _;
@@ -63,35 +63,35 @@ namespace Trunc
   section
     variable {B : Type v} (elemπ : A → B) (uniqπ : is-n-type B)
 
-    hott def rec : ∥A∥ₙ → B := @ind A n (λ _, B) elemπ (λ _, uniqπ)
+    hott definition rec : ∥A∥ₙ → B := @ind A n (λ _, B) elemπ (λ _, uniqπ)
 
     hott corollary recβrule (x : A) : rec elemπ uniqπ (elem x) = elemπ x :=
     by apply indβrule
   end
 
-  hott def elemClose {B : Type v} (G : is-n-type B)
+  hott definition elemClose {B : Type v} (G : is-n-type B)
     (f g : ∥A∥ₙ → B) (H : f ∘ elem = g ∘ elem) : f = g :=
   begin
     apply Theorems.funext; fapply ind <;> intro x;
     { exact ap (λ (f : A → B), f x) H };
     { apply hlevel.cumulative; assumption }
   end
 
-  hott def nthTrunc (H : is-n-type A) : A ≃ ∥A∥ₙ :=
+  hott definition nthTrunc (H : is-n-type A) : A ≃ ∥A∥ₙ :=
   begin
     existsi elem; apply Prod.mk <;> existsi rec id H;
     { intro; apply recβrule; };
     { apply Interval.happly; apply elemClose; apply uniq;
       apply Theorems.funext; intro; apply ap elem; apply recβrule; }
   end
 
-  hott def setEquiv {A : Type u} (H : hset A) : A ≃ ∥A∥₀ :=
+  hott definition setEquiv {A : Type u} (H : hset A) : A ≃ ∥A∥₀ :=
   begin apply nthTrunc; apply zeroEqvSet.left; assumption end
 
-  hott def ap {A : Type u} {B : Type v} {n : ℕ₋₂} (f : A → B) : ∥A∥ₙ → ∥B∥ₙ :=
+  hott definition ap {A : Type u} {B : Type v} {n : ℕ₋₂} (f : A → B) : ∥A∥ₙ → ∥B∥ₙ :=
   rec (elem ∘ f) (uniq n)
 
-  hott def ap₂ {A : Type u} {B : Type v} {C : Type w}
+  hott definition ap₂ {A : Type u} {B : Type v} {C : Type w}
     {n : ℕ₋₂} (f : A → B → C) : ∥A∥ₙ → ∥B∥ₙ → ∥C∥ₙ :=
   rec (ap ∘ f) (piRespectsNType n (λ _, uniq n))
 

GroundZero/Meta/Notation.lean

@@ -66,7 +66,7 @@ section
   }
 end
 
-macro "begin " ts:sepBy1(tactic, ";", "; ", allowTrailingSep) i:"end" : term =>
+macro "begin " ts:sepBy(tactic, ";", "; ", allowTrailingSep) i:"end" : term =>
   `(by { $[($ts:tactic)]* }%$i)
 
 declare_syntax_cat superscriptNumeral
@@ -323,8 +323,8 @@ namespace Defeq
   elab "#success " σ₁:term tag:" ≡ " σ₂:term τ:(typeSpec)? : command =>
   Elab.Command.runTermElabM fun _ => do {
     let T  ← elabTypeSpec τ;
-    let τ₁ ← Elab.Term.elabTerm σ₁ T;
-    let τ₂ ← Elab.Term.elabTerm σ₂ T;
+    let τ₁ ← Elab.Term.elabTermEnsuringType σ₁ T;
+    let τ₂ ← Elab.Term.elabTermEnsuringType σ₂ T;
 
     Elab.Term.synthesizeSyntheticMVarsNoPostponing;
     let τ₁ ← Elab.Term.levelMVarToParam (← instantiateMVars τ₁);
@@ -336,8 +336,8 @@ namespace Defeq
   elab "#failure " σ₁:term tag:" ≡ " σ₂:term τ:(typeSpec)? : command =>
   Elab.Command.runTermElabM fun _ => do {
     let T  ← elabTypeSpec τ;
-    let τ₁ ← Elab.Term.elabTerm σ₁ T;
-    let τ₂ ← Elab.Term.elabTerm σ₂ T;
+    let τ₁ ← Elab.Term.elabTermEnsuringType σ₁ T;
+    let τ₂ ← Elab.Term.elabTermEnsuringType σ₂ T;
 
     Elab.Term.synthesizeSyntheticMVarsNoPostponing;
     let τ₁ ← Elab.Term.levelMVarToParam (← instantiateMVars τ₁);

GroundZero/Meta/Trust.lean

@@ -22,7 +22,7 @@ def Quot.withUseOf {X : Type u} {R : X → X → Sort 0} {A : Type v} {B : Type
 
 section
   variable (X : Type u) (R : X → X → Sort 0) (A : Type u) (B : Type w) (a₁ a₂ : A) (b : B)
-  #failure @Quot.withUseOf X R A B a₁ b ≡ @Quot.withUseOf X R A B a₂ b
+  #failure @Quot.withUseOf X R A B a₁ b ≡ @Quot.withUseOf X R A B a₂ b : Quot R → B
 end
 
 /--
@@ -43,11 +43,11 @@ namespace EtaFailure
 
   variable (X : Type u) (A : Type u) (B : Type w) (a₁ a₂ : A) (b : B)
 
-  #success @withUseOf X A B a₁ b ≡ @withUseOf X A B a₂ b
+  #success @withUseOf X A B a₁ b ≡ @withUseOf X A B a₂ b : Opaque X → B
 
   variable (x : Opaque X)
-  #success @withUseOf X A B a₁ b x ≡ b
-  #success @withUseOf X A B a₂ b x ≡ b
+  #success @withUseOf X A B a₁ b x ≡ b : B
+  #success @withUseOf X A B a₂ b x ≡ b : B
 end EtaFailure
 
 namespace Opaque

GroundZero/Theorems/Functions.lean

@@ -26,16 +26,14 @@ hott def Ran {A : Type u} {B : Type v} (f : A → B) :=
 total (fibInh f)
 
 hott def cut {A : Type u} {B : Type v} (f : A → B) : A → Ran f :=
-λ x, ⟨f x, Merely.elem ⟨x, idp (f x)⟩⟩
+λ x, ⟨f x, |⟨x, idp (f x)⟩|⟩
 
 hott def cutIsSurj {A : Type u} {B : Type v} (f : A → B) : surjective (cut f) :=
 begin
   intro ⟨x, (H : ∥_∥)⟩; induction H;
-  case elemπ G => {
-    apply Merely.elem; existsi G.1;
-    fapply Sigma.prod; exact G.2;
-    apply Merely.uniq
-  };
+  case elemπ G =>
+  { apply Merely.elem; existsi G.1; fapply Sigma.prod;
+    exact G.2; apply Merely.uniq };
   apply Merely.uniq
 end
 
@@ -52,9 +50,8 @@ begin
   { intro; reflexivity }
 end
 
-hott def ranConst {A : Type u} (a : A) {B : Type v} (b : B) :
-  Ran (Function.const A b) :=
-⟨b, Merely.elem ⟨a, idp b⟩⟩
+hott def ranConst {A : Type u} (a : A) {B : Type v} (b : B) : Ran (Function.const A b) :=
+⟨b, |⟨a, idp b⟩|⟩
 
 hott def ranConstEqv {A : Type u} (a : A) {B : Type v}
   (H : hset B) (b : B) : Ran (Function.const A b) ≃ 𝟏 :=

GroundZero/Types/CellComplex.lean

@@ -1,21 +1,21 @@
 import GroundZero.HITs.Sphere
 open GroundZero.HITs
 
-universe u v
+universe u v w
 
 namespace GroundZero
 namespace Types
 
--- https://github.com/leanprover/lean2/blob/master/hott/homotopy/cellcomplex.hlean
--- https://arxiv.org/abs/1802.02191
+/- https://github.com/leanprover/lean2/blob/master/hott/homotopy/cellcomplex.hlean
+   Cellular Cohomology in Homotopy Type Theory, https://arxiv.org/abs/1802.02191
+-/
 
 hott definition Model :=
 Σ (X : Type u), X → Type v
 
 hott definition FdCC : ℕ → Model
-| Nat.zero   => ⟨Set u, Sigma.fst⟩
-| Nat.succ n => ⟨Σ (X : (FdCC n).1) (A : Set u), A.1 × Sⁿ → (FdCC n).2 X,
-                 λ w, Pushout (@Prod.fst w.2.1.1 Sⁿ) w.2.2⟩
+| Nat.zero   => ⟨Set u, Sigma.pr₁⟩
+| Nat.succ n => ⟨Σ (X : (FdCC n).1) (A : Set u), A.1 × Sⁿ → (FdCC n).2 X, λ w, Pushout Prod.pr₁ w.2.2⟩
 
 -- finite-dimensional cell complex
 hott definition fdcc (n : ℕ) := (FdCC n).1