Commit something in case the universes collapse.

src/lib/Val.ml

@@ -740,14 +740,65 @@ struct
     | V info ->
       begin
         let r, r' = Star.unleash dir in
-        let xty1 = Abs.bind1 x info.ty1 in
+        let abs1 = Abs.bind1 x info.ty1 in
+
+        match D.compare (Gen.unleash info.x) (D.named x) with
+        | D.Same ->
+          let base src dest =
+            make_coe (Star.make src dest) abs1 @@
+            let phi = D.subst src x in
+            vproj (Gen.make src) (Val.act phi info.ty0) (Val.act phi info.ty1) (Val.act phi info.equiv) el
+          in
+          let base0 dest = base D.dim0 dest in
+          let base1 dest = base D.dim1 dest in
+          let fiber b = car @@ apply (cdr @@ Val.act (D.subst r' x) info.equiv) b in
+          let sys = force_abs_sys @@
+            let face_diag = AbsFace.make r r' @@ Abs.bind [Name.fresh ()] el in
+            let face0 = AbsFace.make r D.dim0 @@ Abs.bind [Name.fresh ()] (base0 r') in
+            let face1 = AbsFace.make r D.dim1 @@
+              let y = Name.fresh () in
+              Abs.bind1 y @@
+                let ty = Val.act (D.subst r' x) info.ty1 in
+                let cap = base1 r' in
+                let msys = force_abs_sys @@
+                  let face0 = AbsFace.make r' D.dim0 @@
+                    let z = Name.fresh () in
+                    Abs.bind1 z @@ ext_apply (cdr (fiber cap)) [D.named z]
+                  in
+                  let face1 = AbsFace.make r' D.dim1 @@ Abs.bind [Name.fresh ()] el in
+                  [face0; face1]
+                in
+                make_hcom (Star.make D.dim1 (D.named y)) ty cap msys
+            let el0, face_front =
+              let mode = `SPLIT_COERCION (* how should we switch this? *)
+              match mode with
+              | `SPLIT_COERCION ->
+                match Gen.make r with
+                | `Const `Dim0 -> el, face0
+                | `Const `Dim1 -> car (fiber cap), face1
+                | `Ok r_gen -> failwith "favonia is lazy; maybe candy bars will help" (* AbsFace.make r' D.dim0 @@ *)
+              | `UNIFORM_HCOM ->
+                let el0 =
+                  make_hcom (Star.make D.dim0 D.dim1) (Val.act (D.subst r' x) ty0) (base r D.dim0) @@
+                  force_abs_sys @@
+                  let face0 =
+                in
+                AbsFace.make r' D.dim0 @@
+                let z = Name.fresh () in
+                let ty = make @
+              | `UNICORN ->
+                failwith "too immortal; not suitable for mortal beings"
+          in
+          failwith "wow"
 
+        | D.Apart ->
+          failwith "wow"
+        | D.Indeterminate ->
+          failwith "impossible"
+      end
+      (*
         match Gen.make r with
         | `Const `Dim0 ->
-          let el1 =
-            rigid_coe dir xty1 @@
-            apply (car @@ Val.act (D.subst D.dim0 x) info.equiv) el
-          in
           make_vin (Gen.make r') el el1
 
         | `Const `Dim1 ->
@@ -772,8 +823,6 @@ struct
 
         | `Ok _ ->
           begin
-            match D.compare (Gen.unleash info.x) (D.named x) with
-            | D.Same ->
               failwith "This is the hard one"
 
             | _ ->
@@ -806,6 +855,7 @@ struct
               make @@ VIn {x = info.x; el0; el1}
           end
       end
+      *)
 
     | _ ->
       failwith "TODO: rigid_coe"