From e25f50f6604052defe6ebea227a163fb6f9d10d5 Mon Sep 17 00:00:00 2001 From: Siegmentation Fault Date: Thu, 16 Nov 2023 20:05:35 +0700 Subject: [PATCH] formatting --- GroundZero/Types/Equiv.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/GroundZero/Types/Equiv.lean b/GroundZero/Types/Equiv.lean index 4633fab..99571a4 100644 --- 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⟩)⟩