From 74669bee03c2df5bf906253d7530b5c8c2e3ed24 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Tue, 22 Nov 2022 16:56:52 -0600
Subject: [PATCH] identity proof

---
 src/Lemma641.agda | 43 +++++++++++++++++++++++++++++++++++++------
 1 file changed, 37 insertions(+), 6 deletions(-)

diff --git a/src/Lemma641.agda b/src/Lemma641.agda
index 0b473e7..d4fa160 100644
--- a/src/Lemma641.agda
+++ b/src/Lemma641.agda
@@ -4,9 +4,9 @@ module Lemma641 where
 
 open import Level
 open import Cubical.Foundations.Prelude 
-  using (_≡_; refl; _∙_; _≡⟨⟩_; _≡⟨_⟩_; _∎; cong; sym; fst; snd; _,_; ~_)
+  using (_≡_; refl; _∙_; _≡⟨_⟩_; _∎; cong; sym; fst; snd; _,_; ~_)
 open import Cubical.Data.Empty as ⊥
-open import Cubical.Foundations.Equiv using (isEquiv; equiv-proof)
+open import Cubical.Foundations.Equiv using (isEquiv; equivProof; equiv-proof)
 open import Relation.Nullary using (¬_)
 open import Relation.Binary.Core using (Rel)
 
@@ -29,9 +29,40 @@ bool-id≡bool : (b : Bool) → bool-id b ≡ b
 bool-id≡bool true _ = true
 bool-id≡bool false _ = false
 
+-- record isEquiv {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) : Set (ℓ ⊔ ℓ') where
+--   no-eta-equality
+--   field
+--     equiv-proof : (y : B) → isContr (fiber f y)
+
+--  isEquiv bool-id
+--    A = Bool
+--    B = Bool
+--    f : Bool → Bool
+--  equiv-proof : (y : B = Bool) → isContr (fiber f y)
+
+--  fiber : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) (y : B) → Set (ℓ ⊔ ℓ')
+--  fiber {A = A} f y = Σ A \ x → f x ≡ y
+--  fiber f y
+--    f : Bool → Bool
+--    A = Bool
+--    B = Bool
+--    y : Bool = y
+--  fiber f y = Σ Bool \ x → f x ≡ y
+
+--  isContr : ∀ {ℓ} → Set ℓ → Set ℓ
+--  isContr A = Σ A \ x → (∀ y → x ≡ y)
+--  isContr (Σ Bool \ x → f x ≡ y)
+--    = Σ (Σ Bool \ x → f x ≡ y) \ x → (∀ y → x ≡ y)
+--
+--    .fst = (x , f x ≡ y)
+--    .snd = (∀ y → .fst ≡ y)
+
 bool-id-is-equiv : isEquiv bool-id
-bool-id-is-equiv .equiv-proof y .fst = ( y , bool-id≡bool y )
-bool-id-is-equiv .equiv-proof y .snd (y′ , p) i = let b = p (~ i) in (? , bool-id≡bool y)
+bool-id-is-equiv .equiv-proof y = ?
+-- First is an element of bool-id ≡ bool
+-- bool-id-is-equiv .equiv-proof y .fst = ( y , bool-id≡bool y )
+-- -- Second is a proof that any other inhabitant of bool-id ≡ bool is the same as the above
+-- bool-id-is-equiv .equiv-proof y .snd = ?
 
 bool-flip : Bool → Bool
 bool-flip true = false
@@ -80,8 +111,8 @@ consequence x p loop≡refl = p
     refl-x x
   ∎
 
-lemma641 : loop ≢ refl
-lemma641 x = ?
+-- lemma641 : loop ≢ refl
+-- lemma641 x = ?
 
 -- https://serokell.io/blog/playing-with-negation