style

GroundZero/Cubical/Connection.lean

@@ -10,7 +10,7 @@ universe u
 
 variable {A : Type u} {a b : A} (p : Path A a b)
 
-hott def and (i : I) : Path A a (p @ i) := <j> p @ i ∧ j
-hott def or  (i : I) : Path A (p @ i) b := <j> p @ i ∨ j
+hott definition and (i : I) : Path A a (p @ i) := <j> p @ i ∧ j
+hott definition or  (i : I) : Path A (p @ i) b := <j> p @ i ∨ j
 
-end GroundZero.Cubical.Connection
+end GroundZero.Cubical.Connection

GroundZero/Cubical/Cubes.lean

@@ -10,23 +10,23 @@ open GroundZero.HITs.Interval (i₀ i₁ seg)
 namespace GroundZero.Cubical
 universe u v w r
 
-def binary (A : Type u) : ℕ → Type u
+hott definition binary (A : Type u) : ℕ → Type u
 | Nat.zero   => A × A
 | Nat.succ n => binary A n × binary A n
 
 -- cube n represents (n + 1)-cube.
-hott def cube (A : Type u) : ℕ → Type u
+hott definition cube (A : Type u) : ℕ → Type u
 | Nat.zero   => I → A
 | Nat.succ n => I → cube A n
 
-hott def cube.tree {A : Type u} : Π {n : ℕ}, cube A n → binary A n
+hott definition cube.tree {A : Type u} : Π {n : ℕ}, cube A n → binary A n
 | Nat.zero,   f => (f 0, f 1)
 | Nat.succ n, f => (tree (f 0), tree (f 1))
 
 inductive Cube {A : Type u} (n : ℕ) : binary A n → Type u
 | lam (f : cube A n) : Cube n (cube.tree f)
 
-def Cube.lambda {A : Type u} (n : ℕ) (f : cube A n) : Cube n (cube.tree f) :=
+hott definition Cube.lambda {A : Type u} (n : ℕ) (f : cube A n) : Cube n (cube.tree f) :=
 Cube.lam f
 
 /-
@@ -37,16 +37,16 @@ Cube.lam f
      |         |
      a ------> b
 -/
-hott def Square {A : Type u} (a b c d : A) :=
+hott definition Square {A : Type u} (a b c d : A) :=
 Cube 1 ((a, b), (c, d))
 
-def Square.lam {A : Type u} (f : I → I → A) :
+hott definition Square.lam {A : Type u} (f : I → I → A) :
   Square (f 0 0) (f 0 1) (f 1 0) (f 1 1) :=
 @Cube.lam A 1 f
 
-hott def Square.rec {A : Type u} {C : Π (a b c d : A), Square a b c d → Type v}
+hott definition Square.rec {A : Type u} {C : Π (a b c d : A), Square a b c d → Type v}
   (H : Π (f : I → I → A), C (f 0 0) (f 0 1) (f 1 0) (f 1 1) (Square.lam f))
   {a b c d : A} (τ : Square a b c d) : C a b c d τ :=
 @Cube.casesOn A 1 (λ w, C w.1.1 w.1.2 w.2.1 w.2.2) ((a, b), (c, d)) τ H
 
-end GroundZero.Cubical
+end GroundZero.Cubical

GroundZero/HITs/Flattening.lean

@@ -13,27 +13,27 @@ section
   variable {A : Type u} {B : Type v} (f g : A → B)
            (C : B → Type w) (D : Π x, C (f x) ≃ C (g x))
 
-  def Flattening := @Coeq (Σ x, C (f x)) (Σ x, C x)
+  hott definition Flattening := @Coeq (Σ x, C (f x)) (Σ x, C x)
     (λ w, ⟨f w.1, w.2⟩) (λ w, ⟨g w.1, (D w.1).1 w.2⟩)
 
-  hott def P : Coeq f g → Type w :=
+  hott definition P : Coeq f g → Type w :=
   Coeq.rec (Type w) C (λ x, ua (D x))
 end
 
 namespace Flattening
   variable {A : Type u} {B : Type v} {f g : A → B}
            {C : B → Type w} {D : Π x, C (f x) ≃ C (g x)}
 
-  hott def iota (x : B) (c : C x) : Flattening f g C D :=
+  hott definition iota (x : B) (c : C x) : Flattening f g C D :=
   Coeq.iota ⟨x, c⟩
 
-  hott def resp (x : A) (y : C (f x)) : @Id (Flattening f g C D) (iota (f x) y) (iota (g x) ((D x).1 y)) :=
+  hott definition resp (x : A) (y : C (f x)) : @Id (Flattening f g C D) (iota (f x) y) (iota (g x) ((D x).1 y)) :=
   @Coeq.resp (Σ x, C (f x)) (Σ x, C x) (λ w, ⟨f w.1, w.2⟩) (λ w, ⟨g w.1, (D w.1).1 w.2⟩) ⟨x, y⟩
 
