naming

forked-from-1kasper · Oct 18, 2024 · 39044da · 39044da
1 parent 6f4ff30
commit 39044da
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 7 deletions.
diff --git a/GroundZero/HITs/Circle.lean b/GroundZero/HITs/Circle.lean
@@ -245,11 +245,11 @@ namespace Circle
   hott definition succ (l : Ω¹(S¹)) : Ω¹(S¹) := l ⬝ loop
   hott definition pred (l : Ω¹(S¹)) : Ω¹(S¹) := l ⬝ loop⁻¹
 
-  hott abbreviation zero   := idp base
-  hott abbreviation one    := succ zero
-  hott abbreviation two    := succ one
-  hott abbreviation three  := succ two
-  hott abbreviation fourth := succ three
+  hott abbreviation zero  := idp base
+  hott abbreviation one   := succ zero
+  hott abbreviation two   := succ one
+  hott abbreviation three := succ two
+  hott abbreviation four  := succ three
 
   hott definition helix : S¹ → Type :=
   rec ℤ (ua Integer.succEquiv)

diff --git a/GroundZero/Theorems/Univalence.lean b/GroundZero/Theorems/Univalence.lean
@@ -182,9 +182,9 @@ begin
   apply univalence; apply propEquivProp G
 end
 
-noncomputable hott theorem propsetIsSet : hset propset :=
+noncomputable hott theorem propsetIsSet : hset (Prop u) :=
 begin
-  intro ⟨x, H⟩ ⟨y, G⟩; apply transport (λ π, Π (p q : π), p = q);
+  intro ⟨x, H⟩ ⟨y, G⟩; apply transport (λ X, Π (p q : X), p = q);
   symmetry; apply ua; apply Sigma.sigmaPath;
   intro ⟨p, p'⟩ ⟨q, q'⟩; fapply Sigma.prod;
   { apply propEqProp; exact G };