The boundary of the Moebius band, and fixes for V types. (#317)

* The boundary of the Moebius band.

* Owned by the new comment syntax. LOL

* Tricks to write down boxes without using boxes.

* More code.

* A possible typo.

* Fix the fix for V.

* More definitional equality!

* New API to compare dimensions.

* More progress in moebius-boundary.red.

* Add some comment.

* Expose more stuff.

* Write the code to typecheck `box`.

* Update the comment.

* Use the new notation.

* Remove a useless lemma.

example/moebius-boundary.red

@@ -0,0 +1,109 @@
+import bool
+import s1
+import isotoequiv
+
+let not/equiv : equiv bool bool =
+  iso→equiv _ _ (not, (not, (not∘not/id/pt, not∘not/id/pt)))
+
+let not/path : path^1 type bool bool =
+  ua _ _ not/equiv
+
+let moebius-boundary/fiber : s1 → type =
+  λ [
+  | base → bool
+  | loop i → not/path i
+  ]
+
+let moebius-boundary : type = (x : s1) × moebius-boundary/fiber x
+
+let moebius-boundary→s1/loop-base (i : dim) : bool → s1 =
+  λ [ tt → loop i | ff → base ]
+
+let moebius-boundary→s1/commuting :
+  (y : bool) →
+  path _
+    (moebius-boundary→s1/loop-base 0 y)
+    (moebius-boundary→s1/loop-base 1 (coe 0 1 y in not/path))
+  =
+  λ [ tt → refl | ff → refl ]
+
+let moebius-boundary→s1/loop/filler (i j : dim) (y : not/path i) : s1 =
+  let z : bool = coe i 1 y in not/path
+  in
+  comp 1 j (moebius-boundary→s1/loop-base i z) [
+  | i=0 → moebius-boundary→s1/commuting y
+  | i=1 → refl
+  ]
+
+let moebius-boundary→s1' : (x : s1) → moebius-boundary/fiber x → s1 =
+  λ [
+  | base → moebius-boundary→s1/loop-base 0
+  | loop i → moebius-boundary→s1/loop/filler i 0
+  ]
+
+let moebius-boundary→s1 (x : moebius-boundary) : s1 =
+  moebius-boundary→s1' (x .fst) (x .snd)
+
+let s1→moebius-boundary/base : moebius-boundary =
+  (base, ff)
+
+let loop-path (b : bool) :
+  path moebius-boundary (base, b) (base, not b) =
+  λ i → (loop i , `(vin i b (not b)))
+
+let s1→moebius-boundary/loop/filler (i j : dim) : moebius-boundary =
+  comp 0 j (loop-path ff i) [i=0 → refl | i=1 → loop-path tt]
+
+let s1→moebius-boundary : s1 → moebius-boundary =
+  λ [
+  | base → s1→moebius-boundary/base
+  | loop i → s1→moebius-boundary/loop/filler i 1
+  ]
+
+opaque let s1→moebius-boundary→s1/loop :
+  [i j] s1 [
+  | ∂[i] → base
+  | j=0 → moebius-boundary→s1 (s1→moebius-boundary/loop/filler i 1)
+  | j=1 → loop i
+  ]
+  =
+  λ i j →
+    comp 0 1 (moebius-boundary→s1/loop/filler i j (loop-path ff i .snd)) [
+    | i=0 → refl
+    | i=1 k → moebius-boundary→s1/loop/filler k j (loop-path tt k .snd)
+    | j=0 k → moebius-boundary→s1 (s1→moebius-boundary/loop/filler i k)
+    | j=1 → refl
+    ]
+
+/-
+  This will force re-typechecking `box`, but why?
+-/
+let s1→moebius-boundary→s1 :
+  (x : s1) → path s1 (moebius-boundary→s1 (s1→moebius-boundary x)) x
+  =
+  λ [
+  | base → refl
+  | loop i → λ j → s1→moebius-boundary→s1/loop i j
+  ]
+
+quit
+
+-- there is an invalid fhcom in the middle?!
+-- ... (fhcom 0 1 (loop x) [x=0 <x1> base]) ...
+let test : dim → moebius-boundary =
+  λ i → s1→moebius-boundary (loop i)
+--normalize test
+
+-- there is an invalid fhcom in the middle?!
+-- ... (fhcom 0 1 (loop x) [x=0 <x1> base]) ...
+let test1 : dim → s1 =
+  λ i → moebius-boundary→s1 (s1→moebius-boundary (loop i))
+-- normalize test1
+
+/-
+let double : s1 → s1 = λ x → s1→moebius-boundary x .fst
+
+import omega1s1
+
+let test0 : path int (winding (λ i → double (loopn (pos (suc zero)) i))) (pos (suc (suc zero))) = refl
+-/

src/core/Cx.ml

@@ -201,6 +201,10 @@ let check_eq_ty cx el0 el1 =
   let (module Q) = quoter cx in
   Q.equiv_ty cx.qenv el0 el1
 
+let check_eq_dim cx r0 r1 =
+  let (module Q) = quoter cx in
+  Q.equiv_dim cx.qenv r0 r1
+
 let check_subtype cx ty0 ty1 =
   let (module Q) = quoter cx in
   Q.subtype cx.qenv ty0 ty1

src/core/Cx.mli

@@ -51,6 +51,7 @@ val quote : t -> ty:value -> value -> Tm.tm
 val quote_ty : t -> value -> Tm.tm
 val quote_dim : t -> I.t -> Tm.tm
 val check_eq_ty : t -> value -> value -> unit
+val check_eq_dim : t -> I.t -> I.t -> unit
 
 val evaluator : t -> (module Val.S)
 val quoter : t -> (module Quote.S)

src/core/Quote.ml

@@ -72,6 +72,7 @@ sig
 
   val equiv : env -> ty:value -> value -> value -> unit
   val equiv_ty : env -> value -> value -> unit
+  val equiv_dim : env -> I.t -> I.t -> unit
   val subtype : env -> value -> value -> unit
 
   val approx_restriction : env -> value -> value -> val_sys -> val_sys -> unit
@@ -767,6 +768,9 @@ struct
   let equiv_ty env ty0 ty1 =
     ignore @@ equate_ty env ty0 ty1
 
+  let equiv_dim env r0 r1 =
+    ignore @@ equate_dim env r0 r1
+
   let quote_ty env ty =
     equate_ty env ty ty
 

src/core/Quote.mli

@@ -34,6 +34,7 @@ sig
 
   val equiv : env -> ty:value -> value -> value -> unit
   val equiv_ty : env -> value -> value -> unit
+  val equiv_dim : env -> I.t -> I.t -> unit
   val subtype : env -> value -> value -> unit
 
   val approx_restriction : env -> value -> value -> val_sys -> val_sys -> unit

src/core/Typing.ml

@@ -17,6 +17,8 @@ type cofibration = (I.t * I.t) list
 type error =
   | ExpectedDimension of cx * Tm.tm
   | ExpectedTick of cx * Tm.tm
+  | UnequalDimensions of I.t * I.t
+  | TypeError of value * (cx * Tm.tm)
 
 exception E of error
 
@@ -35,6 +37,14 @@ struct
       Format.fprintf fmt
         "Expected tick, but got %a."
         (Tm.pp (Cx.ppenv cx)) tm
+    | UnequalDimensions (i0, i1) ->
+      Format.fprintf fmt
+        "Unequal dimensions: %a /= %a"
+        I.pp i0 I.pp i1
+    | TypeError (ty, (cx, tm)) ->
+      Format.fprintf fmt
+        "Unable to show %a is of type %a."
+        (Tm.pp (Cx.ppenv cx)) tm D.pp_value ty
 
 end
 
@@ -329,6 +339,9 @@ let rec check_ cx ty rst tm =
         failwith "v/vin dimension mismatch"
     end;
 
+  | [], D.FHCom tyinfo, T.Box tinfo ->
+    check_box cx tyinfo.dir tyinfo.cap tyinfo.sys tinfo.r tinfo.r' tinfo.cap tinfo.sys
+
   | [], _, T.Up tm ->
     let ty' = infer cx tm in
     Cx.check_subtype cx ty' ty
@@ -346,8 +359,7 @@ let rec check_ cx ty rst tm =
     check_boundary cx ty rst v
 
   | [], _, _ ->
-    (* Format.eprintf "Failed to check term %a@." (Tm.pp (CxUtil.ppenv cx)) tm; *)
-    failwith "Type error"
+    raise @@ E (TypeError (ty, (cx, tm)))
 
 and check cx ty tm =
   check_ cx ty [] tm
@@ -390,6 +402,83 @@ and cofibration_of_sys : type a. cx -> (Tm.tm, a) Tm.system -> cofibration =
     in
     List.map face sys
 
+and check_box cx tydir tycap tysys tr tr' tcap tsys =
+  let raiseError () =
+    let ty = D.make @@ D.FHCom {dir=tydir; cap=tycap; sys=tysys} in
+    let tm = Tm.make @@ Tm.Box {r=tr; r'=tr'; cap=tcap; sys=tsys} in
+    raise @@ E (TypeError (ty, (cx, tm)))
+  in
+  let tyr, tyr' = Dir.unleash tydir in
+  let r = check_eval_dim cx tr in
+  Cx.check_eq_dim cx tyr r;
+  let r' = check_eval_dim cx tr' in
+  Cx.check_eq_dim cx tyr' r';
+  let cap = check_eval cx tycap tcap in
+  let rec go tysys tsys acc =
+    match tsys with
+    | [] -> if tysys = [] then () else raiseError ()
+    | (tri0, tri1, otm) :: tsys ->
+      let ri0 = check_eval_dim cx tri0 in
+      let ri1 = check_eval_dim cx tri1 in
+      match tysys, I.compare ri0 ri1, otm with
+      | _, `Apart, _ ->
+        (* skipping false boundaries without consuming `tysys`. *)
+        go tysys tsys acc
+
+      | _, `Same, _ ->
+        raiseError ()
+
+      | (Face.Indet (p, tyabs) :: tysys), `Indet, Some tm ->
+        let tyri0, tyri1 = Eq.unleash p in
+        Cx.check_eq_dim cx tyri0 ri0;
+        Cx.check_eq_dim cx tyri1 ri1;
+
+        begin
+          try
+            let cx, phi = Cx.restrict cx ri0 ri1 in
+            let (module V) = Cx.evaluator cx in
+            let tyabs = Lazy.force tyabs in
+            let ty_r' = D.Abs.inst1 tyabs tyr' in
+            let el = check_eval cx ty_r' tm in
+            Cx.check_eq cx ~ty:(D.Value.act phi tycap)
+              (D.Value.act phi cap)
+              (V.make_coe (Dir.act phi (Dir.swap tydir)) tyabs el);
+
+            (* Check face-face adjacency conditions *)
+            go_adj cx ty_r' acc (ri0, ri1, el);
+            go tysys tsys @@ (ri0, ri1, el) :: acc
+          with
+        | I.Inconsistent -> raiseError ()
+        end
+      | _ ->
+        raiseError ()
+
+  and go_adj cx ty faces (ri0, ri1, el) : unit =
+    match faces with
+    | [] -> ()
+    | (ri'0, ri'1, el') :: faces ->
+      (* Invariant: cx, ty and el should already be restricted by ri0=ri1,
+       * and el' should already be restricted by ri'0=ri'1. *)
+      begin
+        try
+          let phi' =
+            let ri0 = I.act (I.equate ri'0 ri'1) ri0 in
+            let ri1 = I.act (I.equate ri'0 ri'1) ri1 in
+            I.equate ri0 ri1
+          in
+          let cx, phi =
+            let ri'0 = I.act (I.equate ri0 ri1) ri'0 in
+            let ri'1 = I.act (I.equate ri0 ri1) ri'1 in
+            Cx.restrict cx ri'0 ri'1
+          in
+          Cx.check_eq cx ~ty:(D.Value.act phi ty) (D.Value.act phi el) (D.Value.act phi' el')
+        with
+        | I.Inconsistent -> ()
+      end;
+      go_adj cx ty faces (ri0, ri1, el)
+  in
+  go tysys tsys []
+
 and check_fhcom cx ty tr tr' tcap tsys =
   let r = check_eval_dim cx tr in
   check_dim cx tr';
@@ -425,8 +514,6 @@ and check_boundary_face cx ty face el =
     | I.Inconsistent ->
       ()
 
-
-
 and check_tm_sys cx ty sys =
   let rec go sys acc =
     match sys with

src/core/Val.ml

@@ -829,7 +829,8 @@ struct
               in
               let face1 =
                 AbsFace.make phi (I.act phi r') `Dim1 @@ fun phi ->
-                Abs.make1 @@ fun _ -> Value.act phi el in
+                Abs.make1 @@ fun _ -> Value.act phi el
+              in
               [face0; face1]
             in
             make_hcom (Dir.make `Dim1 (`Atom y)) ty cap msys
@@ -904,7 +905,7 @@ struct
             AbsFace.make I.idn r' `Dim0 @@ fun phi ->
             Abs.make1 @@ fun w -> ext_apply (cdr (fixer_fiber phi)) [`Atom w]
           in
-          let el1 = make_hcom (Dir.make `Dim1 `Dim0) info.ty1 (base I.idn r r') @@
+          let el1 = make_hcom (Dir.make `Dim1 r') info.ty1 (base I.idn r r') @@
             force_abs_sys [face0; face1; face_diag; face_front]
           in
           make_vin I.idn r' el0 el1
@@ -920,7 +921,6 @@ struct
               let funcr = Value.act phi @@ car info.equiv in
               rigid_vproj info.x ~func:funcr ~el
             in
-            let mode = `INCONSISTENCY_REMOVAL in
             let sys =
               let face0 =
                 AbsFace.gen_const I.idn info.x `Dim0 @@ fun phi ->
@@ -932,10 +932,7 @@ struct
                 Abs.bind1 x @@
                 make_coe (Dir.make (I.act phi r) (`Atom x)) (Abs.act phi abs1) (Value.act phi el)
               in
-              match mode with
-              | `OLD_SCHOOL -> Option.filter_map force_abs_face [face0; face1]
-              | `INCONSISTENCY_REMOVAL -> Option.filter_map force_abs_face [face0]
-              | `UNICORN -> raise @@ E InternalMortalityError
+              Option.filter_map force_abs_face [face0; face1]
             in
             rigid_com dir abs1 cap sys
           in
@@ -1107,11 +1104,6 @@ struct
           apply (car (Value.act phi equiv)) @@
           hcom phi (`Atom y) ty0 (* ty0 is already under `phi0` *)
         in
-        let face1 =
-          AbsFace.gen_const I.idn x `Dim1 @@ fun phi ->
-          Abs.make1 @@ fun y ->
-          hcom phi (`Atom y) (Value.act phi ty1)
-        in
         let func = car equiv in
         let el1_cap = rigid_vproj x ~func ~el:cap in
         let el1_sys =
@@ -1121,7 +1113,7 @@ struct
             let yi, el = Abs.unleash absi in
             Abs.bind yi @@ vproj phi (I.act phi @@ `Atom x) ~func:(fun phi -> Value.act phi func) ~el
           in
-          Option.filter_map force_abs_face [face0; face1] @ List.map face sys
+          Option.filter_map force_abs_face [face0] @ List.map face sys
         in
         rigid_hcom dir ty1 el1_cap el1_sys
       in
@@ -1173,7 +1165,7 @@ struct
               | `Proj abs -> abs
               | `Ok faces ->
                 Abs.make1 @@ fun y ->
-                make_hcom (Dir.make (I.act phi r) (`Atom y)) (Value.act phi ty) (Value.act phi cap) (`Ok (faces @ rest))
+                make_hcom (Dir.make (I.act phi r) (`Atom y)) (Value.act phi ty) (Value.act phi cap) (`Ok (faces @ rest0))
           in
           let face0 = face (`Dim0, `Dim1) in
           let face1 = face (`Dim1, `Dim0) in

src/core/ValSig.ml

@@ -44,6 +44,8 @@ sig
   val restriction_force : value -> value
 
   val rigid_vproj : atom -> func:value -> el:value -> value
+  val rigid_coe : dir -> abs -> value -> value
+  val make_coe : dir Dir.m -> abs -> value -> value
 
   val inst_clo : clo -> value -> value
   val inst_nclo : nclo -> env_el list -> value