add a 'beta' for the fundamental thm of id

agda · Dec 7, 2022 · ddb192d · ddb192d
1 parent b2a0c41
commit ddb192d
Showing 1 changed file with 8 additions and 0 deletions.
diff --git a/Cubical/Foundations/Equiv/Fiberwise.agda b/Cubical/Foundations/Equiv/Fiberwise.agda
@@ -89,3 +89,11 @@ fundamentalTheoremOfId : {A : Type ℓ} (Eq : A → A → Type ℓ')
   → ((x : A) → isContr (Σ[ y ∈ A ] Eq x y))
   → (x y : A) → (x ≡ y) ≃ (Eq x y)
 fundamentalTheoremOfId Eq eqRefl eqContr x = recognizeId (Eq x) (eqRefl x) (eqContr x)
+
+fundamentalTheoremOfIdβ :
+  {A : Type ℓ} (Eq : A → A → Type ℓ')
+  → (eqRefl : (x : A) → Eq x x)
+  → (eqContr : (x : A) → isContr (Σ[ y ∈ A ] Eq x y))
+  → (x : A)
+  → fst (fundamentalTheoremOfId Eq eqRefl eqContr x x) refl ≡ eqRefl x
+fundamentalTheoremOfIdβ Eq eqRefl eqContr x = JRefl (λ y p → Eq x y) (eqRefl x)