-  hott def iotaφ : Π x, C x → Σ x, P f g C D x :=
+  hott definition iotaφ : Π x, C x → Σ x, P f g C D x :=
   λ x y, ⟨Coeq.iota x, y⟩
 
-  noncomputable hott def respφ (x : A) (y : C (f x)) :
+  noncomputable hott definition respφ (x : A) (y : C (f x)) :
     @Id (Σ x, P f g C D x) (iotaφ (f x) y) (iotaφ (g x) ((D x).1 y)) :=
   begin
     fapply Sigma.prod; apply Coeq.resp;
@@ -42,7 +42,7 @@ namespace Flattening
     apply Coeq.recβrule (Type w) C (λ x, ua (D x)) x; apply uaβ
   end
 
-  hott def sec : Flattening f g C D → Σ x, P f g C D x :=
+  hott definition sec : Flattening f g C D → Σ x, P f g C D x :=
   begin fapply Coeq.rec; intro w; apply iotaφ w.1 w.2; intro w; apply respφ w.1 w.2 end
 end Flattening
 

GroundZero/HITs/Int.lean

@@ -11,19 +11,19 @@ open GroundZero
 
 namespace GroundZero.HITs
 
-hott def Int.rel (w₁ w₂ : ℕ × ℕ) : Type :=
+hott definition Int.rel (w₁ w₂ : ℕ × ℕ) : Type :=
 w₁.1 + w₂.2 = w₁.2 + w₂.1
 
-hott def Int := Quotient Int.rel
+hott definition Int := Quotient Int.rel
 local notation "ℤ" => Int
 
 namespace Nat.Product
-  def add (x y : ℕ × ℕ) : ℕ × ℕ :=
+  hott definition add (x y : ℕ × ℕ) : ℕ × ℕ :=
   (x.1 + y.1, x.2 + y.2)
 
   instance : Add (ℕ × ℕ) := ⟨add⟩
 
-  def mul (x y : ℕ × ℕ) : ℕ × ℕ :=
+  hott definition mul (x y : ℕ × ℕ) : ℕ × ℕ :=
   (x.1 * y.1 + x.2 * y.2, x.1 * y.2 + x.2 * y.1)
 
   instance : Mul (ℕ × ℕ) := ⟨mul⟩
@@ -32,31 +32,31 @@ end Nat.Product
 namespace Int
   universe u v
 
-  def mk : ℕ × ℕ → ℤ := Quotient.elem
-  def elem (a b : ℕ) : ℤ := Quotient.elem (a, b)
+  hott definition mk : ℕ × ℕ → ℤ := Quotient.elem
+  hott definition elem (a b : ℕ) : ℤ := Quotient.elem (a, b)
 
-  def pos (n : ℕ) := mk (n, 0)
+  hott definition pos (n : ℕ) := mk (n, 0)
   instance (n : ℕ) : OfNat ℤ n := ⟨pos n⟩
 
-  def neg (n : ℕ) := mk (0, n)
+  hott definition neg (n : ℕ) := mk (0, n)
 
-  hott def glue {a b c d : ℕ} (H : a + d = b + c) : mk (a, b) = mk (c, d) :=
+  hott definition glue {a b c d : ℕ} (H : a + d = b + c) : mk (a, b) = mk (c, d) :=
   Quotient.line H
 
-  hott def ind {C : ℤ → Type u} (mkπ : Π x, C (mk x))
+  hott definition ind {C : ℤ → Type u} (mkπ : Π x, C (mk x))
     (glueπ : Π {a b c d : ℕ} (H : a + d = b + c),
       mkπ (a, b) =[glue H] mkπ (c, d)) (x : ℤ) : C x :=
   begin fapply Quotient.ind; exact mkπ; intros x y H; apply glueπ end
 
-  hott def rec {C : Type u} (mkπ : ℕ × ℕ → C)
+  hott definition rec {C : Type u} (mkπ : ℕ × ℕ → C)
     (glueπ : Π {a b c d : ℕ} (H : a + d = b + c),
       mkπ (a, b) = mkπ (c, d)) : ℤ → C :=
   begin fapply Quotient.rec; exact mkπ; intros x y H; apply glueπ H end
 
   instance : Neg Int :=
   ⟨rec (λ x, mk ⟨x.2, x.1⟩) (λ H, glue H⁻¹)⟩
 
-  hott def addRight (a b k : ℕ) : mk (a, b) = mk (a + k, b + k) :=
+  hott definition addRight (a b k : ℕ) : mk (a, b) = mk (a + k, b + k) :=
   begin
     apply glue; transitivity; symmetry; apply Theorems.Nat.assoc;
     symmetry; transitivity; symmetry; apply Theorems.Nat.assoc;

