formatting

forked-from-1kasper · Nov 16, 2023 · e25f50f · e25f50f
1 parent fb39839
commit e25f50f
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/GroundZero/Types/Equiv.lean b/GroundZero/Types/Equiv.lean
@@ -82,11 +82,11 @@ namespace Equiv
   hott def forward {A : Type u} {B : Type v} (e : A ≃ B) : A → B := e.fst
   instance forwardCoe {A : Type u} {B : Type v} : CoeFun (A ≃ B) (λ _, A → B) := ⟨forward⟩
 
-  hott def left {A : Type u} {B : Type v} (e : A ≃ B) : B → A := e.2.1.1
+  hott def left  {A : Type u} {B : Type v} (e : A ≃ B) : B → A := e.2.1.1
   hott def right {A : Type u} {B : Type v} (e : A ≃ B) : B → A := e.2.2.1
 
-  hott def leftForward {A : Type u} {B : Type v} (e : A ≃ B) : e.left ∘ e.forward ~ id := e.2.1.2
-  hott def forwardRight {A : Type u} {B : Type v} (e : A ≃ B) : e.forward ∘ e.right ~ id := e.2.2.2
+  hott def leftForward  {A : Type u} {B : Type v} (e : A ≃ B) : e.left    ∘ e.forward ~ id := e.2.1.2
+  hott def forwardRight {A : Type u} {B : Type v} (e : A ≃ B) : e.forward ∘ e.right   ~ id := e.2.2.2
 
   hott def ideqv (A : Type u) : A ≃ A :=
   ⟨idfun, (⟨idfun, idp⟩, ⟨idfun, idp⟩)⟩