From 39044dae1b039208c372afb92f4b20633646d7ed Mon Sep 17 00:00:00 2001 From: Siegmentation Fault Date: Fri, 18 Oct 2024 18:19:11 +0700 Subject: [PATCH] naming --- GroundZero/HITs/Circle.lean | 10 +++++----- GroundZero/Theorems/Univalence.lean | 4 ++-- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/GroundZero/HITs/Circle.lean b/GroundZero/HITs/Circle.lean index 5d5af45..14d97fe 100644 --- 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 index 6ea76d2..dcc9363 100644 --- 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 };