🌌 Make the Universe Strict

src/core/Conversion.ml

@@ -106,8 +106,12 @@ let rec equate_tp (tp0 : D.tp) (tp1 : D.tp) =
   | D.Circle, D.Circle
   | D.Univ, D.Univ ->
     ret ()
-  | D.ElStable code0, D.ElStable code1 ->
-    equate_stable_code D.Univ code0 code1
+  | D.ElStable code0, _ ->
+    let* tp0 = lift_cmp @@ Sem.unfold_el code0 in
+    equate_tp tp0 tp1
+  | _, D.ElStable code1 ->
+    let* tp1 = lift_cmp @@ Sem.unfold_el code1 in
+    equate_tp tp0 tp1
   | D.ElCut cut0, D.ElCut cut1 ->
     equate_cut cut0 cut1
   | D.ElUnstable (`HCom (r0, s0, phi0, bdy0)), D.ElUnstable (`HCom (r1, s1, phi1, bdy1)) ->
@@ -232,10 +236,8 @@ and equate_con tp con0 con1 =
     let* out1 = lift_cmp @@ do_sub_out con1 in
     equate_con tp out0 out1
   | D.ElStable code, _, _ ->
-    let* out0 = lift_cmp @@ do_el_out con0 in
-    let* out1 = lift_cmp @@ do_el_out con1 in
     let* tp = lift_cmp @@ unfold_el code in
-    equate_con tp out0 out1
+    equate_con tp con0 con1
   | _, D.Zero, D.Zero ->
     ret ()
   | _, D.Suc con0, D.Suc con1 ->
@@ -260,7 +262,7 @@ and equate_con tp con0 con1 =
       Splice.con bdy @@ fun bdy ->
       Splice.term @@
       TB.lam @@ fun i -> TB.lam @@ fun prf ->
-      TB.el_in @@ TB.ap bdy [i; prf]
+      TB.ap bdy [i; prf]
     in
     let* bdy0' = fix_body bdy0 in
     let* bdy1' = fix_body bdy1 in
@@ -271,7 +273,7 @@ and equate_con tp con0 con1 =
       Splice.con bdy @@ fun bdy ->
       Splice.term @@
       TB.lam @@ fun i -> TB.lam @@ fun prf ->
-      TB.el_in @@ TB.ap bdy [i; prf]
+      TB.ap bdy [i; prf]
     in
     let* bdy0' = fix_body bdy0 in
     let* bdy1' = fix_body bdy1 in
@@ -401,8 +403,6 @@ and equate_frm k0 k1 =
       TB.el @@ TB.ap mot [TB.loop x]
     in
     equate_con loop_tp loop_case0 loop_case1
-  | D.KElOut, D.KElOut ->
-    ret ()
   | _ ->
     conv_err @@ ExpectedFrmEq (k0, k1)
 

src/core/Domain.ml

@@ -33,8 +33,6 @@ struct
   let snd = Lam (`Anon, Clo (S.Snd (S.Var 0), {tpenv = Emp; conenv = Emp}))
 
   let proj lbl = Lam (`Anon, Clo (S.Proj (S.Var 0, lbl), {tpenv = Emp; conenv = Emp}))
-  let el_out = Lam (`Anon, Clo (S.ElOut (S.Var 0), {tpenv = Emp; conenv = Emp}))
-
   let tm_abort = Split []
   let tp_abort = TpSplit []
 
@@ -106,7 +104,6 @@ struct
     | KProj lbl -> Format.fprintf fmt "proj[%a]" Ident.pp_user lbl
     | KNatElim _ -> Format.fprintf fmt "<nat-elim>"
     | KCircleElim _ -> Format.fprintf fmt "<circle-elim>"
-    | KElOut -> Uuseg_string.pp_utf_8 fmt "⭝ₑₗ"
 
   and pp_cof : cof Pp.printer =
     fun fmt cof ->
@@ -174,8 +171,6 @@ struct
       Format.fprintf fmt "dim0"
     | Dim1 ->
       Format.fprintf fmt "dim1"
-    | ElIn con ->
-      Format.fprintf fmt "el/in[%a]" pp_con con
     | StableCode `Nat ->
       Format.fprintf fmt "nat/code"
     | StableCode `Circle ->

src/core/Domain.mli

@@ -23,7 +23,6 @@ module Make : functor (Symbol : Symbol.S) -> sig
   val fst : con
   val snd : con
   val proj : Ident.user -> con
-  val el_out : con
 
   val tm_abort : con
   val tp_abort : tp

src/core/DomainData.ml

@@ -70,10 +70,7 @@ struct
     | Pair of con * con
     | Struct of (Ident.user * con) list
     | SubIn of con
-
-    | ElIn of con
-    (** The introduction form for the extension of a {i stable} type code only (see {!constructor:ElStable} and {!constructor:ElUnstable}). *)
-
+
     | Dim0
     | Dim1
     | DimProbe of DimProbe.t
@@ -139,10 +136,6 @@ struct
     | KNatElim of con * con * con
     | KCircleElim of con * con * con
 
-    | KElOut
-    (** The elimination form for the extension of a {i stable} type code only (see {!constructor:ElStable}). *)
-
-
   (** An {i unstable} frame is a {i dimension substitution-unstable} elimination form with a hole in place of its principal argument. *)
   and unstable_frm =
     | KHCom of dim * dim * cof * con

src/core/Quote.ml

@@ -115,12 +115,8 @@ let rec quote_con (tp : D.tp) con =
     S.SubIn tout
 
   | D.ElStable code, _ ->
-    let+ tout =
-      let* unfolded = lift_cmp @@ unfold_el code in
-      let* out = lift_cmp @@ do_el_out con in
-      quote_con unfolded out
-    in
-    S.ElIn tout
+    let* unfolded = lift_cmp @@ unfold_el code in
+    quote_con unfolded con
 
   | _, D.Zero ->
     ret S.Zero
@@ -160,10 +156,9 @@ let rec quote_con (tp : D.tp) con =
       Splice.con bdy @@ fun bdy ->
       Splice.term @@
       TB.lam @@ fun i -> TB.lam @@ fun prf ->
-      TB.el_in @@ TB.ap bdy [i; prf]
+      TB.ap bdy [i; prf]
     in
-    let+ tm = quote_hcom (D.StableCode `Nat) r s phi bdy' in
-    S.ElOut tm
+    quote_hcom (D.StableCode `Nat) r s phi bdy'
 
   | _univ, D.UnstableCode (`V (r, pcode, code, pequiv)) ->
     let+ tr, t_pcode, tcode, t_pequiv = quote_v_data r pcode code pequiv in
