From d5eee8e7e0d29f3a2c89c3602bbdfc8f7e3730d3 Mon Sep 17 00:00:00 2001
From: Siegmentation Fault <siegmentationfault@yandex.ru>
Date: Sun, 5 Nov 2023 00:05:53 +0700
Subject: [PATCH] windRev

---
 GroundZero/HITs/Circle.lean | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

diff --git a/GroundZero/HITs/Circle.lean b/GroundZero/HITs/Circle.lean
index d1de0d9..33dd81b 100644
--- a/GroundZero/HITs/Circle.lean
+++ b/GroundZero/HITs/Circle.lean
@@ -139,15 +139,18 @@ namespace Circle
   def base₁ : S¹ := Suspension.north
   def base₂ : S¹ := Suspension.south
 
-  def seg₁ : base₁ = base₂ := Suspension.merid false
-  def seg₂ : base₁ = base₂ := Suspension.merid true
+  hott def seg₁ : base₁ = base₂ := Suspension.merid false
+  hott def seg₂ : base₁ = base₂ := Suspension.merid true
 
   hott def ind₂ {B : S¹ → Type u} (b₁ : B base₁) (b₂ : B base₂)
     (ℓ₁ : b₁ =[seg₁] b₂) (ℓ₂ : b₁ =[seg₂] b₂) : Π x, B x :=
   Suspension.ind b₁ b₂ (λ | false => ℓ₁ | true => ℓ₂)
 
-  def base : S¹ := base₁
-  def loop : base = base := seg₂ ⬝ seg₁⁻¹
+  hott def base : S¹ := base₁
+  hott def loop : base = base := seg₂ ⬝ seg₁⁻¹
+
+  abbrev loop₁ : base₁ = base₁ := loop
+  hott def loop₂ : base₂ = base₂ := seg₁⁻¹ ⬝ seg₂
 
   hott def rec {B : Type u} (b : B) (ℓ : b = b) : S¹ → B :=
   Suspension.rec b b (λ | false => idp b | true => ℓ)
@@ -755,6 +758,9 @@ namespace Circle
       symmetry; apply powerOfWinding; apply powerRev
     end
 
+    noncomputable hott corollary windRev : Π {x : S¹} (p : x = x), wind x p⁻¹ = -(wind x p) :=
+    begin fapply indΩ; apply windingRev; intro; apply piProp; intro; apply Integer.set end
+
     noncomputable hott lemma windingMult : Π (p q : Ω¹(S¹)), winding (mult p q) = winding p * winding q :=
     begin
       intro p; fapply Ωind₁;