GroundZero/HITs/Suspension.lean

@@ -13,7 +13,7 @@ open GroundZero.Types
 namespace GroundZero
 namespace HITs
 
-def Suspension.{u} (A : Type u) :=
+hott definition Suspension.{u} (A : Type u) :=
 @Pushout.{0, 0, u} 𝟏 𝟏 A (λ _, ★) (λ _, ★)
 
 notation "∑ " => Suspension
@@ -22,33 +22,33 @@ namespace Suspension
   -- https://github.com/leanprover/lean2/blob/master/hott/homotopy/susp.hlean
   universe u v
 
-  hott def north {A : Type u} : ∑ A := Pushout.inl ★
-  hott def south {A : Type u} : ∑ A := Pushout.inr ★
+  hott definition north {A : Type u} : ∑ A := Pushout.inl ★
+  hott definition south {A : Type u} : ∑ A := Pushout.inr ★
 
-  hott def merid {A : Type u} (x : A) : @Id (∑ A) north south :=
+  hott definition merid {A : Type u} (x : A) : @Id (∑ A) north south :=
   Pushout.glue x
 
-  hott def ind {A : Type u} {B : ∑ A → Type v} (n : B north) (s : B south)
+  hott definition ind {A : Type u} {B : ∑ A → Type v} (n : B north) (s : B south)
     (m : Π x, n =[merid x] s) : Π x, B x :=
   Pushout.ind (λ ★, n) (λ ★, s) m
 
   attribute [eliminator] ind
 
-  hott def rec {A : Type u} {B : Type v} (n s : B) (m : A → n = s) : ∑ A → B :=
+  hott definition rec {A : Type u} {B : Type v} (n s : B) (m : A → n = s) : ∑ A → B :=
   Pushout.rec (λ _, n) (λ _, s) m
 
-  hott def indβrule {A : Type u} {B : ∑ A → Type v}
+  hott definition indβrule {A : Type u} {B : ∑ A → Type v}
     (n : B north) (s : B south) (m : Π x, n =[merid x] s) (x : A) :
     apd (ind n s m) (merid x) = m x :=
   by apply Pushout.indβrule
 
-  hott def recβrule {A : Type u} {B : Type v} (n s : B)
+  hott definition recβrule {A : Type u} {B : Type v} (n s : B)
     (m : A → n = s) (x : A) : ap (rec n s m) (merid x) = m x :=
   by apply Pushout.recβrule
 
   instance (A : Type u) : isPointed (∑ A) := ⟨north⟩
 
-  hott def σ {A : Type u} [isPointed A] : A → Ω¹(∑ A) :=
+  hott definition σ {A : Type u} [isPointed A] : A → Ω¹(∑ A) :=
   λ x, merid x ⬝ (merid (pointOf A))⁻¹
 
   hott lemma σComMerid {A : Type u} [isPointed A] (x : A) : σ x ⬝ merid (pointOf A) = merid x :=

GroundZero/HITs/Wedge.lean

@@ -14,30 +14,30 @@ namespace HITs
 
 universe u
 
-def Wedge (A B : Type⁎) :=
+hott definition Wedge (A B : Type⁎) :=
 @Pushout.{_, _, 0} A.1 B.1 𝟏 (λ _, A.2) (λ _, B.2)
 
 infix:50 " ∨ " => Wedge
 
 namespace Wedge
   variable {A B : Type⁎}
 
-  def inl : A.1 → A ∨ B := Pushout.inl
-  def inr : B.1 → A ∨ B := Pushout.inr
+  hott definition inl : A.1 → A ∨ B := Pushout.inl
+  hott definition inr : B.1 → A ∨ B := Pushout.inr
 
-  hott def glue : inl A.2 = inr B.2 :=
+  hott definition glue : inl A.2 = inr B.2 :=
   Pushout.glue ★
 
-  hott def ind {C : A ∨ B → Type u} (inlπ : Π x, C (inl x)) (inrπ : Π x, C (inr x))
+  hott definition ind {C : A ∨ B → Type u} (inlπ : Π x, C (inl x)) (inrπ : Π x, C (inr x))
     (glueπ : inlπ A.2 =[glue] inrπ B.2) : Π x, C x :=
   Pushout.ind inlπ inrπ (λ ★, glueπ)
 
   attribute [eliminator] ind
 
-  hott def rec {C : Type u} (inlπ : A.1 → C) (inrπ : B.1 → C)
+  hott definition rec {C : Type u} (inlπ : A.1 → C) (inrπ : B.1 → C)
     (glueπ : inlπ A.2 = inrπ B.2) : A ∨ B → C :=
   Pushout.rec inlπ inrπ (λ ★, glueπ)
 end Wedge
 
 end HITs
-end GroundZero
+end GroundZero