From e9d44924d2fe780947cf8b49f3f318eb788479d9 Mon Sep 17 00:00:00 2001
From: loic-p <loic.pujet@ens.fr>
Date: Sat, 10 Oct 2020 17:15:36 +0200
Subject: [PATCH] Improve contractibility of singletons, split files

---
 _CoqProject                |   5 +-
 theories/category.v        | 135 ++++++---
 theories/funext.v          | 509 +++++++++++++++++++++++++++++++++
 theories/singletons.v      | 225 +++++++++++++++
 theories/translation_fib.v | 572 ++++++++++---------------------------
 theories/transport.v       | 304 ++++++++++++++++++++
 theories/univalence.v      |  38 +++
 7 files changed, 1329 insertions(+), 459 deletions(-)
 create mode 100644 theories/funext.v
 create mode 100644 theories/singletons.v
 create mode 100644 theories/transport.v
 create mode 100644 theories/univalence.v

diff --git a/_CoqProject b/_CoqProject
index a9de5bc..e99fe38 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -2,4 +2,7 @@
 
 theories/category.v
 theories/translation_fib.v
-theories/translation_fib_path.v
\ No newline at end of file
+theories/transport.v
+theories/singletons.v
+theories/univalence.v
+theories/funext.v
\ No newline at end of file
diff --git a/theories/category.v b/theories/category.v
index e6ce27b..c6d3a10 100644
--- a/theories/category.v
+++ b/theories/category.v
@@ -213,28 +213,28 @@ Notation "α · x" := (fun r β => x r (α ∘ β)) (at level 40).
 
 Definition side_0 {p : ℙ} : p ≤ S p.
 Proof.
