From 30725d71b6552d97882626cdcfcb0d202613ca54 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Tue, 20 Mar 2018 11:58:54 +0100
Subject: [PATCH] [WIP] Scary goal

---
 src/Cat/Categories/Sets.agda | 19 +++++++++++++++++--
 1 file changed, 17 insertions(+), 2 deletions(-)

diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index cc3d655..1e92b60 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -28,10 +28,21 @@ sym≃ = Equivalence.symmetry
 infixl 10 _⊙_
 
 module _ {ℓ : Level} {A : Set ℓ} {a : A} where
+  -- "This follows from the propositional equiality for `J`" - Vezzosi.
   id-coe : coe refl a ≡ a
   id-coe = begin
-    coe refl a ≡⟨ {!!} ⟩
+    coe refl a                 ≡⟨⟩
+    -- pathJprop : pathJ _ refl ≡ d
+    pathJ (λ y x → A) scary A refl ≡⟨ pathJprop {x = scary} (λ y x → A) scary ⟩
+    scary ≡⟨ {!!} ⟩
+    -- pathJ (λ y x → A) scary A refl ≡⟨ pathJprop {A = A} (λ y x → A) scary ⟩
+    -- scary ≡⟨ {!!} ⟩
+
+    -- pathJ (λ y _ → B _ → B y) (λ x → x) _ p ≡⟨ {!!} ⟩
     a ∎
+    where
+    scary : A
+    scary = (primComp (λ j → A) i0 (λ j → p[ a ] i0 (~ j)) a)
 
 module _ {ℓ : Level} {A B : Set ℓ} {a : A} where
   inv-coe : (p : A ≡ B) → coe (sym p) (coe p a) ≡ a
@@ -225,7 +236,11 @@ module _ (ℓ : Level) where
           h = sym≃ (univalence {A = A} {B})
           k : Σ _ (isEquiv (A ≃ B) (A ≡ B))
           k = Eqv.doEta h
-        in {!!}
+          eqv : Σ (A → B) (isEquiv A B) Eqv.≅ (A ≃ B)
+          eqv = {!!} , {!!} , {!!}
+          hh : Σ (A → B) (isEquiv A B) ≃ (A ≃ B)
+          hh = Eeq.fromIsomorphism eqv
+        in hh ⊙ h
 
       -- lem2 with propIsSet
       step2 : (A ≡ B) ≃ (hA ≡ hB)