iso-J has the same structure as equiv-J

lib/foundations/univalent/iso.anders

@@ -76,16 +76,33 @@ def isoToEquiv (A B : U) (f : A -> B) (g : B -> A)
 -- [Cohen, Coquand, Huber, Mörtberg] 2016
 
 def iso (A B: U) : U :=
-  Σ (f : A -> B) (g : B -> A)
+  Σ (f : A -> B)
+    (g : B -> A)
     (s : section A B f g)
-    (t : retract A B f g), unit
-
-def iso-intro (A: U) : iso A A := (id A, id A, (\(x:A), <_>x), (\(x:A), <_>x), star)
-
-axiom iso-J (A B: U) (C : Π (A B : U) (f: A → B) (g: B → A), U)
-    (d : C A A (id A) (id A))
-    (f : A → B) (g : B → A) (s: section A B f g) (t: retract A B f g)
-  : C A B f g
+    (t : retract A B f g),
+    𝟏
+
+def iso-intro (A: U)
+  : iso A A
+ := ( id A,
+      id A,
+      (\(x:A), <_>x),
+      (\(x:A), <_>x),
+      ★
+    )
+
+def iso-single (B : U) : U := Σ (A: U), iso A B
+def iso-EquivIsContr (B: U) : isContr (iso-single B) := ?
+def iso-isContr→isProp (A: U) (w: isContr A) (a b : A) : Path A a b
+ := <i> hcomp A (∂ i) (λ (j : I), [(i = 0) → a, (i = 1) → (w.2 b) @ j])
+                      ((<i4> w.2 a @ -i) @ i)
+def iso-contrSinglEquiv (A B : U) (e : iso A B)
+  : Path (iso-single B) (B,iso-intro B) (A,e)
+ := isContr→isProp (iso-single B) (iso-EquivIsContr B) (B,iso-intro B) (A,e)
+def iso-J (A B: U) (P: Π (A B: U), iso A B → U) (r: P B B (iso-intro B))
+  : Π (e: iso A B), P A B e
+ := λ (e: iso A B), subst (iso-single B) (\ (z: iso-single B), P z.1 B z.2)
+                            (B,iso-intro B) (A,e) (iso-contrSinglEquiv A B e) r
 
 def iso→Path (A B : U) (f : A -> B) (g : B -> A)
     (s : Π (y : B), Path B (f (g y)) y)