-unshelve refine (mkCubeArr _ _ _ _).
-- unshelve refine (fun c n => _).
-  destruct n as [n nε]. destruct n as [|n'].
+unshelve econstructor.
+- unshelve refine (fun c => _).
+  refine (finmatch (fun _ => bool) _ _).
   + exact false.
-  + apply c. unshelve refine (mkFinset p n' _).
-    apply le_to_sle. apply le_S_n. apply sle_to_le. exact nε.
-- intros c d Hcd n. destruct n as [n nε]. destruct n.
+  + refine (fun n => c n).
+- intros c d Hcd.
+  refine (sfinmatch _ _ _) ; simpl.
   + exact sI.
-  + refine (Hcd _).
+  + refine (fun n => _). refine (Hcd _).
 Defined.
 
 Definition side_1 {p : ℙ} : p ≤ S p.
 Proof.
-unshelve refine (mkCubeArr _ _ _ _).
-- unshelve refine (fun c n => _).
-  destruct n as [n nε]. destruct n as [|n'].
+unshelve econstructor.
+- unshelve refine (fun c => _).
+  refine (finmatch (fun _ => bool) _ _).
   + exact true.
-  + apply c. unshelve refine (mkFinset p n' _).
-    apply le_to_sle. apply le_S_n. apply sle_to_le. exact nε.
-- intros c d Hcd n. destruct n as [n nε]. destruct n.
+  + refine (fun n => c n).
+- intros c d Hcd.
+  refine (sfinmatch _ _ _) ; simpl.
   + exact sI.
-  + refine (Hcd _).
+  + refine (fun n => _). refine (Hcd _).
 Defined.
 
 Definition squish {p : ℙ} : S p ≤ p.
@@ -256,18 +256,16 @@ Defined.
 Definition promote {p q : ℙ} (α : q ≤ p) : S q ≤ S p.
 Proof.
 unshelve refine (mkCubeArr _ _ _ _).
-- unshelve refine (fun c n => _).
-  destruct n as [n nε]. destruct n as [| n'].
-  + apply c. exact finzero.
-  + destruct α as [α αε]. apply α.
-    * refine (fun n => _). apply c. apply finsucc. exact n.
-    * unshelve refine (mkFinset p n' _).
-      apply le_to_sle. apply le_S_n. apply sle_to_le. exact nε.
-- intros c d Hcd n.
-  destruct n as [n nε]. destruct n as [| n'].
+- unshelve refine (fun c => _).
+  refine (finmatch (fun _ => bool) _ _).
+  + exact (c finzero).
+  + apply (arr α).
+    refine (fun n => c (finsucc n)).
+- intros c d Hcd.
+  refine (sfinmatch _ _ _) ; simpl.
   + eapply Hcd.
-  + destruct α as [α αε]. eapply αε.
-    unfold le_cube. intro m. eapply Hcd.
+  + eapply (eps_arr α). 
+    refine (fun m => _). eapply Hcd.
 Defined.
 
 Definition merge {p q : ℙ} (α : q ≤ p) (β : q ≤ 1) : q ≤ S p.
@@ -283,6 +281,36 @@ unshelve econstructor.
   + refine (fun n => α.(eps_arr) c d Hcd n).
 Defined.
 
+Definition vee {p : ℙ} : S (S p) ≤ S p.
+Proof.
+unshelve econstructor.
+- refine (fun c => _).
+  refine (finmatch (fun _ => bool) _ _).
+  + exact (orb (c finzero) (c (finsucc finzero))).
+  + refine (fun n' => _).
+    exact (c (finsucc (finsucc n'))).
+- intros c d Hcd.
+  refine (sfinmatch _ _ _) ; simpl.
+  + pose proof (Hcd finzero) as H0. pose proof (Hcd (finsucc finzero)) as H1.
+    revert H0 H1. destruct (c finzero) ; destruct (c (finsucc finzero)) ; destruct (d finzero) ; destruct (d (finsucc finzero)) ; simpl ; easy.
+  + refine (fun n => _). eapply Hcd.
+Defined.
+
+Definition wedge {p : ℙ} : S (S p) ≤ S p.
+Proof.
+unshelve econstructor.
+- refine (fun c => _).
+  refine (finmatch (fun _ => bool) _ _).
+  + exact (andb (c finzero) (c (finsucc finzero))).
+  + refine (fun n' => _).
+    exact (c (finsucc (finsucc n'))).
+- intros c d Hcd.
+  refine (sfinmatch _ _ _) ; simpl.
+  + pose proof (Hcd finzero) as H0. pose proof (Hcd (finsucc finzero)) as H1.
+    revert H0 H1. destruct (c finzero) ; destruct (c (finsucc finzero)) ; destruct (d finzero) ; destruct (d (finsucc finzero)) ; simpl ; easy.
+  + refine (fun n => _). eapply Hcd.
+Defined.
+
 (* All of the following hold definitionally *)
 
 Lemma arrow_eq_0 {p : ℙ} : (@squish p) ∘ side_0 = !.
@@ -325,16 +353,60 @@ Proof.
 reflexivity.
 Defined.
 
-(* this one, however, requires η for nat. 
+Lemma arrow_eq_7 {p : ℙ} : squish ∘ squish ≡ squish ∘ (@wedge p).
+Proof.
+reflexivity.
+Defined.
+
+Lemma arrow_eq_8 {p : ℙ} : squish ∘ squish ≡ squish ∘ (@vee p).
+Proof.
+reflexivity.
+Defined.
+
+(* these ones, however, requires η for nat. 
   without it, we can only get an extensional equality. tough luck *)
 
-Lemma arrow_eq_fail {p q : ℙ} (α : q ≤ S p) : 
+Lemma arrow_eq_fail1 {p q : ℙ} (α : q ≤ S p) : 
   forall c n, (merge (squish ∘ α) (antisquish ∘ α)).(arr) c n ≡ α.(arr) c n.
 Proof.
 refine (fun c n => _). revert n.
 refine (sfinmatch _ _ _) ; reflexivity.
 Defined.
 
+Lemma arrow_eq_fail2 {p : ℙ} : 
+  forall c n, (wedge ∘ (@side_1 (S p))).(arr) c n ≡ !.(arr) c n.
+Proof.
+refine (fun c n => _). revert n.
+refine (sfinmatch _ _ _) ; reflexivity.
+Defined.
+
+Lemma arrow_eq_fail3 {p : ℙ} : 
+  forall c n, (wedge ∘ (@side_0 (S p))).(arr) c n ≡ (side_0 ∘ squish).(arr) c n.
+Proof.
+refine (fun c n => _). revert n.
+refine (sfinmatch _ _ _) ; reflexivity.
+Defined.
+
+Lemma arrow_eq_fail4 {p : ℙ} : 
+  forall c n, (wedge ∘ (promote (@side_1 p))).(arr) c n ≡ !.(arr) c n.
+Proof.
+refine (fun c n => _). revert n.
+refine (sfinmatch _ _ _).
+- unfold vee ; unfold promote ; unfold side_1 ; simpl. 
+  destruct (c finzero) ; easy.
+- easy.
+Defined.
+
+Lemma arrow_eq_fail5 {p : ℙ} : 
+  forall c n, (wedge ∘ (promote (@side_0 p))).(arr) c n ≡ (side_0 ∘ squish).(arr) c n.
+Proof.
+refine (fun c n => _). revert n.
+refine (sfinmatch _ _ _).
+- unfold vee ; unfold promote ; unfold side_0 ; simpl. 
+  destruct (c finzero) ; easy.
+- easy.
+Defined.
+
 (* Axioms for interval-types, à la CubicalTT *)
 
 Definition i0 {p} : p ≤ 1.
@@ -351,15 +423,6 @@ unshelve econstructor.
 - refine (fun c d Hcd n => _). easy.
 Defined.
 
-Definition is_i0 {p} : p ≤ 1 -> bool.
-Admitted.
-
-Definition is_i0_i0 {p} : is_i0 (@i0 p) ≡ true.
-Admitted.
-
-Definition is_i0_i1 {p} : is_i0 (@i1 p) ≡ false.
-Admitted.
-
 Definition itype (p : ℙ) (A : Type) (x y : A) : Type.
 Admitted.
 
diff --git a/theories/funext.v b/theories/funext.v
new file mode 100644
index 0000000..a6feae5
--- /dev/null
+++ b/theories/funext.v
@@ -0,0 +1,509 @@
+From Theories Require Import category.
+From Theories Require Import translation_fib.
+
+Set Primitive Projections.
+Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
+
+
+(* translation of equality, CubicalTT-style *)
+
+Definition path0 {p}
+  (A0 : @El0 p Type0)
+  (A1 : @El1 p Type0 Type1 A0)
+  (x0 : El0 A0)
+  (x1 : El1 A0 A1 x0)
+  (y0 : El0 A0)
+  (y1 : El1 A0 A1 y0)
+: @El0 p Type0.
+Proof.
+refine (fun q α => _).
+unshelve econstructor.
+- refine (fun r β => _).
+  exact (itype r ((A0 r (α ∘ β)).(yft0) r !)
+    (x0 r (α ∘ β)) (y0 r (α ∘ β))).
+- refine (fun r β s => _). simpl in s.
+  refine
+  (forall (αi : r ≤ 1),
+  (A0 r (α ∘ β)).(yft1) r !
+  (fun r0 β0 => cast0 A0 A1 (α ∘ β) β0
+    _
+  )).
+  refine (itype_out (s r0 β0) (αi ∘ β0)).
+- refine (fun r β => _).
+  apply falso.
+Defined.
+
+Definition path1 {p}
+  (A0 : @El0 p Type0)
+  (A1 : @El1 p Type0 Type1 A0)
+  (x0 : El0 A0)
+  (x1 : El1 A0 A1 x0)
+  (y0 : El0 A0)
+  (y1 : El1 A0 A1 y0)
+: @El1 p Type0 Type1 (path0 A0 A1 x0 x1 y0 y1).
+Proof.
+refine (fun q α => _).
+reflexivity.
+Defined.
+
+Definition path_refl0 {p}
+  (A0 : @El0 p Type0)
+  (A1 : @El1 p Type0 Type1 A0)
+  (x0 : El0 A0)
+  (x1 : El1 A0 A1 x0)
+: El0 (path0 A0 A1 x0 x1 x0 x1).
+Proof.
+refine (fun q α => _). simpl.
+exact (itype_in (fun _ => x0 q α)).
+Defined.
+
+Definition path_refl1 {p}
+  (A0 : @El0 p Type0)
+  (A1 : @El1 p Type0 Type1 A0)
+  (x0 : El0 A0)
+  (x1 : El1 A0 A1 x0)
+: El1 _ (path1 A0 A1 x0 x1 x0 x1) (path_refl0 A0 A1 x0 x1).
+Proof.
+refine (fun q α αi => _).
+unfold path_refl0 ; simpl. unfold cast0 ; simpl.
+refine (J_seqs _ (fun p A x y => x y)
+  (fun X _ => yft1 (A0 q α) q !
+    (fun r β => J_seq _ (α ⋅ A0)
+      (fun a _ => yft0 (a r β) r !)
+      (X r (yft0 (A0 r (α ∘ β)) r !) (fun _ => x0 r (α ∘ β)) (αi ∘ β))
+      (fun r (β : r ≤ q) => yft_funct β (A0 q α)) (A1 q α)
+    )
+  )
+  _ (fun p A (x : p ≤ 1 -> A) y => itype_out (itype_in x) y)
+  (ssym itype_inout)).
+refine (x1 q α).
+Defined.
+
+Definition itype_out0_aux {p} {A : Type} {B : A -> SProp}
+  {X : forall (a : A) (b : B a), Type} {y z : forall (a : A) (b : B a), X a b}
+  {x : forall (a : A) (b : B a), itype p (X a b) (y a b) (z a b)} :
+  (fun a b => itype_out (x a b) i0) ≡ y.
+Proof.
+refine (J_seqs _ _ (fun T _ => (fun a b => T p (X a b) (y a b) (z a b) (x a b)) ≡ y) (srefl _) _ (ssym itype_out0)).
+Defined.
+
+Definition itype_out1_aux {p} {A : Type} {B : A -> SProp}
+  {X : forall (a : A) (b : B a), Type} {y z : forall (a : A) (b : B a), X a b}
+  {x : forall (a : A) (b : B a), itype p (X a b) (y a b) (z a b)} :
+  (fun a b => itype_out (x a b) i1) ≡ z.
+Proof.
+refine (J_seqs _ _ (fun T _ => (fun a b => T p (X a b) (y a b) (z a b) (x a b)) ≡ z) (srefl _) _ (ssym itype_out1)).
+Defined.
+
+Definition path_funext0 {p}
+  (A0 : @El0 p Type0)
+  (A1 : @El1 p Type0 Type1 A0)
+  (B0 : @El0 p Type0)
+  (B1 : @El1 p Type0 Type1 B0)
+  (f0 : El0 (Arr0 A0 A1 B0 B1))
+  (f1 : El1 _ (Arr1 A0 A1 B0 B1) f0)
+  (g0 : El0 (Arr0 A0 A1 B0 B1))
+  (g1 : El1 _ (Arr1 A0 A1 B0 B1) g0)
+  (h0 : El0 (Prod0 A0 A1
+    (fun q α x0 x1 => path0 (α ⋅ B0) (α ⋅ B1)
+      (app0 (α ⋅ f0) x0 x1) (app1 (α ⋅ f1) x0 x1)
+      (app0 (α ⋅ g0) x0 x1) (app1 (α ⋅ g1) x0 x1) q !)
+    (fun q α x0 x1 => path1 (α ⋅ B0) (α ⋅ B1)
+      (app0 (α ⋅ f0) x0 x1) (app1 (α ⋅ f1) x0 x1)
+      (app0 (α ⋅ g0) x0 x1) (app1 (α ⋅ g1) x0 x1) q !)
+    ))
+  (h1 : El1 _ (Prod1 A0 A1
+    (fun q α x0 x1 => path0 (α ⋅ B0) (α ⋅ B1)
+      (app0 (α ⋅ f0) x0 x1) (app1 (α ⋅ f1) x0 x1)
+      (app0 (α ⋅ g0) x0 x1) (app1 (α ⋅ g1) x0 x1) q !)
+    (fun q α x0 x1 => path1 (α ⋅ B0) (α ⋅ B1)
+      (app0 (α ⋅ f0) x0 x1) (app1 (α ⋅ f1) x0 x1)
+      (app0 (α ⋅ g0) x0 x1) (app1 (α ⋅ g1) x0 x1) q !)
+    ) h0)
+: El0 (path0 (Arr0 A0 A1 B0 B1) (Arr1 A0 A1 B0 B1) f0 f1 g0 g1).
+Proof.
+refine (fun q α => _).
+change (itype q (forall x0 : El0 (α ⋅ A0), El1 (α ⋅ A0) (α ⋅ A1) x0 -> yft0 (B0 q α) q !) (f0 q α) (g0 q α)).
+assert ((fun x0 x1 => itype_out (h0 q α x0 x1) i0) ≡ f0 q α) as H0.
+{ apply itype_out0_aux. }
+assert ((fun x0 x1 => itype_out (h0 q α x0 x1) i1) ≡ g0 q α) as H1.
+{ apply itype_out1_aux. }
+refine (J_seq _ _ (fun x _ => itype q _ x _) _ _ H0).
+refine (J_seq _ _ (fun x _ => itype q _ _ x) _ _ H1).
+refine (itype_in (fun αi x0 x1 => itype_out (h0 q α x0 x1) αi)).
+Defined.
+
+Lemma app2_seq {A : Type} {B : A -> Type} {C : forall (x : A) (y : B x), Type} {f g : forall (x : A) (y : B x), C x y} (e : f ≡ g) (x : A) (y : B x) : f x y ≡ g x y.
+Proof.
+refine (J_seqs _ _ (fun X _ => f x y ≡ X x y) (srefl _) _ e).
+Defined.
+
+Definition path_funext1 {p}
+  (A0 : @El0 p Type0)
+  (A1 : @El1 p Type0 Type1 A0)
+  (B0 : @El0 p Type0)
+  (B1 : @El1 p Type0 Type1 B0)
+  (f0 : El0 (Arr0 A0 A1 B0 B1))
+  (f1 : El1 _ (Arr1 A0 A1 B0 B1) f0)
+  (g0 : El0 (Arr0 A0 A1 B0 B1))
+  (g1 : El1 _ (Arr1 A0 A1 B0 B1) g0)
+  (h0 : El0 (Prod0 A0 A1
+    (fun q α x0 x1 => path0 (α ⋅ B0) (α ⋅ B1)
+      (app0 (α ⋅ f0) x0 x1) (app1 (α ⋅ f1) x0 x1)
+      (app0 (α ⋅ g0) x0 x1) (app1 (α ⋅ g1) x0 x1) q !)
+    (fun q α x0 x1 => path1 (α ⋅ B0) (α ⋅ B1)
+      (app0 (α ⋅ f0) x0 x1) (app1 (α ⋅ f1) x0 x1)
+      (app0 (α ⋅ g0) x0 x1) (app1 (α ⋅ g1) x0 x1) q !)
+    ))
+  (h1 : El1 _ (Prod1 A0 A1
+    (fun q α x0 x1 => path0 (α ⋅ B0) (α ⋅ B1)
+      (app0 (α ⋅ f0) x0 x1) (app1 (α ⋅ f1) x0 x1)
+      (app0 (α ⋅ g0) x0 x1) (app1 (α ⋅ g1) x0 x1) q !)
+    (fun q α x0 x1 => path1 (α ⋅ B0) (α ⋅ B1)
+      (app0 (α ⋅ f0) x0 x1) (app1 (α ⋅ f1) x0 x1)
+      (app0 (α ⋅ g0) x0 x1) (app1 (α ⋅ g1) x0 x1) q !)
+    ) h0)
+: El1 _ (path1 (Arr0 A0 A1 B0 B1) (Arr1 A0 A1 B0 B1) f0 f1 g0 g1)
+  (path_funext0 A0 A1 B0 B1 f0 f1 g0 g1 h0 h1).
+Proof.
+refine (fun q α αi x0 x1 => _).
+change (yft1 (B0 q α) q ! (fun r β => cast0 B0 B1 α β (itype_out (path_funext0 A0 A1 B0 B1 f0 f1 g0 g1 h0 h1 r (α ∘ β)) (αi ∘ β) (β ⋅ x0) (β ⋅ x1)))).
+unfold path_funext0 ; simpl.
+assert ((fun r β y0 y1 => itype_out (h0 r (α ∘ β) y0 y1) i0) ≡ (fun r β => f0 r (α ∘ β))) as H0.
+{ refine (J_seqs _ _ (fun T _ => (fun r β y0 y1 => T r (yft0 (B0 r (α ∘ β)) r !) (f0 r (α ∘ β) y0 y1) (g0 r (α ∘ β) y0 y1) (h0 r (α ∘ β) y0 y1)) ≡ α ⋅ f0) (srefl _) _ (ssym itype_out0)). }
+assert ((fun r β y0 y1 => itype_out (h0 r (α ∘ β) y0 y1) i1) ≡ (fun r β => g0 r (α ∘ β))) as H1.
+{ refine (J_seqs _ _ (fun T _ => (fun r β y0 y1 => T r (yft0 (B0 r (α ∘ β)) r !) (f0 r (α ∘ β) y0 y1) (g0 r (α ∘ β) y0 y1) (h0 r (α ∘ β) y0 y1)) ≡ α ⋅ g0) (srefl _) _ (ssym itype_out1)). }
+
+match goal with
+|- yft1 (B0 q α) q ! (fun r β => cast0 B0 B1 α β (itype_out (J_seq ?TT ?XX ?PP ?AA ?YY ?EE) (αi ∘ β) (β ⋅ x0) (β ⋅ x1))) =>
+refine (J_seqs _ (fun r β y0 y1 => itype_out (h0 r (α ∘ β) y0 y1) i0) (fun X E =>
+  yft1 (B0 q α) q ! (fun r β => cast0 B0 B1 α β (@itype_out r
+    (forall y0 y1, yft0 (B0 r (α ∘ β)) r !) (X r β) (g0 r (α ∘ β))
+    (J_seq TT (fun y0 y1 => itype_out (h0 r (α ∘ β) y0 y1) i0) PP AA (X r β) (app2_seq E r β))
+    (αi ∘ β) (β ⋅ x0) (β ⋅ x1))))
+  _ (fun r β => f0 r (α ∘ β)) H0)
+end.
+simpl.
+
+match goal with
+|- yft1 (B0 q α) q ! (fun r β => cast0 B0 B1 α β (itype_out (J_seq ?TT ?XX ?PP ?AA ?YY ?EE) (αi ∘ β) (β ⋅ x0) (β ⋅ x1))) =>
+refine (J_seqs _ (fun r β y0 y1 => itype_out (h0 r (α ∘ β) y0 y1) i1) (fun X E =>
+  yft1 (B0 q α) q ! (fun r β => cast0 B0 B1 α β (@itype_out r
+    (forall y0 y1, yft0 (B0 r (α ∘ β)) r !) (fun y0 y1 => itype_out (h0 r (α ∘ β) y0 y1) i0) (X r β)
+    (J_seq TT (fun y0 y1 => itype_out (h0 r (α ∘ β) y0 y1) i1) PP AA (X r β) (app2_seq E r β))
+    (αi ∘ β) (β ⋅ x0) (β ⋅ x1))))
+  _ (fun r β => g0 r (α ∘ β)) H1)
+end.
+simpl.
+
+refine (J_seqs _ (fun (p : ℙ) (A : Type) (x : (p ≤ 1) -> A) (y : p ≤ 1) => x y)
+               (fun X _ => yft1 (B0 q α) q ! (fun r β => cast0 B0 B1 α β (X r (forall y0 y1, yft0 (B0 r (α ∘ β)) r !) (fun αi0 x2 x3 => itype_out (h0 r (α ∘ β) x2 x3) αi0) (αi ∘ β) (β ⋅ x0) (β ⋅ x1))))
+               _ (fun p A (x : p ≤ 1 -> A) y => itype_out (itype_in x) y) (ssym itype_inout)).
+refine (h1 q α x0 x1 αi).
+Defined.
+
+(* comparing eq and path *)
+(* we get functions both ways, but they do not form an equivalence without funext/η, since
+   α ≠ merge (squish ∘ α) (antisquish ∘ α) *)
+
+Lemma itype_out0_aux2 {A : Type} {B : A -> Type}
+  {p : forall (a : A) (b : B a), nat}
+  {X : forall (a : A) (b : B a), Type} {y z : forall (a : A) (b : B a), X a b}
+  {x : forall (a : A) (b : B a), itype (p a b) (X a b) (y a b) (z a b)} :
+  (fun a b => itype_out (x a b) i0) ≡ y.
+Proof.
+refine (J_seqs _ _ (fun T _ => (fun a b => T (p a b) (X a b) (y a b) (z a b) (x a b)) ≡ y) (srefl _) _ (ssym itype_out0)).
+Defined.
+
+Lemma itype_out1_aux2 {A : Type} {B : A -> Type}
+  {p : forall (a : A) (b : B a), nat}
+  {X : forall (a : A) (b : B a), Type} {y z : forall (a : A) (b : B a), X a b}
+  {x : forall (a : A) (b : B a), itype (p a b) (X a b) (y a b) (z a b)} :
+  (fun a b => itype_out (x a b) i1) ≡ z.
+Proof.
+refine (J_seqs _ _ (fun T _ => (fun a b => T (p a b) (X a b) (y a b) (z a b) (x a b)) ≡ z) (srefl _) _ (ssym itype_out1)).
+Defined.
+
+Definition compare0 {p}
+  (A0 : @El0 p Type0)
+  (A1 : @El1 p Type0 Type1 A0)
+  (x0 : El0 A0)
+  (x1 : El1 A0 A1 x0)
+  (y0 : El0 A0)
+  (y1 : El1 A0 A1 y0)
+  (e0 : El0 (path0 A0 A1 x0 x1 y0 y1))
+  (e1 : El1 _ (path1 A0 A1 x0 x1 y0 y1) e0)
+  : El0 (eq0 A0 A1 x0 x1 y0 y1).
+Proof.
+refine (fun q α => _).
+unshelve econstructor.
+- refine (fun r β => _).
+  refine (itype_out (e0 r (α ∘ squish ∘ β)) (antisquish ∘ β)).
+- refine (fun r β => _).
+  refine (e1 r (α ∘ squish ∘ β) (antisquish ∘ β)).
+- change ((fun r β => itype_out (e0 r (α ∘ β)) i0) ≡ α ⋅ x0).
+  eapply itype_out0_aux2.
+- change ((fun r β => itype_out (e0 r (α ∘ β)) i1) ≡ α ⋅ y0).
+  eapply itype_out1_aux2.
+Defined.
+
+Definition compare1 {p}
+  (A0 : @El0 p Type0)
+  (A1 : @El1 p Type0 Type1 A0)
+  (x0 : El0 A0)
+  (x1 : El1 A0 A1 x0)
+  (y0 : El0 A0)
+  (y1 : El1 A0 A1 y0)
+  (e0 : El0 (path0 A0 A1 x0 x1 y0 y1))
+  (e1 : El1 _ (path1 A0 A1 x0 x1 y0 y1) e0)
+  : El1 _ (eq1 A0 A1 x0 x1 y0 y1) (compare0 A0 A1 x0 x1 y0 y1 e0 e1).
+Proof.
+refine (fun q α => _). simpl. unfold cube_eqR.
+reflexivity.
+Defined.
+
+Definition anticompare0 {p}
+  (A0 : @El0 p Type0)
+  (A1 : @El1 p Type0 Type1 A0)
+  (x0 : El0 A0)
+  (x1 : El1 A0 A1 x0)
+  (y0 : El0 A0)
+  (y1 : El1 A0 A1 y0)
+  (e0 : El0 (eq0 A0 A1 x0 x1 y0 y1))
+  (e1 : El1 _ (eq1 A0 A1 x0 x1 y0 y1) e0)
+  : El0 (path0 A0 A1 x0 x1 y0 y1).
+Proof.
+refine (fun q α => _). simpl.
+refine (J_seq _ _ (fun x _ => itype q _ (x q !) _) _ _ ((e0 q α).(ce_s))).
+refine (J_seq _ _ (fun x _ => itype q _ _ (x q !)) _ _ ((e0 q α).(ce_t))).
+refine (@itype_in q (yft0 (A0 q α) q !) (fun αi => (e0 q α).(ce_f0) q (merge ! αi))).
+Defined.
+
+Definition anticompare1 {p}
+  (A0 : @El0 p Type0)
+  (A1 : @El1 p Type0 Type1 A0)
+  (x0 : El0 A0)
+  (x1 : El1 A0 A1 x0)
+  (y0 : El0 A0)
+  (y1 : El1 A0 A1 y0)
+  (e0 : El0 (eq0 A0 A1 x0 x1 y0 y1))
+  (e1 : El1 _ (eq1 A0 A1 x0 x1 y0 y1) e0)
+  : El1 _ (path1 A0 A1 x0 x1 y0 y1) (anticompare0 A0 A1 x0 x1 y0 y1 e0 e1).
+Proof.
+refine (fun q α αi => _).
+change (yft1 (A0 q α) q ! (fun r β => cast0 A0 A1 α β (itype_out (anticompare0 A0 A1 x0 x1 y0 y1 e0 e1 r (α ∘ β)) (αi ∘ β)))).
+unfold anticompare0.
+pose proof (e1 q α). simpl in H. unfold cube_eqR in H. unfold cast0 in H. simpl in H.
+refine (J_seqs _ _ (fun X _ =>
+  yft1 (A0 q α) q ! (fun r β => cast0 A0 A1 α β (itype_out
+    (J_seq _ _
+      (fun x (_ : side_0 ⋅ ce_f0 (X r β) ≡ x) =>
+        itype r (yft0 (A0 r (α ∘ β)) r !)
+          (x r !) (y0 r ((α ∘ β) ∘ !)))
+      (J_seq _ _
+        (fun x (_ : side_1 ⋅ ce_f0 (X r β) ≡ x) =>
+          itype r (yft0 (A0 r (α ∘ β)) r !)
+            (ce_f0 (X r β) r side_0) (x r !))
+        (@itype_in r (yft0 (A0 r (α ∘ β)) r !) (fun αi0 : r ≤ 1 => ce_f0 (X r β) r (merge ! αi0)))
+        (α ∘ β ⋅ y0) (ce_t (X r β)))
+      (α ∘ β ⋅ x0) (ce_s (X r β)))
+    (αi ∘ β)))) _ _ (ssym H)). simpl.
+pose proof (ce_t (e0 q α)).
+refine (J_seqs _ _ (fun X E =>
+  yft1 (A0 q α) q !
+    (fun (r : nat) (β : r ≤ q) =>
+     cast0 A0 A1 α β
+       (itype_out
+          (J_seq _ _
+             (fun (x : forall (x2 : nat) (x3 : x2 ≤ r), yft0 (A0 x2 ((α ∘ β) ∘ (squish ∘ (side_0 ∘ x3)))) x2 !)
+                (_ : (fun (r0 : nat) (β0 : r0 ≤ r) => ce_f0 (e0 q (α ∘ !)) r0 (promote β ∘ (side_0 ∘ β0))) ≡ x)
+              => itype r (yft0 (A0 r (α ∘ β)) r !) (x r !) (X r β))
+             (J_seq _ _
+                (fun
+                   (x : forall (x2 : nat) (x3 : x2 ≤ r), yft0 (A0 x2 ((α ∘ β) ∘ (squish ∘ (side_1 ∘ x3)))) x2 !)
+                   (_ : (fun (r0 : nat) (β0 : r0 ≤ r) => ce_f0 (e0 q (α ∘ !)) r0 (promote β ∘ (side_1 ∘ β0))) ≡ x)
+                 => itype r (yft0 (A0 r (α ∘ β)) r !) (ce_f0 (e0 q (α ∘ !)) r (promote β ∘ side_0)) (x r !))
+                (@itype_in r (yft0 (A0 r (α ∘ β)) r !)
+                   (fun αi0 : r ≤ 1 => ce_f0 (e0 q (α ∘ !)) r (promote β ∘ merge ! αi0)))
+                (β ⋅ X)
+                (J_seqs _ _
+                   (fun (u : forall (x2 : nat) (x3 : x2 ≤ q), yft0 (A0 x2 ((α ∘ !) ∘ (! ∘ x3))) x2 !)
+                      (_ : side_1 ⋅ ce_f0 (e0 q (α ∘ !)) ≡ u) =>
+                    (fun (r0 : nat) (β0 : r0 ≤ r) => ce_f0 (e0 q (α ∘ !)) r0 (side_1 ∘ (β ∘ β0))) ≡ β ⋅ u)
+                   (srefl (fun (r0 : nat) (β0 : r0 ≤ r) => ce_f0 (e0 q (α ∘ !)) r0 (side_1 ∘ (β ∘ β0))))
+                   X E))
+             (α ∘ β ⋅ x0)
+             (J_seqs _ _
+                (fun (u : forall (x2 : nat) (x3 : x2 ≤ q), yft0 (A0 x2 ((α ∘ !) ∘ (! ∘ x3))) x2 !)
+                   (_ : side_0 ⋅ ce_f0 (e0 q (α ∘ !)) ≡ u) =>
+                 (fun (r0 : nat) (β0 : r0 ≤ r) => ce_f0 (e0 q (α ∘ !)) r0 (side_0 ∘ (β ∘ β0))) ≡ β ⋅ u)
+                (srefl (fun (r0 : nat) (β0 : r0 ≤ r) => ce_f0 (e0 q (α ∘ !)) r0 (side_0 ∘ (β ∘ β0))))
+                (fun (r0 : nat) (β0 : r0 ≤ q) => x0 r0 ((α ∘ !) ∘ (! ∘ β0))) (ce_s (e0 q (α ∘ !)))))
+          (αi ∘ β)))) _ _ (ce_t (e0 q α))). simpl.
+refine (J_seqs _ _ (fun X E =>
+  yft1 (A0 q α) q !
+    (fun (r : nat) (β : r ≤ q) =>
+     cast0 A0 A1 α β
+       (itype_out
+          (J_seq (forall (x2 : nat) (x3 : x2 ≤ r), yft0 (A0 x2 ((α ∘ β) ∘ (squish ∘ (side_0 ∘ x3)))) x2 !)
+             (fun (r0 : nat) (β0 : r0 ≤ r) => ce_f0 (e0 q (α ∘ !)) r0 (promote β ∘ (side_0 ∘ β0)))
+             (fun (x : forall (x2 : nat) (x3 : x2 ≤ r), yft0 (A0 x2 ((α ∘ β) ∘ (squish ∘ (side_0 ∘ x3)))) x2 !)
+                (_ : (fun (r0 : nat) (β0 : r0 ≤ r) => ce_f0 (e0 q (α ∘ !)) r0 (promote β ∘ (side_0 ∘ β0))) ≡ x)
+              => itype r (yft0 (A0 r (α ∘ β)) r !) (x r !) (ce_f0 (e0 q (α ∘ !)) r (side_1 ∘ β)))
+             (@itype_in r (yft0 (A0 r (α ∘ β)) r !)
+                (fun αi0 : r ≤ 1 => ce_f0 (e0 q (α ∘ !)) r (promote β ∘ merge ! αi0)))
+             (β ⋅ X)
+             (J_seqs (forall (x2 : nat) (x3 : x2 ≤ q), yft0 (A0 x2 ((α ∘ !) ∘ (! ∘ x3))) x2 !)
+                (side_0 ⋅ ce_f0 (e0 q (α ∘ !)))
+                (fun (u : forall (x2 : nat) (x3 : x2 ≤ q), yft0 (A0 x2 ((α ∘ !) ∘ (! ∘ x3))) x2 !)
+                   (_ : side_0 ⋅ ce_f0 (e0 q (α ∘ !)) ≡ u) =>
+                 (fun (r0 : nat) (β0 : r0 ≤ r) => ce_f0 (e0 q (α ∘ !)) r0 (side_0 ∘ (β ∘ β0))) ≡ β ⋅ u)
+                (srefl (fun (r0 : nat) (β0 : r0 ≤ r) => ce_f0 (e0 q (α ∘ !)) r0 (side_0 ∘ (β ∘ β0))))
+                X E))
+          (αi ∘ β)))) _ _ (ce_s (e0 q α))). simpl.
+refine (J_seqs _ _
+  (fun x _ => yft1 (A0 q α) q ! (fun r β => cast0 A0 A1 α β (x r (yft0 (A0 r (α ∘ β)) r !) (fun αi0 : r ≤ 1 => ce_f0 (e0 q α) r (promote β ∘ merge ! αi0)) (αi ∘ β)))) _ _
+               (ssym itype_inout)).
+refine ((e0 q α).(ce_f1) q (merge ! αi)).
+Defined.
+
+Definition funext0 {p}
+(A0 : @El0 p Type0)
+(A1 : @El1 p Type0 Type1 A0)
+(B0 : @El0 p Type0)
+(B1 : @El1 p Type0 Type1 B0)
+(f0 : El0 (Arr0 A0 A1 B0 B1))
+(f1 : El1 _ (Arr1 A0 A1 B0 B1) f0)
+(g0 : El0 (Arr0 A0 A1 B0 B1))
+(g1 : El1 _ (Arr1 A0 A1 B0 B1) g0)
+(h0 : El0 (Prod0 A0 A1
+  (fun q α x0 x1 => eq0 (α ⋅ B0) (α ⋅ B1)
+    (app0 (α ⋅ f0) x0 x1) (app1 (α ⋅ f1) x0 x1)
+    (app0 (α ⋅ g0) x0 x1) (app1 (α ⋅ g1) x0 x1) q !)
+  (fun q α x0 x1 => eq1 (α ⋅ B0) (α ⋅ B1)
+    (app0 (α ⋅ f0) x0 x1) (app1 (α ⋅ f1) x0 x1)
+    (app0 (α ⋅ g0) x0 x1) (app1 (α ⋅ g1) x0 x1) q !)
+  ))
+(h1 : El1 _ (Prod1 A0 A1
+  (fun q α x0 x1 => eq0 (α ⋅ B0) (α ⋅ B1)
+    (app0 (α ⋅ f0) x0 x1) (app1 (α ⋅ f1) x0 x1)
+    (app0 (α ⋅ g0) x0 x1) (app1 (α ⋅ g1) x0 x1) q !)
+  (fun q α x0 x1 => eq1 (α ⋅ B0) (α ⋅ B1)
+    (app0 (α ⋅ f0) x0 x1) (app1 (α ⋅ f1) x0 x1)
+    (app0 (α ⋅ g0) x0 x1) (app1 (α ⋅ g1) x0 x1) q !)
+  ) h0)
+: El0 (eq0 (Arr0 A0 A1 B0 B1) (Arr1 A0 A1 B0 B1) f0 f1 g0 g1).
+Proof.
+unshelve refine (compare0 (Arr0 A0 A1 B0 B1) (Arr1 A0 A1 B0 B1) f0 f1 g0 g1 _ _).
+unshelve refine (path_funext0 A0 A1 B0 B1 f0 f1 g0 g1 _ _).
+refine (fun q α x0 x1 => _).
+refine (anticompare0 (α ⋅ B0) (α ⋅ B1)
+  (app0 (α ⋅ f0) x0 x1) (app1 (α ⋅ f1) x0 x1)
+  (app0 (α ⋅ g0) x0 x1) (app1 (α ⋅ g1) x0 x1)
+  (@dapp0 q (α ⋅ A0) (α ⋅ A1)
+    (fun r β y0 y1 => eq0 (α ∘ β ⋅ B0) (α ∘ β ⋅ B1)
+      (app0 (α ∘ β ⋅ f0) y0 y1) (app1 (α ∘ β ⋅ f1) y0 y1)
+      (app0 (α ∘ β ⋅ g0) y0 y1) (app1 (α ∘ β ⋅ g1) y0 y1) r !)
+    (fun r β y0 y1 => eq1 (α ∘ β ⋅ B0) (α ∘ β ⋅ B1)
+      (app0 (α ∘ β ⋅ f0) y0 y1) (app1 (α ∘ β ⋅ f1) y0 y1)
+      (app0 (α ∘ β ⋅ g0) y0 y1) (app1 (α ∘ β ⋅ g1) y0 y1) r !)
+    (α ⋅ h0) x0 x1)
+  (@dapp1 q (α ⋅ A0) (α ⋅ A1)
+    (fun r β y0 y1 => eq0 (α ∘ β ⋅ B0) (α ∘ β ⋅ B1)
+      (app0 (α ∘ β ⋅ f0) y0 y1) (app1 (α ∘ β ⋅ f1) y0 y1)
+      (app0 (α ∘ β ⋅ g0) y0 y1) (app1 (α ∘ β ⋅ g1) y0 y1) r !)
+    (fun r β y0 y1 => eq1 (α ∘ β ⋅ B0) (α ∘ β ⋅ B1)
+      (app0 (α ∘ β ⋅ f0) y0 y1) (app1 (α ∘ β ⋅ f1) y0 y1)
+      (app0 (α ∘ β ⋅ g0) y0 y1) (app1 (α ∘ β ⋅ g1) y0 y1) r !)
+    (α ⋅ h0) (α ⋅ h1) x0 x1) q !).
+refine (fun q α x0 x1 => _).
+refine (anticompare1 (α ⋅ B0) (α ⋅ B1)
+  (app0 (α ⋅ f0) x0 x1) (app1 (α ⋅ f1) x0 x1)
+  (app0 (α ⋅ g0) x0 x1) (app1 (α ⋅ g1) x0 x1)
+  (@dapp0 q (α ⋅ A0) (α ⋅ A1)
+    (fun r β y0 y1 => eq0 (α ∘ β ⋅ B0) (α ∘ β ⋅ B1)
+      (app0 (α ∘ β ⋅ f0) y0 y1) (app1 (α ∘ β ⋅ f1) y0 y1)
+      (app0 (α ∘ β ⋅ g0) y0 y1) (app1 (α ∘ β ⋅ g1) y0 y1) r !)
+    (fun r β y0 y1 => eq1 (α ∘ β ⋅ B0) (α ∘ β ⋅ B1)
+      (app0 (α ∘ β ⋅ f0) y0 y1) (app1 (α ∘ β ⋅ f1) y0 y1)
+      (app0 (α ∘ β ⋅ g0) y0 y1) (app1 (α ∘ β ⋅ g1) y0 y1) r !)
+    (α ⋅ h0) x0 x1)
+  (@dapp1 q (α ⋅ A0) (α ⋅ A1)
+  (fun r β y0 y1 => eq0 (α ∘ β ⋅ B0) (α ∘ β ⋅ B1)
+    (app0 (α ∘ β ⋅ f0) y0 y1) (app1 (α ∘ β ⋅ f1) y0 y1)
+    (app0 (α ∘ β ⋅ g0) y0 y1) (app1 (α ∘ β ⋅ g1) y0 y1) r !)
+  (fun r β y0 y1 => eq1 (α ∘ β ⋅ B0) (α ∘ β ⋅ B1)
+    (app0 (α ∘ β ⋅ f0) y0 y1) (app1 (α ∘ β ⋅ f1) y0 y1)
+    (app0 (α ∘ β ⋅ g0) y0 y1) (app1 (α ∘ β ⋅ g1) y0 y1) r !)
+  (α ⋅ h0) (α ⋅ h1) x0 x1) q !).
+unshelve refine (path_funext1 A0 A1 B0 B1 f0 f1 g0 g1
+  (fun q α x0 x1 => anticompare0 (α ⋅ B0) (α ⋅ B1)
+  (app0 (α ⋅ f0) x0 x1) (app1 (α ⋅ f1) x0 x1)
+  (app0 (α ⋅ g0) x0 x1) (app1 (α ⋅ g1) x0 x1)
+  (@dapp0 q (α ⋅ A0) (α ⋅ A1)
+    (fun r β y0 y1 => eq0 (α ∘ β ⋅ B0) (α ∘ β ⋅ B1)
+      (app0 (α ∘ β ⋅ f0) y0 y1) (app1 (α ∘ β ⋅ f1) y0 y1)
+      (app0 (α ∘ β ⋅ g0) y0 y1) (app1 (α ∘ β ⋅ g1) y0 y1) r !)
+    (fun r β y0 y1 => eq1 (α ∘ β ⋅ B0) (α ∘ β ⋅ B1)
+      (app0 (α ∘ β ⋅ f0) y0 y1) (app1 (α ∘ β ⋅ f1) y0 y1)
+      (app0 (α ∘ β ⋅ g0) y0 y1) (app1 (α ∘ β ⋅ g1) y0 y1) r !)
+    (α ⋅ h0) x0 x1)
+  (@dapp1 q (α ⋅ A0) (α ⋅ A1)
+    (fun r β y0 y1 => eq0 (α ∘ β ⋅ B0) (α ∘ β ⋅ B1)
+      (app0 (α ∘ β ⋅ f0) y0 y1) (app1 (α ∘ β ⋅ f1) y0 y1)
+      (app0 (α ∘ β ⋅ g0) y0 y1) (app1 (α ∘ β ⋅ g1) y0 y1) r !)
+    (fun r β y0 y1 => eq1 (α ∘ β ⋅ B0) (α ∘ β ⋅ B1)
+      (app0 (α ∘ β ⋅ f0) y0 y1) (app1 (α ∘ β ⋅ f1) y0 y1)
+      (app0 (α ∘ β ⋅ g0) y0 y1) (app1 (α ∘ β ⋅ g1) y0 y1) r !)
+    (α ⋅ h0) (α ⋅ h1) x0 x1) q !)
+   (fun q α x0 x1 => anticompare1 (α ⋅ B0) (α ⋅ B1)
+  (app0 (α ⋅ f0) x0 x1) (app1 (α ⋅ f1) x0 x1)
+  (app0 (α ⋅ g0) x0 x1) (app1 (α ⋅ g1) x0 x1)
+  (@dapp0 q (α ⋅ A0) (α ⋅ A1)
+    (fun r β y0 y1 => eq0 (α ∘ β ⋅ B0) (α ∘ β ⋅ B1)
+      (app0 (α ∘ β ⋅ f0) y0 y1) (app1 (α ∘ β ⋅ f1) y0 y1)
+      (app0 (α ∘ β ⋅ g0) y0 y1) (app1 (α ∘ β ⋅ g1) y0 y1) r !)
+    (fun r β y0 y1 => eq1 (α ∘ β ⋅ B0) (α ∘ β ⋅ B1)
+      (app0 (α ∘ β ⋅ f0) y0 y1) (app1 (α ∘ β ⋅ f1) y0 y1)
+      (app0 (α ∘ β ⋅ g0) y0 y1) (app1 (α ∘ β ⋅ g1) y0 y1) r !)
+    (α ⋅ h0) x0 x1)
+  (@dapp1 q (α ⋅ A0) (α ⋅ A1)
+  (fun r β y0 y1 => eq0 (α ∘ β ⋅ B0) (α ∘ β ⋅ B1)
+    (app0 (α ∘ β ⋅ f0) y0 y1) (app1 (α ∘ β ⋅ f1) y0 y1)
+    (app0 (α ∘ β ⋅ g0) y0 y1) (app1 (α ∘ β ⋅ g1) y0 y1) r !)
+  (fun r β y0 y1 => eq1 (α ∘ β ⋅ B0) (α ∘ β ⋅ B1)
+    (app0 (α ∘ β ⋅ f0) y0 y1) (app1 (α ∘ β ⋅ f1) y0 y1)
+    (app0 (α ∘ β ⋅ g0) y0 y1) (app1 (α ∘ β ⋅ g1) y0 y1) r !)
+  (α ⋅ h0) (α ⋅ h1) x0 x1) q !)).
+Defined.
+
+Definition funext1 {p}
+(A0 : @El0 p Type0)
+(A1 : @El1 p Type0 Type1 A0)
+(B0 : @El0 p Type0)
+(B1 : @El1 p Type0 Type1 B0)
+(f0 : El0 (Arr0 A0 A1 B0 B1))
+(f1 : El1 _ (Arr1 A0 A1 B0 B1) f0)
+(g0 : El0 (Arr0 A0 A1 B0 B1))
+(g1 : El1 _ (Arr1 A0 A1 B0 B1) g0)
+(h0 : El0 (Prod0 A0 A1
+  (fun q α x0 x1 => eq0 (α ⋅ B0) (α ⋅ B1)
+    (app0 (α ⋅ f0) x0 x1) (app1 (α ⋅ f1) x0 x1)
+    (app0 (α ⋅ g0) x0 x1) (app1 (α ⋅ g1) x0 x1) q !)
+  (fun q α x0 x1 => eq1 (α ⋅ B0) (α ⋅ B1)
+    (app0 (α ⋅ f0) x0 x1) (app1 (α ⋅ f1) x0 x1)
+    (app0 (α ⋅ g0) x0 x1) (app1 (α ⋅ g1) x0 x1) q !)
+  ))
+(h1 : El1 _ (Prod1 A0 A1
+  (fun q α x0 x1 => eq0 (α ⋅ B0) (α ⋅ B1)
+    (app0 (α ⋅ f0) x0 x1) (app1 (α ⋅ f1) x0 x1)
+    (app0 (α ⋅ g0) x0 x1) (app1 (α ⋅ g1) x0 x1) q !)
+  (fun q α x0 x1 => eq1 (α ⋅ B0) (α ⋅ B1)
+    (app0 (α ⋅ f0) x0 x1) (app1 (α ⋅ f1) x0 x1)
+    (app0 (α ⋅ g0) x0 x1) (app1 (α ⋅ g1) x0 x1) q !)
+  ) h0)
+: El1 _ (eq1 (Arr0 A0 A1 B0 B1) (Arr1 A0 A1 B0 B1) f0 f1 g0 g1) (funext0 A0 A1 B0 B1 f0 f1 g0 g1 h0 h1).
+Proof.
+(* TODO : just plug things together *)
+Admitted.
\ No newline at end of file
diff --git a/theories/singletons.v b/theories/singletons.v
new file mode 100644
index 0000000..a858e64
--- /dev/null
+++ b/theories/singletons.v
@@ -0,0 +1,225 @@
+From Theories Require Import category.
+From Theories Require Import translation_fib.
+
+Set Primitive Projections.
+Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
+
+(* contractibility of singletons *)
+
+Record wedge_eq {p} 
+  (A0 : @El0 p Type0)
+  (A1 : @El1 p Type0 Type1 A0)
+  (a0 : El0 A0)
+  (a1 : El1 A0 A1 a0)
+  (b0 : El0 A0)
+  (b1 : El1 A0 A1 b0)
+  (e0 : El0 (eq0 A0 A1 a0 a1 b0 b1))
+  (e1 : El1 _ (eq1 A0 A1 a0 a1 b0 b1) e0) : Type :=
+mkWE {
+  we_f0 : @El0 (S (S p)) (squish ∘ squish ⋅ A0) ;
+  we_f1 : @El1 (S (S p)) (squish ∘ squish ⋅ A0) (squish ∘ squish ⋅ A1) we_f0 ;
+  we_0y : side_0 ⋅ we_f0 ≡ squish ⋅ a0 ;
+  we_1y : side_1 ⋅ we_f0 ≡ ce_f0 (e0 p !) ;
+  we_x0 : promote side_0 ⋅ we_f0 ≡ squish ⋅ a0 ;
+  we_x1 : promote side_1 ⋅ we_f0 ≡ ce_f0 (e0 p !) ;
+}.
+
+Arguments we_f0 {_ _ _ _ _ _ _ _ _}.
+Arguments we_f1 {_ _ _ _ _ _ _ _ _}.
+Arguments we_0y {_ _ _ _ _ _ _ _ _}.
+Arguments we_1y {_ _ _ _ _ _ _ _ _}.
+Arguments we_x0 {_ _ _ _ _ _ _ _ _}.
+Arguments we_x1 {_ _ _ _ _ _ _ _ _}.
+
+Definition we_funct {p} 
+  (A0 : @El0 p Type0)
+  (A1 : @El1 p Type0 Type1 A0)
+  (a0 : El0 A0)
+  (a1 : El1 A0 A1 a0)
+  (b0 : El0 A0)
+  (b1 : El1 A0 A1 b0)
+  (e0 : El0 (eq0 A0 A1 a0 a1 b0 b1))
+  (e1 : El1 _ (eq1 A0 A1 a0 a1 b0 b1) e0) {q} (α : q ≤ p) :
+  wedge_eq A0 A1 a0 a1 b0 b1 e0 e1 -> wedge_eq (α ⋅ A0) (α ⋅ A1) (α ⋅ a0) (α ⋅ a1) (α ⋅ b0) (α ⋅ b1) (α ⋅ e0) (α ⋅ e1).
+Proof.
+unshelve refine (fun x => _).
+unshelve econstructor.
+- exact (promote (promote α) ⋅ x.(we_f0)).
+- exact (promote (promote α) ⋅ x.(we_f1)).
+- refine (J_seqs _ _ (fun X _ => promote α ⋅ X ≡ _) (srefl _) _ (ssym (we_0y x))).
+- refine (J_seqs _ _ (fun X _ => promote α ⋅ X ≡ _) _ _ (ssym (we_1y x))).
+  refine (J_seqs _ (fun q α => ce_funct α (e0 p !)) (fun X _ => _ ≡ ce_f0 (X q α)) (srefl _) _ (ssym (e1 p !))).
+- refine (J_seqs _ _ (fun X _ => promote α ⋅ X ≡ _) (srefl _) _ (ssym (we_x0 x))).
+- refine (J_seqs _ _ (fun X _ => promote α ⋅ X ≡ _) _ _ (ssym (we_x1 x))).
+  refine (J_seqs _ (fun q α => ce_funct α (e0 p !)) (fun X _ => _ ≡ ce_f0 (X q α)) (srefl _) _ (ssym (e1 p !))).
+Defined.
+
+Definition wedge_eqR {p}
+  (A0 : @El0 p Type0)
+  (A1 : @El1 p Type0 Type1 A0)
+  (a0 : El0 A0)
+  (a1 : El1 A0 A1 a0)
+  (b0 : El0 A0)
+  (b1 : El1 A0 A1 b0)
+  (e0 : El0 (eq0 A0 A1 a0 a1 b0 b1))
+  (e1 : El1 _ (eq1 A0 A1 a0 a1 b0 b1) e0) :
+ (forall q (α : q ≤ p), wedge_eq (α ⋅ A0) (α ⋅ A1) (α ⋅ a0) (α ⋅ a1) (α ⋅ b0) (α ⋅ b1) (α ⋅ e0) (α ⋅ e1)) -> SProp :=
+fun s => s ≡ fun q α => we_funct A0 A1 a0 a1 b0 b1 e0 e1 α (s p !).
+
+Definition contractor0 {p}
+  (A0 : @El0 p Type0)
+  (A1 : @El1 p Type0 Type1 A0)
+  (a0 : El0 A0)
+  (a1 : El1 A0 A1 a0)
+  (b0 : El0 A0)
+  (b1 : El1 A0 A1 b0)
+  (e0 : El0 (eq0 A0 A1 a0 a1 b0 b1))
+  (e1 : El1 _ (eq1 A0 A1 a0 a1 b0 b1) e0)
+  : @El0 p Type0.
+Proof.
+refine (fun q α => _). unshelve econstructor.
+- unshelve refine (fun r β => _).
+  exact (wedge_eq ((α ∘ β) · A0) ((α ∘ β) · A1) ((α ∘ β) · a0) ((α ∘ β) · a1) ((α ∘ β) · b0) ((α ∘ β) · b1) ((α ∘ β) · e0) ((α ∘ β) · e1)).
+- unshelve refine (fun r β s => _). simpl in s.
+  exact (wedge_eqR ((α ∘ β) · A0) ((α ∘ β) · A1) ((α ∘ β) · a0) ((α ∘ β) · a1) ((α ∘ β) · b0) ((α ∘ β) · b1) ((α ∘ β) · e0) ((α ∘ β) · e1) s).
+- unshelve refine (fun r β b e l le l' => _).
+  apply falso.
+Defined.
+
+Definition contractor1 {p}
+  (A0 : @El0 p Type0)
+  (A1 : @El1 p Type0 Type1 A0)
+  (a0 : El0 A0)
+  (a1 : El1 A0 A1 a0)
+  (b0 : El0 A0)
+  (b1 : El1 A0 A1 b0)
+  (e0 : El0 (eq0 A0 A1 a0 a1 b0 b1))
+  (e1 : El1 _ (eq1 A0 A1 a0 a1 b0 b1) e0)
+  : @El1 p Type0 Type1 (contractor0 A0 A1 a0 a1 b0 b1 e0 e1).
+Proof.
+refine (fun q α => _).
+reflexivity.
+Defined.
+
+Definition contr_filler0 {p}
+  (A0 : @El0 p Type0)
+  (A1 : @El1 p Type0 Type1 A0)
+  (a0 : El0 A0)
+  (a1 : El1 A0 A1 a0)
+  (b0 : El0 A0)
+  (b1 : El1 A0 A1 b0)
+  (e0 : El0 (eq0 A0 A1 a0 a1 b0 b1))
+  (e1 : El1 _ (eq1 A0 A1 a0 a1 b0 b1) e0)
+  : El0 (contractor0 A0 A1 a0 a1 b0 b1 e0 e1).
+Proof.
+refine (fun q α => _). simpl. unshelve econstructor.
+- refine (wedge ⋅ ce_f0 (e0 q α)).
+- refine (wedge ⋅ ce_f1 (e0 q α)).
+- apply sfalso.
+- apply sfalso.
+- apply sfalso.
+- apply sfalso.
+(* as is, this requires some computation rules for wedge *)
+Defined.
+
+Definition contr_filler1 {p}
+  (A0 : @El0 p Type0)
+  (A1 : @El1 p Type0 Type1 A0)
+  (a0 : El0 A0)
+  (a1 : El1 A0 A1 a0)
+  (b0 : El0 A0)
+  (b1 : El1 A0 A1 b0)
+  (e0 : El0 (eq0 A0 A1 a0 a1 b0 b1))
+  (e1 : El1 _ (eq1 A0 A1 a0 a1 b0 b1) e0)
+  : El1 _ (contractor1 A0 A1 a0 a1 b0 b1 e0 e1) (contr_filler0 A0 A1 a0 a1 b0 b1 e0 e1).
+Proof.
+refine (fun q α => _).
+assert (forall (f g : forall (r : ℙ) (β : r ≤ q), wedge_eq ((α ∘ β) · A0) ((α ∘ β) · A1) ((α ∘ β) · a0) ((α ∘ β) · a1) ((α ∘ β) · b0) ((α ∘ β) · b1) ((α ∘ β) · e0) ((α ∘ β) · e1)), 
+  ((fun r β => we_f0 (f r β)) ≡ (fun r β => we_f0 (g r β))) -> f ≡ g)
+  as lemma.
+{ intros f g Hfg.
+  refine (J_seqs _ (fun r β => we_f0 (g r β)) 
+    (fun X E => (fun r β => 
+      {| we_f0 := X r β ; 
+         we_f1 := J_seqs _ _ (fun Y _ => El1 (squish ∘ squish ⋅ (α ∘ β ⋅ A0)) (squish ∘ squish ⋅ (α ∘ β ⋅ A1)) (Y r β)) (we_f1 (g r β)) _ E ;
+         we_0y := J_seqs _ (fun r β => we_f0 (g r β)) (fun Y _ => side_0 ⋅ (Y r β) ≡ squish ⋅ (α ∘ β ⋅ a0)) (we_0y (g r β)) X E ; 
+         we_1y := J_seqs _ _ (fun Y _ => side_1 ⋅ (Y r β) ≡ ce_f0 (e0 r (α ∘ β))) (we_1y (g r β)) X E ;
+         we_x0 := J_seqs _ _ (fun Y _ => (promote side_0) ⋅ (Y r β) ≡ squish ⋅ (α ∘ β ⋅ a0)) (we_x0 (g r β)) X E ;
+         we_x1 := J_seqs _ _ (fun Y _ => (promote side_1) ⋅ (Y r β) ≡ ce_f0 (e0 r (α ∘ β))) (we_x1 (g r β)) X E ; |}) 
+      ≡ g)
+    (srefl _)
+    (fun r β => we_f0 (f r β))
+    (ssym Hfg)). }
+eapply lemma. simpl.
+refine (J_seqs _ _ (fun X _ => (fun r β => wedge ⋅ ce_f0 (X r β)) ≡ _) (srefl _) (α ⋅ e0) (ssym (e1 q α))).
+Defined.
+
+
+(* that one is more or less contr_filler0 with some packaging *)
+(* todo : prove it from contr_filler0 *)
+Definition singl_contr0 {p}
+  (A0 : @El0 p Type0)
+  (A1 : @El1 p Type0 Type1 A0)
+  (a0 : El0 A0)
+  (a1 : El1 A0 A1 a0)
+  (b0 : El0 A0)
+  (b1 : El1 A0 A1 b0)
+  (e0 : El0 (eq0 A0 A1 a0 a1 b0 b1))
+  (e1 : El1 _ (eq1 A0 A1 a0 a1 b0 b1) e0)
+  : El0 (eq0
+    (Sigma0 A0 A1 (fun q α x0 x1 => eq0 (α ⋅ A0) (α ⋅ A1) (α ⋅ a0) (α ⋅ a1) x0 x1 q !) (fun q α x0 x1 => eq1 (α ⋅ A0) (α ⋅ A1) (α ⋅ a0) (α ⋅ a1) x0 x1 q !))
+    (Sigma1 A0 A1 (fun q α x0 x1 => eq0 (α ⋅ A0) (α ⋅ A1) (α ⋅ a0) (α ⋅ a1) x0 x1 q !) (fun q α x0 x1 => eq1 (α ⋅ A0) (α ⋅ A1) (α ⋅ a0) (α ⋅ a1) x0 x1 q !))
+    (dpair0 a0 a1 (eq_refl0 A0 A1 a0 a1) (eq_refl1 A0 A1 a0 a1))
+    (dpair1 a0 a1 (eq_refl0 A0 A1 a0 a1) (eq_refl1 A0 A1 a0 a1))
+    (dpair0 b0 b1 e0 e1)
+    (dpair1 b0 b1 e0 e1)).
+Proof.
+refine (fun q α => _) ; simpl.
+unshelve econstructor.
+- refine (fun r β => _) ; simpl.
+  unshelve econstructor.
+  + exact (β ⋅ ce_f0 (e0 q α)).
+  + exact (β ⋅ ce_f1 (e0 q α)).
+  + refine (fun r0 β0 => _) ; simpl.
+    unshelve econstructor.
+    * change (El0 (α ∘ squish ∘ wedge ∘ promote β ∘ promote β0 ⋅ A0)).
+      exact (wedge ∘ promote β ∘ promote β0 ⋅ (ce_f0 (e0 q α))).
+    * exact (wedge ∘ promote β ∘ promote β0 ⋅ (ce_f1 (e0 q α))).
+    * refine (J_seqs _ _ (fun X _ => _ ≡ β ∘ β0 ⋅ (squish ⋅ X)) _ _ (ce_s (e0 q α))).
+      change (β ∘ β0 ⋅ (wedge ∘ side_0 ⋅ ce_f0 (e0 q α)) ≡ β ∘ β0 ⋅ (side_0 ∘ squish ⋅ (ce_f0 (e0 q α)))).
+      (* here we would need some more computation *)
+      apply sfalso.
+    * change (β ∘ β0 ⋅ (wedge ∘ side_1 ⋅ ce_f0 (e0 q α)) ≡ β ∘ β0 ⋅ (ce_f0 (e0 q α))).
+      (* here too *)
+      apply sfalso.
+  + refine (fun r0 β0 => _) ; simpl.
+    reflexivity.
+- refine (fun r β => _) ; simpl.
+  reflexivity.
+- admit.
+- admit.
+Admitted.
+
+
+Definition singl_contr1 {p}
+  (A0 : @El0 p Type0)
+  (A1 : @El1 p Type0 Type1 A0)
+  (a0 : El0 A0)
+  (a1 : El1 A0 A1 a0)
+  (b0 : El0 A0)
+  (b1 : El1 A0 A1 b0)
+  (e0 : El0 (eq0 A0 A1 a0 a1 b0 b1))
+  (e1 : El1 _ (eq1 A0 A1 a0 a1 b0 b1) e0)
+  : El1 _ (eq1
+    (Sigma0 A0 A1 (fun q α x0 x1 => eq0 (α ⋅ A0) (α ⋅ A1) (α ⋅ a0) (α ⋅ a1) x0 x1 q !) (fun q α x0 x1 => eq1 (α ⋅ A0) (α ⋅ A1) (α ⋅ a0) (α ⋅ a1) x0 x1 q !))
+    (Sigma1 A0 A1 (fun q α x0 x1 => eq0 (α ⋅ A0) (α ⋅ A1) (α ⋅ a0) (α ⋅ a1) x0 x1 q !) (fun q α x0 x1 => eq1 (α ⋅ A0) (α ⋅ A1) (α ⋅ a0) (α ⋅ a1) x0 x1 q !))
+    (dpair0 a0 a1 (eq_refl0 A0 A1 a0 a1) (eq_refl1 A0 A1 a0 a1))
+    (dpair1 a0 a1 (eq_refl0 A0 A1 a0 a1) (eq_refl1 A0 A1 a0 a1))
+    (dpair0 b0 b1 e0 e1)
+    (dpair1 b0 b1 e0 e1))
+    (singl_contr0 A0 A1 a0 a1 b0 b1 e0 e1).
+Proof.
+refine (fun q α => _). simpl.
+(* komarimasu… *)
+Admitted.
diff --git a/theories/translation_fib.v b/theories/translation_fib.v
index b36e599..20ed1be 100644
--- a/theories/translation_fib.v
+++ b/theories/translation_fib.v
@@ -569,6 +569,155 @@ intros [a0 a1 b0 b1].
 exact (Sigma_c _ _ _ _ (α ⋅ a0) (α ⋅ a1) (α ⋅ b0) (α ⋅ b1)).
 Defined.
 
+Definition SigmaR {p}
+  (A0 : @El0 p Type0)
+  (A1 : @El1 p Type0 Type1 A0)
+  (P0 : El0 (Arr0 A0 A1 Type0 Type1))
+  (P1 : El1 _ (Arr1 A0 A1 Type0 Type1) P0)
+  : (forall q (α : q ≤ p), SigmaT (α ⋅ A0) (α ⋅ A1) (α ⋅ P0) (α ⋅ P1)) -> SProp :=
+fun s => s ≡ fun q α => SigmaT_funct α (s p !).
+
+Definition Sigma0 {p}
+  (A0 : @El0 p Type0)
+  (A1 : @El1 p Type0 Type1 A0)
+  (P0 : El0 (Arr0 A0 A1 Type0 Type1))
+  (P1 : El1 _ (Arr1 A0 A1 Type0 Type1) P0) :
+  @El0 p Type0.
+Proof.
+refine (fun q α => _).
+unshelve econstructor.
+- refine (fun r β => _).
+  exact (SigmaT (α ∘ β ⋅ A0) (α ∘ β ⋅ A1) (α ∘ β ⋅ P0) (α ∘ β ⋅ P1)).
+- refine (fun r β => _).
+  exact (SigmaR (α ∘ β ⋅ A0) (α ∘ β ⋅ A1) (α ∘ β ⋅ P0) (α ∘ β ⋅ P1)).
+- refine (fun r β b e l le l' => _).
+  apply falso.
+Defined.
+
+Definition Sigma1 {p}
+  (A0 : @El0 p Type0)
+  (A1 : @El1 p Type0 Type1 A0)
+  (P0 : El0 (Arr0 A0 A1 Type0 Type1))
+  (P1 : El1 _ (Arr1 A0 A1 Type0 Type1) P0) :
+  @El1 p Type0 Type1 (Sigma0 A0 A1 P0 P1).
+Proof.
+refine (fun q α => _).
+reflexivity.
+Defined.
+
+Definition fst0 {p}
+  {A0 : @El0 p Type0}
+  {A1 : @El1 p Type0 Type1 A0}
+  {P0 : El0 (Arr0 A0 A1 Type0 Type1)}
+  {P1 : El1 _ (Arr1 A0 A1 Type0 Type1) P0}
+  (x0 : El0 (Sigma0 A0 A1 P0 P1)) :
+  El0 A0.
+Proof.
+destruct (x0 p !) as [a0 a1 b0 b1].
+exact a0.
+Defined.
+
+Definition fst1 {p}
+  {A0 : @El0 p Type0}
+  {A1 : @El1 p Type0 Type1 A0}
+  {P0 : El0 (Arr0 A0 A1 Type0 Type1)}
+  {P1 : El1 _ (Arr1 A0 A1 Type0 Type1) P0}
+  (x0 : El0 (Sigma0 A0 A1 P0 P1)) :
+  El1 A0 A1 (fst0 x0).
+Proof.
+unfold fst0.
+destruct (x0 p !) as [a0 a1 b0 b1].
+exact a1.
+Defined.
+
+Definition snd0 {p}
+  {A0 : @El0 p Type0}
+  {A1 : @El1 p Type0 Type1 A0}
+  {P0 : El0 (Arr0 A0 A1 Type0 Type1)}
+  {P1 : El1 _ (Arr1 A0 A1 Type0 Type1) P0}
+  (x0 : El0 (Sigma0 A0 A1 P0 P1)) :
+  El0 (app0 P0 (fst0 x0) (fst1 x0)).
+Proof.
+unfold fst0. unfold fst1.
+destruct (x0 p !) as [a0 a1 b0 b1].
+exact b0.
+Defined.
+
+Definition snd1 {p}
+  {A0 : @El0 p Type0}
+  {A1 : @El1 p Type0 Type1 A0}
+  {P0 : El0 (Arr0 A0 A1 Type0 Type1)}
+  {P1 : El1 _ (Arr1 A0 A1 Type0 Type1) P0}
+  (x0 : El0 (Sigma0 A0 A1 P0 P1)) :
+  El1 _ (app1 P1 (fst0 x0) (fst1 x0)) (snd0 x0).
+Proof.
+unfold fst0. unfold fst1. unfold snd0.
+destruct (x0 p !) as [a0 a1 b0 b1].
+exact b1.
+Defined.
+
+Definition seq_Sigma_transp {p}
+  {A0 : @El0 p Type0}
+  {A1 : @El1 p Type0 Type1 A0}
+  {P0 : El0 (Arr0 A0 A1 Type0 Type1)}
+  {P1 : El1 _ (Arr1 A0 A1 Type0 Type1) P0}
+  {a0 : El0 (Sigma0 A0 A1 P0 P1)}
+  {b0 : El0 (Sigma0 A0 A1 P0 P1)}
+  : fst0 a0 ≡ fst0 b0 ->
+    El0 (app0 P0 (fst0 a0) (fst1 a0)) ->
+    El0 (app0 P0 (fst0 b0) (fst1 b0)).
+Proof.
+refine (fun H x => _).
+refine (J_seq _ (fst0 a0)
+  (fun x e => El0 (app0 P0 x
+    (J_seqs _ (fst0 a0) (fun y _ => El1 A0 A1 y) (fst1 a0) x e)))
+  x (fst0 b0) H).
+Defined.
+
+Definition seq_Sigma {p}
+  {A0 : @El0 p Type0}
+  {A1 : @El1 p Type0 Type1 A0}
+  {P0 : El0 (Arr0 A0 A1 Type0 Type1)}
+  {P1 : El1 _ (Arr1 A0 A1 Type0 Type1) P0}
+  (a0 : El0 (Sigma0 A0 A1 P0 P1))
+  (a1 : El1 _ (Sigma1 A0 A1 P0 P1) a0)
+  (b0 : El0 (Sigma0 A0 A1 P0 P1))
+  (b1 : El1 _ (Sigma1 A0 A1 P0 P1) b0)
+  : forall (e0 : fst0 a0 ≡ fst0 b0)
+    (e1 : seq_Sigma_transp e0 (snd0 a0) ≡ snd0 b0),
+    a0 ≡ b0.
+Proof.
+refine (fun H0 H1 => _).
+refine (J_seqs _ _ (fun x _ => x ≡ b0) _ a0 (ssym (a1 p !))).
+unfold cast0 ; simpl.
+assert (a0 p ! ≡ b0 p !).
+admit.
+refine (J_seqs _ _ (fun x _ => (fun q α => SigmaT_funct α x) ≡ b0) _ _ (ssym H)).
+exact (ssym (b1 p !)).
+Admitted.
+
+(* Inductive SigmaT {p}
+  (A0 : @El0 p Type0)
+  (A1 : @El1 p Type0 Type1 A0)
+  (P0 : El0 (Arr0 A0 A1 Type0 Type1))
+  (P1 : El1 _ (Arr1 A0 A1 Type0 Type1) P0) :
+  Type :=
+| Sigma_c : forall (a0 : El0 A0) (a1 : El1 A0 A1 a0)
+  (b0 : El0 (app0 P0 a0 a1)) (b1 : El1 _ (app1 P1 a0 a1) b0),
+  SigmaT A0 A1 P0 P1.
+
+Definition SigmaT_funct {p}
+  {A0 : @El0 p Type0}
+  {A1 : @El1 p Type0 Type1 A0}
+  {P0 : El0 (Arr0 A0 A1 Type0 Type1)}
+  {P1 : El1 _ (Arr1 A0 A1 Type0 Type1) P0}
+  {q} (α : q ≤ p) :
+  SigmaT A0 A1 P0 P1 -> SigmaT (α ⋅ A0) (α ⋅ A1) (α ⋅ P0) (α ⋅ P1).
+Proof.
+intros [a0 a1 b0 b1].
+exact (Sigma_c _ _ _ _ (α ⋅ a0) (α ⋅ a1) (α ⋅ b0) (α ⋅ b1)).
+Defined.
+
 Definition fst0_SigmaT {p}
   {A0 : @El0 p Type0}
   {A1 : @El1 p Type0 Type1 A0}
@@ -683,7 +832,7 @@ Definition Sigma1 {p}
 Proof.
 refine (fun q α => _).
 reflexivity.
-Defined.
+Defined. *)
 
 Definition dpair0 {p}
   {A0 : @El0 p Type0}
@@ -901,424 +1050,3 @@ unshelve refine (fun q α => _).
 reflexivity.
 Defined.
 
-(* shifted types *)
-
-Record shifted_ty {p} : Type :=
-mkST {
-  st_t0 : @El0 (S p) (squish ⋅ Type0) ;
-  st_t1 : @El1 (S p) (squish ⋅ Type0) (squish ⋅ Type1) st_t0 ;
-}.
-
-Definition st_funct {p} {q} (α : q ≤ p) :
-  @shifted_ty p -> @shifted_ty q.
-Proof.
-unshelve refine (fun x => _).
-unshelve econstructor.
-- exact (promote α ⋅ x.(st_t0)).
-- exact (promote α ⋅ x.(st_t1)).
-Defined.
-
-Definition shifted_tyR {p} :
- (forall q (α : q ≤ p), @shifted_ty q) -> SProp :=
-fun s => s ≡ fun q α => st_funct α (s p !).
-
-Definition shiftedType0 {p}
-  : @El0 p Type0.
-Proof.
-unshelve refine (fun q α => mkYFT _ _ _ _).
-- unshelve refine (fun r β => _).
-  exact (@shifted_ty r).
-- unshelve refine (fun r β s => _). simpl in s.
-  exact (shifted_tyR s).
-- unshelve refine (fun r β b e l le l' => _).
-  apply falso. (** TODO **)
-Defined.
-
-Definition shiftedType1 {p}
-  : @El1 p Type0 Type1 shiftedType0.
-Proof.
-refine (fun q α => _). reflexivity.
-Defined.
-
-Definition shiftedTypeStart0 {p}
-  (A0 : @El0 p shiftedType0)
-  (A1 : @El1 p shiftedType0 shiftedType1 A0) :
-  @El0 p Type0.
-Proof.
-refine (fun q α => _).
-refine ((side_0 ⋅ st_t0 (A0 q α)) q !). 
-Defined.
-
-Definition shiftedTypeStart1 {p}
-  (A0 : @El0 p shiftedType0)
-  (A1 : @El1 p shiftedType0 shiftedType1 A0) :
-  @El1 p Type0 Type1 (shiftedTypeStart0 A0 A1).
-Proof.
-refine (fun q α => _). 
-refine (J_seqs _ _ (fun X _ => yftR (fun r β => st_t0 (X r β) r side_0 )) _ (α ⋅ A0) (ssym (A1 q α))).
-refine ((side_0 ⋅ st_t1 (A0 q α)) q !).
-Defined.
-
-Definition shiftedTypeEnd0 {p}
-  (A0 : @El0 p shiftedType0)
-  (A1 : @El1 p shiftedType0 shiftedType1 A0) :
-  @El0 p Type0.
-Proof.
-refine (fun q α => _).
-refine ((side_1 ⋅ st_t0 (A0 q α)) q !). 
-Defined.
-
-Definition shiftedTypeEnd1 {p}
-  (A0 : @El0 p shiftedType0)
-  (A1 : @El1 p shiftedType0 shiftedType1 A0) :
-  @El1 p Type0 Type1 (shiftedTypeEnd0 A0 A1).
-Proof.
-refine (fun q α => _). 
-refine (J_seqs _ _ (fun X _ => yftR (fun r β => st_t0 (X r β) r side_1)) _ (α ⋅ A0) (ssym (A1 q α))).
-refine ((side_1 ⋅ st_t1 (A0 q α)) q !).
-Defined.
-
-(* a predicate over an equality is a shifted type *)
-
-Definition eqToShiftedType0 {p}
-  (A0 : @El0 p Type0)
-  (A1 : @El1 p Type0 Type1 A0)
-  (P0 : El0 (Arr0 A0 A1 Type0 Type1))
-  (P1 : El1 _ (Arr1 A0 A1 Type0 Type1) P0)
-  (a0 : El0 A0)
-  (a1 : El1 A0 A1 a0)
-  (b0 : El0 A0)
-  (b1 : El1 A0 A1 b0)
-  (e0 : El0 (eq0 A0 A1 a0 a1 b0 b1))
-  (e1 : El1 _ (eq1 A0 A1 a0 a1 b0 b1) e0) :
-  @El0 p shiftedType0.
-Proof.
-refine (fun q α => _).
-unshelve econstructor.
-- refine (fun r β => P0 r (α ∘ squish ∘ β) (β ⋅ (ce_f0 (e0 q α))) (β ⋅ ce_f1 (e0 q α))).
-- refine (@app1 (S q) _ _ Type0 Type1 (α ∘ squish ⋅ P0) (α ∘ squish ⋅ P1) (ce_f0 (e0 q α)) (ce_f1 (e0 q α))).
-Defined.
-
-Definition eqToShiftedType1 {p}
-  (A0 : @El0 p Type0)
-  (A1 : @El1 p Type0 Type1 A0)
-  (P0 : El0 (Arr0 A0 A1 Type0 Type1))
-  (P1 : El1 _ (Arr1 A0 A1 Type0 Type1) P0)
-  (a0 : El0 A0)
-  (a1 : El1 A0 A1 a0)
-  (b0 : El0 A0)
-  (b1 : El1 A0 A1 b0)
-  (e0 : El0 (eq0 A0 A1 a0 a1 b0 b1))
-  (e1 : El1 _ (eq1 A0 A1 a0 a1 b0 b1) e0) :
-  @El1 p shiftedType0 shiftedType1 (eqToShiftedType0 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1).
-Proof.
-refine (fun q α => _).
-unfold cast0 ; simpl. unfold shifted_tyR ; simpl.
-change (eqToShiftedType0 (α ⋅ A0) (α ⋅ A1) (α ⋅ P0) (α ⋅ P1) (α ⋅ a0) (α ⋅ a1) (α ⋅ b0) (α ⋅ b1) (α ⋅ e0) (α ⋅ e1) ≡ (fun r β => st_funct β (eqToShiftedType0 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1 q α))).
-pose proof (e1 q α) as He. unfold cast0 in He ; simpl in He.
-unfold cube_eqR in He.
-refine (J_seqs _ _ 
-  (fun X e => eqToShiftedType0 _ _ _ _ _ _ _ _ X 
-    (J_seqs _ _ (fun Y _ => El1 _ (eq1 (α ⋅ A0) (α ⋅ A1) (α ⋅ a0) (α ⋅ a1) (α ⋅ b0) (α ⋅ b1)) Y) 
-      (J_seqs _ (α ⋅ e0) (fun Z _ => El1 _ (eq1 (α ⋅ A0) (α ⋅ A1) (α ⋅ a0) (α ⋅ a1) (α ⋅ b0) (α ⋅ b1)) Z) (α ⋅ e1) _ He) 
-      X e) 
-    ≡ _) 
-  _ (α ⋅ e0) (ssym He)).
-reflexivity.
-Defined.
-
-(* transport boils down to a statement about shifted types *)
-
-Definition transp0 {p}
-  (A0 : @El0 p shiftedType0)
-  (A1 : @El1 p shiftedType0 shiftedType1 A0)
-  (s0 : El0 (shiftedTypeStart0 A0 A1))
-  (s1 : El1 _ (shiftedTypeStart1 A0 A1) s0)
-  : El0 (shiftedTypeEnd0 A0 A1).
-Proof.
-refine (fun q α => _).
-unfold shiftedTypeEnd0 ; simpl.
-unfold El0 in s0 ; unfold shiftedTypeStart0 in s0 ; simpl in s0. 
-change (forall q α, yft0 (st_t0 (A0 q α) q side_0) q !) in s0.
-unfold El0 in A0 ; simpl in A0.
-
-refine (J_seq _ _ (fun X _ => yft0 (X q side_1) q !) _ _ (ssym (st_t1 (A0 q α) (S q) !))).
-change (yft0 (st_t0 (A0 q α) (S q) !) q side_1).
-
-unshelve refine (let s'0 : yft0 (st_t0 (A0 q α) (S q) !) q side_0 := _ in _).
-{ pose proof (st_t1 (A0 q α) (S q) !) as H. change (yftR (st_t0 (A0 q α))) in H. unfold yftR in H.
-  refine (J_seq _ _ (fun X _ => yft0 (X q side_0) q !) _ _ H).
-  refine (s0 q α). }
-
-Admitted.
-
-Definition transp1 {p}
-  (A0 : @El0 p shiftedType0)
-  (A1 : @El1 p shiftedType0 shiftedType1 A0)
-  (s0 : El0 (shiftedTypeStart0 A0 A1))
-  (s1 : El1 _ (shiftedTypeStart1 A0 A1) s0)
-  : El1 _ (shiftedTypeEnd1 A0 A1) (transp0 A0 A1 s0 s1).
-Proof.
-Admitted.
-
-Definition transport_aux1_0 {p}
-  (A0 : @El0 p Type0)
-  (A1 : @El1 p Type0 Type1 A0)
-  (P0 : El0 (Arr0 A0 A1 Type0 Type1))
-  (P1 : El1 _ (Arr1 A0 A1 Type0 Type1) P0)
-  (a0 : El0 A0)
-  (a1 : El1 A0 A1 a0)
-  (x0 : El0 (app0 P0 a0 a1))
-  (x1 : El1 _ (app1 P1 a0 a1) x0)
-  (b0 : El0 A0)
-  (b1 : El1 A0 A1 b0)
-  (e0 : El0 (eq0 A0 A1 a0 a1 b0 b1))
-  (e1 : El1 _ (eq1 A0 A1 a0 a1 b0 b1) e0) :
-  El0 (shiftedTypeStart0 (eqToShiftedType0 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1) (eqToShiftedType1 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1)).
-Proof.
-refine (fun q α => _).
-change (yft0 (P0 q α (side_0 ⋅ ce_f0 (e0 q α)) (side_0 ⋅ ce_f1 (e0 q α))) q !).
-refine (J_seq _ (α ⋅ a0) 
-  (fun X E => yft0 (P0 q α X 
-    (J_seqs _ _ (fun Y _ => El1 (α ⋅ A0) (α ⋅ A1) Y) (α ⋅ a1) X E)) 
-    q !)
-  _ _ (ssym (ce_s (e0 q α)))).
-refine (x0 q α).
-Defined.
-
-Definition transport_aux1_1 {p}
-  (A0 : @El0 p Type0)
-  (A1 : @El1 p Type0 Type1 A0)
-  (P0 : El0 (Arr0 A0 A1 Type0 Type1))
-  (P1 : El1 _ (Arr1 A0 A1 Type0 Type1) P0)
-  (a0 : El0 A0)
-  (a1 : El1 A0 A1 a0)
-  (x0 : El0 (app0 P0 a0 a1))
-  (x1 : El1 _ (app1 P1 a0 a1) x0)
-  (b0 : El0 A0)
-  (b1 : El1 A0 A1 b0)
-  (e0 : El0 (eq0 A0 A1 a0 a1 b0 b1))
-  (e1 : El1 _ (eq1 A0 A1 a0 a1 b0 b1) e0) :
-  El1 _ (shiftedTypeStart1 (eqToShiftedType0 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1) (eqToShiftedType1 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1)) (transport_aux1_0 A0 A1 P0 P1 a0 a1 x0 x1 b0 b1 e0 e1).
-Proof.
-refine (fun q α => _). 
-unfold transport_aux1_0 ; simpl.
-unfold shiftedTypeStart0 ; unfold eqToShiftedType0 at 1 2 ; simpl.
-(* unfolding shiftedTypeStart1 unleashes hell *)
-Admitted.
-
-Definition transport_aux2_0 {p}
-  (A0 : @El0 p Type0)
-  (A1 : @El1 p Type0 Type1 A0)
-  (P0 : El0 (Arr0 A0 A1 Type0 Type1))
-  (P1 : El1 _ (Arr1 A0 A1 Type0 Type1) P0)
-  (a0 : El0 A0)
-  (a1 : El1 A0 A1 a0)
-  (b0 : El0 A0)
-  (b1 : El1 A0 A1 b0)
-  (e0 : El0 (eq0 A0 A1 a0 a1 b0 b1))
-  (e1 : El1 _ (eq1 A0 A1 a0 a1 b0 b1) e0)
-  (x0 : El0 (shiftedTypeEnd0 (eqToShiftedType0 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1) (eqToShiftedType1 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1)))
-  (x1 : El1 _ (shiftedTypeEnd1 (eqToShiftedType0 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1) (eqToShiftedType1 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1)) x0) :
-  El0 (app0 P0 b0 b1).
-Proof.
-refine (fun q α => _).
-change (yft0 (P0 q α (α ⋅ b0) (α ⋅ b1)) q !).
-refine (J_seq _ _ 
-  (fun X E => yft0 (P0 q α X 
-    (J_seqs _ _ (fun Y _ => El1 (α ⋅ A0) (α ⋅ A1) Y) 
-      (J_seqs _ (α ⋅ b0) (fun Z _ => El1 (α ⋅ A0) (α ⋅ A1) Z) (α ⋅ b1) _ (ssym (ce_t (e0 q α)))) X E)) 
-    q !)
-  _ (α ⋅ b0) (ce_t (e0 q α))).
-change (yft0 (P0 q α (side_1 ⋅ ce_f0 (e0 q α)) (side_1 ⋅ ce_f1 (e0 q α))) q !).
-refine (x0 q α).
-Defined.
-
-Definition transport_aux2_1 {p}
-  (A0 : @El0 p Type0)
-  (A1 : @El1 p Type0 Type1 A0)
-  (P0 : El0 (Arr0 A0 A1 Type0 Type1))
-  (P1 : El1 _ (Arr1 A0 A1 Type0 Type1) P0)
-  (a0 : El0 A0)
-  (a1 : El1 A0 A1 a0)
-  (b0 : El0 A0)
-  (b1 : El1 A0 A1 b0)
-  (e0 : El0 (eq0 A0 A1 a0 a1 b0 b1))
-  (e1 : El1 _ (eq1 A0 A1 a0 a1 b0 b1) e0)
-  (x0 : El0 (shiftedTypeEnd0 (eqToShiftedType0 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1) (eqToShiftedType1 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1)))
-  (x1 : El1 _ (shiftedTypeEnd1 (eqToShiftedType0 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1) (eqToShiftedType1 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1)) x0) :
-  El1 (app0 P0 b0 b1) (app1 P1 b0 b1) (transport_aux2_0 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1 x0 x1).
-Proof.
-Admitted.
-
-Definition transport0 {p}
-  (A0 : @El0 p Type0)
-  (A1 : @El1 p Type0 Type1 A0)
-  (P0 : El0 (Arr0 A0 A1 Type0 Type1))
-  (P1 : El1 _ (Arr1 A0 A1 Type0 Type1) P0)
-  (a0 : El0 A0)
-  (a1 : El1 A0 A1 a0)
-  (x0 : El0 (app0 P0 a0 a1))
-  (x1 : El1 _ (app1 P1 a0 a1) x0)
-  (b0 : El0 A0)
-  (b1 : El1 A0 A1 b0)
-  (e0 : El0 (eq0 A0 A1 a0 a1 b0 b1))
-  (e1 : El1 _ (eq1 A0 A1 a0 a1 b0 b1) e0) :
-  El0 (app0 P0 b0 b1).
-Proof.
-refine (transport_aux2_0 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1 
-  (transp0 (eqToShiftedType0 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1) (eqToShiftedType1 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1)
-    (transport_aux1_0 A0 A1 P0 P1 a0 a1 x0 x1 b0 b1 e0 e1)
-    (transport_aux1_1 A0 A1 P0 P1 a0 a1 x0 x1 b0 b1 e0 e1))
-  (transp1 (eqToShiftedType0 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1) (eqToShiftedType1 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1)
-    (transport_aux1_0 A0 A1 P0 P1 a0 a1 x0 x1 b0 b1 e0 e1)
-    (transport_aux1_1 A0 A1 P0 P1 a0 a1 x0 x1 b0 b1 e0 e1))).
-Defined.
-
-Definition transport1 {p}
-  (A0 : @El0 p Type0)
-  (A1 : @El1 p Type0 Type1 A0)
-  (P0 : El0 (Arr0 A0 A1 Type0 Type1))
-  (P1 : El1 _ (Arr1 A0 A1 Type0 Type1) P0)
-  (a0 : El0 A0)
-  (a1 : El1 A0 A1 a0)
-  (x0 : El0 (app0 P0 a0 a1))
-  (x1 : El1 _ (app1 P1 a0 a1) x0)
-  (b0 : El0 A0)
-  (b1 : El1 A0 A1 b0)
-  (e0 : El0 (eq0 A0 A1 a0 a1 b0 b1))
-  (e1 : El1 _ (eq1 A0 A1 a0 a1 b0 b1) e0) :
-  El1 (app0 P0 b0 b1) (app1 P1 b0 b1) (transport0 A0 A1 P0 P1 a0 a1 x0 x1 b0 b1 e0 e1).
-Proof.
-refine (transport_aux2_1 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1 
-  (transp0 (eqToShiftedType0 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1) (eqToShiftedType1 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1)
-    (transport_aux1_0 A0 A1 P0 P1 a0 a1 x0 x1 b0 b1 e0 e1)
-    (transport_aux1_1 A0 A1 P0 P1 a0 a1 x0 x1 b0 b1 e0 e1))
-  (transp1 (eqToShiftedType0 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1) (eqToShiftedType1 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1)
-    (transport_aux1_0 A0 A1 P0 P1 a0 a1 x0 x1 b0 b1 e0 e1)
-    (transport_aux1_1 A0 A1 P0 P1 a0 a1 x0 x1 b0 b1 e0 e1))).
-Defined.
-
-
-(* contractibility of singletons *)
-
-Definition singl_contr0 {p}
-  (A0 : @El0 p Type0)
-  (A1 : @El1 p Type0 Type1 A0)
-  (a0 : El0 A0)
-  (a1 : El1 A0 A1 a0)
-  (b0 : El0 A0)
-  (b1 : El1 A0 A1 b0)
-  (e0 : El0 (eq0 A0 A1 a0 a1 b0 b1))
-  (e1 : El1 _ (eq1 A0 A1 a0 a1 b0 b1) e0)
-  : El0 (eq0
-    (Sigma0 A0 A1 (fun q α x0 x1 => eq0 (α ⋅ A0) (α ⋅ A1) (α ⋅ a0) (α ⋅ a1) x0 x1 q !) (fun q α x0 x1 => eq1 (α ⋅ A0) (α ⋅ A1) (α ⋅ a0) (α ⋅ a1) x0 x1 q !))
-    (Sigma1 A0 A1 (fun q α x0 x1 => eq0 (α ⋅ A0) (α ⋅ A1) (α ⋅ a0) (α ⋅ a1) x0 x1 q !) (fun q α x0 x1 => eq1 (α ⋅ A0) (α ⋅ A1) (α ⋅ a0) (α ⋅ a1) x0 x1 q !))
-    (dpair0 a0 a1 (eq_refl0 A0 A1 a0 a1) (eq_refl1 A0 A1 a0 a1))
-    (dpair1 a0 a1 (eq_refl0 A0 A1 a0 a1) (eq_refl1 A0 A1 a0 a1))
-    (dpair0 b0 b1 e0 e1)
-    (dpair1 b0 b1 e0 e1)).
-Proof.
-Admitted.
-
-Definition singl_contr1 {p}
-  (A0 : @El0 p Type0)
-  (A1 : @El1 p Type0 Type1 A0)
-  (a0 : El0 A0)
-  (a1 : El1 A0 A1 a0)
-  (b0 : El0 A0)
-  (b1 : El1 A0 A1 b0)
-  (e0 : El0 (eq0 A0 A1 a0 a1 b0 b1))
-  (e1 : El1 _ (eq1 A0 A1 a0 a1 b0 b1) e0)
-  : El1 _ (eq1
-    (Sigma0 A0 A1 (fun q α x0 x1 => eq0 (α ⋅ A0) (α ⋅ A1) (α ⋅ a0) (α ⋅ a1) x0 x1 q !) (fun q α x0 x1 => eq1 (α ⋅ A0) (α ⋅ A1) (α ⋅ a0) (α ⋅ a1) x0 x1 q !))
-    (Sigma1 A0 A1 (fun q α x0 x1 => eq0 (α ⋅ A0) (α ⋅ A1) (α ⋅ a0) (α ⋅ a1) x0 x1 q !) (fun q α x0 x1 => eq1 (α ⋅ A0) (α ⋅ A1) (α ⋅ a0) (α ⋅ a1) x0 x1 q !))
-    (dpair0 a0 a1 (eq_refl0 A0 A1 a0 a1) (eq_refl1 A0 A1 a0 a1))
-    (dpair1 a0 a1 (eq_refl0 A0 A1 a0 a1) (eq_refl1 A0 A1 a0 a1))
-    (dpair0 b0 b1 e0 e1)
-    (dpair1 b0 b1 e0 e1))
-    (singl_contr0 A0 A1 a0 a1 b0 b1 e0 e1).
-Proof.
-Admitted.
-
-(* weak univalence *)
-
-Definition glueTypeAux (p : ℙ) (A B : Type) : (p ≤ 1) -> Type :=
-fun αi => if (is_i0 αi) then A else B.
-
-Definition glueTypeAux_i0 {p : ℙ} {A B : Type} : glueTypeAux p A B i0 ≡ A :=
-J_seqs bool true (fun X _ => (if X then A else B) ≡ A) (srefl _) (is_i0 i0) (ssym is_i0_i0).
-
-Definition glueTypeAux_i1 {p : ℙ} {A B : Type} : glueTypeAux p A B i1 ≡ B :=
-J_seqs bool false (fun X _ => (if X then A else B) ≡ B) (srefl _) (is_i0 i1) (ssym is_i0_i1).
-
-Definition glueType (p : ℙ) (A B : Type) : itype p Type A B.
-Proof.
-refine (J_seq _ (glueTypeAux p A B i0) (fun X _ => itype p Type X B) _ _ (glueTypeAux_i0)).
-refine (J_seq _ (glueTypeAux p A B i1) (fun X _ => itype p Type (glueTypeAux p A B i0) X) _ _ (glueTypeAux_i1)).
-refine (itype_in (glueTypeAux p A B)).
-Defined.
-
-Definition weakunivalence0 {p}
-  (A0 : @El0 p Type0)
-  (A1 : @El1 p Type0 Type1 A0)
-  (B0 : @El0 p Type0)
-  (B1 : @El1 p Type0 Type1 B0)
-  : El0 (eq0 Type0 Type1 A0 A1 B0 B1).
-Proof.
-refine (fun q α => _).
-unshelve econstructor.
-- refine (fun r β => _).
-  unshelve econstructor.
-  + refine (fun r0 β0 => _).
-    refine (itype_out (glueType r0 (yft0 (A0 r0 (α ∘ squish ∘ β ∘ β0)) r0 !) (yft0 (B0 r0 (α ∘ squish ∘ β ∘ β0)) r0 !)) (antisquish ∘ β ∘ β0)).
-  + refine (fun r0 β0 s => _) ; simpl in s.
-    admit.
-  + refine (fun r0 β0 a b c d e => _).
-    admit.
-- refine (fun r β r0 β0 => _). unfold cast0 ; simpl. reflexivity.
-- simpl.
-Admitted.
-
-(* incomplete funext proof. for complete proof, see translation_fib_path.v *)
-
-Definition eq_funext {p}
-(A0 : @El0 p Type0)
-(A1 : @El1 p Type0 Type1 A0)
-(B0 : @El0 p Type0)
-(B1 : @El1 p Type0 Type1 B0)
-(f0 : El0 (Arr0 A0 A1 B0 B1))
-(f1 : El1 _ (Arr1 A0 A1 B0 B1) f0)
-(g0 : El0 (Arr0 A0 A1 B0 B1))
-(g1 : El1 _ (Arr1 A0 A1 B0 B1) g0)
-(h0 : El0 (Prod0 A0 A1
-  (fun q α x0 x1 => eq0 (α ⋅ B0) (α ⋅ B1)
-    (app0 (α ⋅ f0) x0 x1) (app1 (α ⋅ f1) x0 x1)
-    (app0 (α ⋅ g0) x0 x1) (app1 (α ⋅ g1) x0 x1) q !)
-  (fun q α x0 x1 => eq1 (α ⋅ B0) (α ⋅ B1)
-    (app0 (α ⋅ f0) x0 x1) (app1 (α ⋅ f1) x0 x1)
-    (app0 (α ⋅ g0) x0 x1) (app1 (α ⋅ g1) x0 x1) q !)
-  ))
-(h1 : El1 _ (Prod1 A0 A1
-  (fun q α x0 x1 => eq0 (α ⋅ B0) (α ⋅ B1)
-    (app0 (α ⋅ f0) x0 x1) (app1 (α ⋅ f1) x0 x1)
-    (app0 (α ⋅ g0) x0 x1) (app1 (α ⋅ g1) x0 x1) q !)
-  (fun q α x0 x1 => eq1 (α ⋅ B0) (α ⋅ B1)
-    (app0 (α ⋅ f0) x0 x1) (app1 (α ⋅ f1) x0 x1)
-    (app0 (α ⋅ g0) x0 x1) (app1 (α ⋅ g1) x0 x1) q !)
-  ) h0)
-: El0 (eq0 (Arr0 A0 A1 B0 B1) (Arr1 A0 A1 B0 B1) f0 f1 g0 g1).
-Proof.
-refine (fun q α => _).
-unshelve econstructor.
-- refine (fun r β x0 x1 => _).
-  refine (@itype_out r (yft0 (B0 r (α ∘ squish ∘ β)) r !)
-    (f0 r (α ∘ squish ∘ β) x0 x1) (g0 r (α ∘ squish ∘ β) x0 x1)
-    _ (antisquish ∘ β)).
-  refine (J_seq _ _ (fun X _ => itype _ _ (X r !) _) _ _ ((h0 r (α ∘ squish ∘ β) x0 x1).(ce_s))).
-  refine (J_seq _ _ (fun X _ => itype _ _ _ (X r !)) _ _ ((h0 r (α ∘ squish ∘ β) x0 x1).(ce_t))).
-  refine (@itype_in r (yft0 (B0 r (α ∘ squish ∘ β)) r !) (fun αi => (h0 r (α ∘ squish ∘ β) x0 x1).(ce_f0) r (merge ! αi))).
-- refine (fun r β x0 x1 => _). admit.
-- simpl. (* use the cbv property for itype_out *) admit.
-- simpl. (* use the cbv property for itype_out *) admit.
-Abort.
\ No newline at end of file
diff --git a/theories/transport.v b/theories/transport.v
new file mode 100644
index 0000000..ed250b1
--- /dev/null
+++ b/theories/transport.v
@@ -0,0 +1,304 @@
+From Theories Require Import category.
+From Theories Require Import translation_fib.
+
+Set Primitive Projections.
+Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
+
+(* shifted types *)
+
+Record shifted_ty {p} : Type :=
+mkST {
+  st_t0 : @El0 (S p) (squish ⋅ Type0) ;
+  st_t1 : @El1 (S p) (squish ⋅ Type0) (squish ⋅ Type1) st_t0 ;
+}.
+
+Definition st_funct {p} {q} (α : q ≤ p) :
+  @shifted_ty p -> @shifted_ty q.
+Proof.
+unshelve refine (fun x => _).
+unshelve econstructor.
+- exact (promote α ⋅ x.(st_t0)).
+- exact (promote α ⋅ x.(st_t1)).
+Defined.
+
+Definition shifted_tyR {p} :
+ (forall q (α : q ≤ p), @shifted_ty q) -> SProp :=
+fun s => s ≡ fun q α => st_funct α (s p !).
+
+Definition shiftedType0 {p}
+  : @El0 p Type0.
+Proof.
+unshelve refine (fun q α => mkYFT _ _ _ _).
+- unshelve refine (fun r β => _).
+  exact (@shifted_ty r).
+- unshelve refine (fun r β s => _). simpl in s.
+  exact (shifted_tyR s).
+- unshelve refine (fun r β b e l le l' => _).
+  apply falso. (** TODO **)
+Defined.
+
+Definition shiftedType1 {p}
+  : @El1 p Type0 Type1 shiftedType0.
+Proof.
+refine (fun q α => _). reflexivity.
+Defined.
+
+Definition shiftedTypeStart0 {p}
+  (A0 : @El0 p shiftedType0)
+  (A1 : @El1 p shiftedType0 shiftedType1 A0) :
+  @El0 p Type0.
+Proof.
+refine (fun q α => _).
+refine ((side_0 ⋅ st_t0 (A0 q α)) q !). 
+Defined.
+
+Definition shiftedTypeStart1 {p}
+  (A0 : @El0 p shiftedType0)
+  (A1 : @El1 p shiftedType0 shiftedType1 A0) :
+  @El1 p Type0 Type1 (shiftedTypeStart0 A0 A1).
+Proof.
+refine (fun q α => _). 
+refine (J_seqs _ _ (fun X _ => yftR (fun r β => st_t0 (X r β) r side_0 )) _ (α ⋅ A0) (ssym (A1 q α))).
+refine ((side_0 ⋅ st_t1 (A0 q α)) q !).
+Defined.
+
+Definition shiftedTypeEnd0 {p}
+  (A0 : @El0 p shiftedType0)
+  (A1 : @El1 p shiftedType0 shiftedType1 A0) :
+  @El0 p Type0.
+Proof.
+refine (fun q α => _).
+refine ((side_1 ⋅ st_t0 (A0 q α)) q !). 
+Defined.
+
+Definition shiftedTypeEnd1 {p}
+  (A0 : @El0 p shiftedType0)
+  (A1 : @El1 p shiftedType0 shiftedType1 A0) :
+  @El1 p Type0 Type1 (shiftedTypeEnd0 A0 A1).
+Proof.
+refine (fun q α => _). 
+refine (J_seqs _ _ (fun X _ => yftR (fun r β => st_t0 (X r β) r side_1)) _ (α ⋅ A0) (ssym (A1 q α))).
+refine ((side_1 ⋅ st_t1 (A0 q α)) q !).
+Defined.
+
+(* a predicate over an equality is a shifted type *)
+
+Definition eqToShiftedType0 {p}
+  (A0 : @El0 p Type0)
+  (A1 : @El1 p Type0 Type1 A0)
+  (P0 : El0 (Arr0 A0 A1 Type0 Type1))
+  (P1 : El1 _ (Arr1 A0 A1 Type0 Type1) P0)
+  (a0 : El0 A0)
+  (a1 : El1 A0 A1 a0)
+  (b0 : El0 A0)
+  (b1 : El1 A0 A1 b0)
+  (e0 : El0 (eq0 A0 A1 a0 a1 b0 b1))
+  (e1 : El1 _ (eq1 A0 A1 a0 a1 b0 b1) e0) :
+  @El0 p shiftedType0.
+Proof.
+refine (fun q α => _).
+unshelve econstructor.
+- refine (fun r β => P0 r (α ∘ squish ∘ β) (β ⋅ (ce_f0 (e0 q α))) (β ⋅ ce_f1 (e0 q α))).
+- refine (@app1 (S q) _ _ Type0 Type1 (α ∘ squish ⋅ P0) (α ∘ squish ⋅ P1) (ce_f0 (e0 q α)) (ce_f1 (e0 q α))).
+Defined.
+
+Definition eqToShiftedType1 {p}
+  (A0 : @El0 p Type0)
+  (A1 : @El1 p Type0 Type1 A0)
+  (P0 : El0 (Arr0 A0 A1 Type0 Type1))
+  (P1 : El1 _ (Arr1 A0 A1 Type0 Type1) P0)
+  (a0 : El0 A0)
+  (a1 : El1 A0 A1 a0)
+  (b0 : El0 A0)
+  (b1 : El1 A0 A1 b0)
+  (e0 : El0 (eq0 A0 A1 a0 a1 b0 b1))
+  (e1 : El1 _ (eq1 A0 A1 a0 a1 b0 b1) e0) :
+  @El1 p shiftedType0 shiftedType1 (eqToShiftedType0 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1).
+Proof.
+refine (fun q α => _).
+unfold cast0 ; simpl. unfold shifted_tyR ; simpl.
+change (eqToShiftedType0 (α ⋅ A0) (α ⋅ A1) (α ⋅ P0) (α ⋅ P1) (α ⋅ a0) (α ⋅ a1) (α ⋅ b0) (α ⋅ b1) (α ⋅ e0) (α ⋅ e1) ≡ (fun r β => st_funct β (eqToShiftedType0 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1 q α))).
+pose proof (e1 q α) as He. unfold cast0 in He ; simpl in He.
+unfold cube_eqR in He.
+refine (J_seqs _ _ 
+  (fun X e => eqToShiftedType0 _ _ _ _ _ _ _ _ X 
+    (J_seqs _ _ (fun Y _ => El1 _ (eq1 (α ⋅ A0) (α ⋅ A1) (α ⋅ a0) (α ⋅ a1) (α ⋅ b0) (α ⋅ b1)) Y) 
+      (J_seqs _ (α ⋅ e0) (fun Z _ => El1 _ (eq1 (α ⋅ A0) (α ⋅ A1) (α ⋅ a0) (α ⋅ a1) (α ⋅ b0) (α ⋅ b1)) Z) (α ⋅ e1) _ He) 
+      X e) 
+    ≡ _) 
+  _ (α ⋅ e0) (ssym He)).
+reflexivity.
+Defined.
+
+(* transport boils down to a statement about shifted types *)
+
+Definition transp0 {p}
+  (A0 : @El0 p shiftedType0)
+  (A1 : @El1 p shiftedType0 shiftedType1 A0)
+  (s0 : El0 (shiftedTypeStart0 A0 A1))
+  (s1 : El1 _ (shiftedTypeStart1 A0 A1) s0)
+  : El0 (shiftedTypeEnd0 A0 A1).
+Proof.
+refine (fun q α => _).
+unfold shiftedTypeEnd0 ; simpl.
+unfold El0 in s0 ; unfold shiftedTypeStart0 in s0 ; simpl in s0. 
+change (forall q α, yft0 (st_t0 (A0 q α) q side_0) q !) in s0.
+unfold El0 in A0 ; simpl in A0.
+
+refine (J_seq _ _ (fun X _ => yft0 (X q side_1) q !) _ _ (ssym (st_t1 (A0 q α) (S q) !))).
+change (yft0 (st_t0 (A0 q α) (S q) !) q side_1).
+
+unshelve refine (let s'0 : yft0 (st_t0 (A0 q α) (S q) !) q side_0 := _ in _).
+{ pose proof (st_t1 (A0 q α) (S q) !) as H. change (yftR (st_t0 (A0 q α))) in H. unfold yftR in H.
+  refine (J_seq _ _ (fun X _ => yft0 (X q side_0) q !) _ _ H).
+  refine (s0 q α). }
+
+Admitted.
+
+Definition transp1 {p}
+  (A0 : @El0 p shiftedType0)
+  (A1 : @El1 p shiftedType0 shiftedType1 A0)
+  (s0 : El0 (shiftedTypeStart0 A0 A1))
+  (s1 : El1 _ (shiftedTypeStart1 A0 A1) s0)
+  : El1 _ (shiftedTypeEnd1 A0 A1) (transp0 A0 A1 s0 s1).
+Proof.
+Admitted.
+
+Definition transport_aux1_0 {p}
+  (A0 : @El0 p Type0)
+  (A1 : @El1 p Type0 Type1 A0)
+  (P0 : El0 (Arr0 A0 A1 Type0 Type1))
+  (P1 : El1 _ (Arr1 A0 A1 Type0 Type1) P0)
+  (a0 : El0 A0)
+  (a1 : El1 A0 A1 a0)
+  (x0 : El0 (app0 P0 a0 a1))
+  (x1 : El1 _ (app1 P1 a0 a1) x0)
+  (b0 : El0 A0)
+  (b1 : El1 A0 A1 b0)
+  (e0 : El0 (eq0 A0 A1 a0 a1 b0 b1))
+  (e1 : El1 _ (eq1 A0 A1 a0 a1 b0 b1) e0) :
+  El0 (shiftedTypeStart0 (eqToShiftedType0 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1) (eqToShiftedType1 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1)).
+Proof.
+refine (fun q α => _).
+change (yft0 (P0 q α (side_0 ⋅ ce_f0 (e0 q α)) (side_0 ⋅ ce_f1 (e0 q α))) q !).
+refine (J_seq _ (α ⋅ a0) 
+  (fun X E => yft0 (P0 q α X 
+    (J_seqs _ _ (fun Y _ => El1 (α ⋅ A0) (α ⋅ A1) Y) (α ⋅ a1) X E)) 
+    q !)
+  _ _ (ssym (ce_s (e0 q α)))).
+refine (x0 q α).
+Defined.
+
+Definition transport_aux1_1 {p}
+  (A0 : @El0 p Type0)
+  (A1 : @El1 p Type0 Type1 A0)
+  (P0 : El0 (Arr0 A0 A1 Type0 Type1))
+  (P1 : El1 _ (Arr1 A0 A1 Type0 Type1) P0)
+  (a0 : El0 A0)
+  (a1 : El1 A0 A1 a0)
+  (x0 : El0 (app0 P0 a0 a1))
+  (x1 : El1 _ (app1 P1 a0 a1) x0)
+  (b0 : El0 A0)
+  (b1 : El1 A0 A1 b0)
+  (e0 : El0 (eq0 A0 A1 a0 a1 b0 b1))
+  (e1 : El1 _ (eq1 A0 A1 a0 a1 b0 b1) e0) :
+  El1 _ (shiftedTypeStart1 (eqToShiftedType0 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1) (eqToShiftedType1 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1)) (transport_aux1_0 A0 A1 P0 P1 a0 a1 x0 x1 b0 b1 e0 e1).
+Proof.
+refine (fun q α => _). 
+unfold transport_aux1_0 ; simpl.
+unfold shiftedTypeStart0 ; unfold eqToShiftedType0 at 1 2 ; simpl.
+(* unfolding shiftedTypeStart1 unleashes hell *)
+Admitted.
+
+Definition transport_aux2_0 {p}
+  (A0 : @El0 p Type0)
+  (A1 : @El1 p Type0 Type1 A0)
+  (P0 : El0 (Arr0 A0 A1 Type0 Type1))
+  (P1 : El1 _ (Arr1 A0 A1 Type0 Type1) P0)
+  (a0 : El0 A0)
+  (a1 : El1 A0 A1 a0)
+  (b0 : El0 A0)
+  (b1 : El1 A0 A1 b0)
+  (e0 : El0 (eq0 A0 A1 a0 a1 b0 b1))
+  (e1 : El1 _ (eq1 A0 A1 a0 a1 b0 b1) e0)
+  (x0 : El0 (shiftedTypeEnd0 (eqToShiftedType0 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1) (eqToShiftedType1 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1)))
+  (x1 : El1 _ (shiftedTypeEnd1 (eqToShiftedType0 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1) (eqToShiftedType1 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1)) x0) :
+  El0 (app0 P0 b0 b1).
+Proof.
+refine (fun q α => _).
+change (yft0 (P0 q α (α ⋅ b0) (α ⋅ b1)) q !).
+refine (J_seq _ _ 
+  (fun X E => yft0 (P0 q α X 
+    (J_seqs _ _ (fun Y _ => El1 (α ⋅ A0) (α ⋅ A1) Y) 
+      (J_seqs _ (α ⋅ b0) (fun Z _ => El1 (α ⋅ A0) (α ⋅ A1) Z) (α ⋅ b1) _ (ssym (ce_t (e0 q α)))) X E)) 
+    q !)
+  _ (α ⋅ b0) (ce_t (e0 q α))).
+change (yft0 (P0 q α (side_1 ⋅ ce_f0 (e0 q α)) (side_1 ⋅ ce_f1 (e0 q α))) q !).
+refine (x0 q α).
+Defined.
+
+Definition transport_aux2_1 {p}
+  (A0 : @El0 p Type0)
+  (A1 : @El1 p Type0 Type1 A0)
+  (P0 : El0 (Arr0 A0 A1 Type0 Type1))
+  (P1 : El1 _ (Arr1 A0 A1 Type0 Type1) P0)
+  (a0 : El0 A0)
+  (a1 : El1 A0 A1 a0)
+  (b0 : El0 A0)
+  (b1 : El1 A0 A1 b0)
+  (e0 : El0 (eq0 A0 A1 a0 a1 b0 b1))
+  (e1 : El1 _ (eq1 A0 A1 a0 a1 b0 b1) e0)
+  (x0 : El0 (shiftedTypeEnd0 (eqToShiftedType0 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1) (eqToShiftedType1 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1)))
+  (x1 : El1 _ (shiftedTypeEnd1 (eqToShiftedType0 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1) (eqToShiftedType1 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1)) x0) :
+  El1 (app0 P0 b0 b1) (app1 P1 b0 b1) (transport_aux2_0 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1 x0 x1).
+Proof.
+Admitted.
+
+Definition transport0 {p}
+  (A0 : @El0 p Type0)
+  (A1 : @El1 p Type0 Type1 A0)
+  (P0 : El0 (Arr0 A0 A1 Type0 Type1))
+  (P1 : El1 _ (Arr1 A0 A1 Type0 Type1) P0)
+  (a0 : El0 A0)
+  (a1 : El1 A0 A1 a0)
+  (x0 : El0 (app0 P0 a0 a1))
+  (x1 : El1 _ (app1 P1 a0 a1) x0)
+  (b0 : El0 A0)
+  (b1 : El1 A0 A1 b0)
+  (e0 : El0 (eq0 A0 A1 a0 a1 b0 b1))
+  (e1 : El1 _ (eq1 A0 A1 a0 a1 b0 b1) e0) :
+  El0 (app0 P0 b0 b1).
+Proof.
+refine (transport_aux2_0 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1 
+  (transp0 (eqToShiftedType0 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1) (eqToShiftedType1 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1)
+    (transport_aux1_0 A0 A1 P0 P1 a0 a1 x0 x1 b0 b1 e0 e1)
+    (transport_aux1_1 A0 A1 P0 P1 a0 a1 x0 x1 b0 b1 e0 e1))
+  (transp1 (eqToShiftedType0 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1) (eqToShiftedType1 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1)
+    (transport_aux1_0 A0 A1 P0 P1 a0 a1 x0 x1 b0 b1 e0 e1)
+    (transport_aux1_1 A0 A1 P0 P1 a0 a1 x0 x1 b0 b1 e0 e1))).
+Defined.
+
+Definition transport1 {p}
+  (A0 : @El0 p Type0)
+  (A1 : @El1 p Type0 Type1 A0)
+  (P0 : El0 (Arr0 A0 A1 Type0 Type1))
+  (P1 : El1 _ (Arr1 A0 A1 Type0 Type1) P0)
+  (a0 : El0 A0)
+  (a1 : El1 A0 A1 a0)
+  (x0 : El0 (app0 P0 a0 a1))
+  (x1 : El1 _ (app1 P1 a0 a1) x0)
+  (b0 : El0 A0)
+  (b1 : El1 A0 A1 b0)
+  (e0 : El0 (eq0 A0 A1 a0 a1 b0 b1))
+  (e1 : El1 _ (eq1 A0 A1 a0 a1 b0 b1) e0) :
+  El1 (app0 P0 b0 b1) (app1 P1 b0 b1) (transport0 A0 A1 P0 P1 a0 a1 x0 x1 b0 b1 e0 e1).
+Proof.
+refine (transport_aux2_1 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1 
+  (transp0 (eqToShiftedType0 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1) (eqToShiftedType1 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1)
+    (transport_aux1_0 A0 A1 P0 P1 a0 a1 x0 x1 b0 b1 e0 e1)
+    (transport_aux1_1 A0 A1 P0 P1 a0 a1 x0 x1 b0 b1 e0 e1))
+  (transp1 (eqToShiftedType0 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1) (eqToShiftedType1 A0 A1 P0 P1 a0 a1 b0 b1 e0 e1)
+    (transport_aux1_0 A0 A1 P0 P1 a0 a1 x0 x1 b0 b1 e0 e1)
+    (transport_aux1_1 A0 A1 P0 P1 a0 a1 x0 x1 b0 b1 e0 e1))).
+Defined.
diff --git a/theories/univalence.v b/theories/univalence.v
new file mode 100644
index 0000000..319068d
--- /dev/null
+++ b/theories/univalence.v
@@ -0,0 +1,38 @@
+From Theories Require Import category.
+From Theories Require Import translation_fib.
+
+Set Primitive Projections.
+Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
+
+(* weak univalence *)
+(* for now lets just try to glue bool along bool... *)
+
+(* Definition glueType (p : ℙ) (A B : Type) : itype p Type A B.
+Proof.
+refine (J_seq _ (glueTypeAux p A B i0) (fun X _ => itype p Type X B) _ _ (glueTypeAux_i0)).
+refine (J_seq _ (glueTypeAux p A B i1) (fun X _ => itype p Type (glueTypeAux p A B i0) X) _ _ (glueTypeAux_i1)).
+refine (itype_in (glueTypeAux p A B)).
+Defined.
+
+Definition weakunivalence0 {p}
+  (A0 : @El0 p Type0)
+  (A1 : @El1 p Type0 Type1 A0)
+  (B0 : @El0 p Type0)
+  (B1 : @El1 p Type0 Type1 B0)
+  : El0 (eq0 Type0 Type1 A0 A1 B0 B1).
+Proof.
+refine (fun q α => _).
+unshelve econstructor.
+- refine (fun r β => _).
+  unshelve econstructor.
+  + refine (fun r0 β0 => _).
+    refine (itype_out (glueType r0 (yft0 (A0 r0 (α ∘ squish ∘ β ∘ β0)) r0 !) (yft0 (B0 r0 (α ∘ squish ∘ β ∘ β0)) r0 !)) (antisquish ∘ β ∘ β0)).
+  + refine (fun r0 β0 s => _) ; simpl in s.
+    admit.
+  + refine (fun r0 β0 a b c d e => _).
+    admit.
+- refine (fun r β r0 β0 => _). unfold cast0 ; simpl. reflexivity.
+- simpl.
+Admitted. *)
+