@@ -176,21 +171,19 @@ let rec quote_con (tp : D.tp) con =
       Splice.con bdy @@ fun bdy ->
       Splice.term @@
       TB.lam @@ fun i -> TB.lam @@ fun prf ->
-      TB.el_in @@ TB.ap bdy [i; prf]
+      TB.ap bdy [i; prf]
     in
-    let+ tm = quote_hcom (D.StableCode `Univ) r s phi bdy' in
-    S.ElOut tm
+    quote_hcom (D.StableCode `Univ) r s phi bdy'
 
   | D.Circle, D.FHCom (`Circle, r, s, phi, bdy) ->
     let* bdy' =
       lift_cmp @@ splice_tm @@
       Splice.con bdy @@ fun bdy ->
       Splice.term @@
       TB.lam @@ fun i -> TB.lam @@ fun prf ->
-      TB.el_in @@ TB.ap bdy [i; prf]
+      TB.ap bdy [i; prf]
     in
-    let+ tm = quote_hcom (D.StableCode `Circle) r s phi bdy' in
-    S.ElOut tm
+    quote_hcom (D.StableCode `Circle) r s phi bdy'
 
   | D.ElUnstable (`HCom (r,s,phi,bdy)), _ ->
     let+ tr = quote_dim r
@@ -650,5 +643,3 @@ and quote_frm tm =
   | D.KAp (tp, con) ->
     let+ targ = quote_con tp con in
     S.Ap (tm, targ)
-  | D.KElOut ->
-    ret @@ S.ElOut tm

src/core/Refiner.ml

@@ -653,7 +653,7 @@ struct
               Splice.con vpatch @@ fun patch ->
               Splice.term @@ TB.lams (field_names :> Ident.t list) @@ fun args -> TB.code_ext 0 (TB.ap field_tp @@ ListUtil.zip_with (@@) elim_conns args) TB.top @@ TB.lam @@ fun _ -> TB.ap patch args
             in
-            (ext_code, fun arg -> TB.sub_out @@ TB.el_out arg)
+            (ext_code, TB.sub_out)
           | None ->
             let+ code =
               RM.lift_cmp @@
@@ -697,7 +697,7 @@ struct
       RM.lift_cmp @@
       Sem.splice_tm @@
       Splice.con vtm @@ fun tm ->
-      Splice.term @@ TB.lams (sign_names :> Ident.t list) @@ fun args -> TB.el_out @@ TB.ap tm [TB.el_in @@ TB.struct_ @@ List.combine sign_names args]
+      Splice.term @@ TB.lams (sign_names :> Ident.t list) @@ fun args -> TB.ap tm [TB.struct_ @@ List.combine sign_names args]
     in
     let+ qfib = RM.quote_con fib_tp fib in
     S.CodeSignature (qsign @ [`User ["fib"], qfib])
@@ -745,7 +745,7 @@ struct
         TB.ap bdry [TB.prf]
       in
       let+ ttm = RM.lift_qu @@ Qu.quote_con tp tm in
-      S.ElIn (S.SubIn ttm)
+      S.SubIn ttm
     | tp -> RM.expected_connective `ElExt tp
 
   let code_v (tac_dim : T.Chk.tac) (tac_pcode: T.Chk.tac) (tac_code : T.Chk.tac) (tac_pequiv : T.Chk.tac) : T.Chk.tac =
@@ -936,14 +936,14 @@ struct
   let intro tac =
     T.Chk.brule ~name:"El.intro" @@ fun (tp, phi, clo) ->
     let* unfolded = dest_el tp in
-    let+ tm = T.Chk.brun tac (unfolded, phi, D.un_lam @@ D.compose D.el_out @@ D.Lam (`Anon, clo)) in
-    S.ElIn tm
+    T.Chk.brun tac (unfolded, phi, D.un_lam @@ D.Lam (`Anon, clo))
 
   let elim tac =
     T.Syn.rule ~name:"El.elim" @@
     let* tm, tp = T.Syn.run tac in
     let+ unfolded = dest_el tp in
-    S.ElOut tm, unfolded
+    tm, unfolded
+
 end
 
 
@@ -1214,7 +1214,7 @@ struct
 
   let assert_nat =
     function
-    | D.Nat -> RM.ret ()
+    | D.Nat | D.ElStable `Nat -> RM.ret ()
     | tp -> RM.expected_connective `Nat tp
 
   let rec int_to_term =
@@ -1282,7 +1282,7 @@ struct
 
   let assert_circle =
     function
-    | D.Circle -> RM.ret ()
+    | D.Circle | D.ElStable `Circle -> RM.ret ()
     | tp -> RM.expected_connective `Circle tp
 
   let base =