Generalised Eckmann-Hilton argument

.github/workflows/publish.yml

@@ -1,32 +1,23 @@
 name: Publish to GitHub Pages
-
 on:
   push:
     branches:
       - master
-
 jobs:
   publish:
     runs-on: ubuntu-latest
     steps:
-      - name: Check out
-        uses: actions/checkout@v1
-
-      - name: Set-up OCaml
-        uses: ocaml/setup-ocaml@v2
+      - uses: actions/checkout@v4
+      - uses: cachix/install-nix-action@v27
         with:
-          ocaml-compiler: "5.0"
-
-      - name: Install dependencies
-        run: opam install -y dune base js_of_ocaml-compiler js_of_ocaml-ppx
-
-      - name: Build the type-checker
-        run: opam exec -- dune build
-
-      - name: Include the backend to the file
-        run: opam exec -- dune install --prefix="./_install"
+          github_access_token: ${{ secrets.GITHUB_TOKEN }}
 
+      - run: nix build ./.#catt-web
+      - id: find-web-path
+        run: |
+          path=$(nix eval ./.#catt-web.outPath --raw)
+          echo "web-path=$path" >> "$GITHUB_OUTPUT"
       - name: Deploy 🚀
         uses: JamesIves/github-pages-deploy-action@v4
         with:
-          folder: _install/share
+          folder: ${{ steps.find-web-path.outputs.web-path }}/share

.github/workflows/test.yml

@@ -1,24 +1,12 @@
 name: Check All
-
 on: [push]
-
 jobs:
-  test:
+  tests:
     runs-on: ubuntu-latest
     steps:
-      - name: Check out
-        uses: actions/checkout@v1
-
-      - name: Set-up OCaml
-        uses: ocaml/setup-ocaml@v2
-        with:
-          ocaml-compiler: "5.0"
-
-      - name: Install dependencies
-        run: opam install -y dune base js_of_ocaml-compiler js_of_ocaml-ppx
-
-      - name: Build the type-checker
-        run: opam exec -- dune build
-
-      - name: Run tests
-        run: bash ./check_all.sh
+    - uses: actions/checkout@v4
+    - uses: cachix/install-nix-action@v27
+      with:
+        github_access_token: ${{ secrets.GITHUB_TOKEN }}
+    - run: nix build
+    - run: nix flake check --all-systems

.ocamlformat

@@ -0,0 +1,2 @@
+
+profile=default

bin/catt.ml

@@ -14,22 +14,35 @@ let usage = "catt [options] [file]"
 let interactive = ref false
 let no_builtins = ref false
 let debug = ref false
+let keep_going = ref false
 
 let () =
   Printexc.record_backtrace true;
   let file_in = ref [] in
   Stdlib.Arg.parse
     [
-      "-i", Stdlib.Arg.Set interactive, "Interactive mode.";
-      "--no-builtins", Stdlib.Arg.Set no_builtins, "Prevent using built-in compositions and identities";
-      "--debug", Stdlib.Arg.Set debug, "Debug mode: stop on error and drops a menu"
+      ("-i", Stdlib.Arg.Set interactive, "Interactive mode.");
+      ( "--no-builtins",
+        Stdlib.Arg.Set no_builtins,
+        "Prevent using built-in compositions and identities" );
+      ( "--debug",
+        Stdlib.Arg.Set debug,
+        "Debug mode: stop on error and drops a menu" );
+      ( "--keep-going",
+        Stdlib.Arg.Set keep_going,
+        "Do not exit on terms that don't typecheck." );
     ]
-    (fun s -> file_in := s::!file_in)
+    (fun s -> file_in := s :: !file_in)
     usage;
-  let _ = match !file_in with
-    | [f] ->
-      Catt.Settings.use_builtins := not !no_builtins;
-      Catt.Settings.debug := !debug;
-      Catt.Command.exec ~loop_fn:Catt.Prover.loop (parse_file f)
+  let _ =
+    match !file_in with
+    | [ f ] -> (
+        Catt.Settings.use_builtins := not !no_builtins;
+        Catt.Settings.keep_going := !keep_going;
+        Catt.Settings.debug := !debug;
+        match parse_file f with
+        | Ok cmds -> Catt.Command.exec ~loop_fn:Catt.Prover.loop cmds
+        | Error () -> exit 1)
     | _ -> ()
-  in if !interactive then Catt.Prover.loop ()
+  in
+  if !interactive then Catt.Prover.loop ()

bin/dune

@@ -1,8 +1,8 @@
 (executable
+ (package catt)
  (public_name catt)
  (name catt)
- (libraries
-        ; landmarks
-        catt)
- ; (preprocess (pps landmarks-ppx --auto))
-)
+ (libraries catt))
+
+(cram
+ (deps %{bin:catt}))

catt-web.opam

@@ -0,0 +1,30 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "Browser embedded version of the catt theorem prover"
+description: "Browser embedded version of the catt theorem prover"
+maintainer: ["Thibaut Benjamin" "Chiara Sarti"]
+authors: ["Thibaut Benjamin" "Chiara Sarti"]
+license: "MIT"
+tags: ["higher-categories" "dependent-type-theory"]
+homepage: "https://github.com/thibautbenjamin/catt"
+bug-reports: "https://github.com/thibautbenjamin/catt/issues"
+depends: [
+  "ocaml"
+  "dune" {>= "3.16"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/thibautbenjamin/catt.git"

dune-project

@@ -1,24 +1,29 @@
-(lang dune 3.7)
+(lang dune 3.16)
 
 (name catt)
-
 (generate_opam_files true)
-
-(source
-  (github thibautbenjamin/catt))
-
-(authors "Thibaut Benjamin")
-
-(maintainers "Thibaut Benjamin")
-
+(source (github thibautbenjamin/catt))
+(authors "Thibaut Benjamin"
+         "Chiara Sarti")
+(maintainers "Thibaut Benjamin"
+             "Chiara Sarti")
 (license MIT)
-
 (using menhir 2.0)
+(cram enable)
 
 (package
   (name catt)
   (synopsis "An infinity-categorical coherence typechecker")
   (description "An infinity-categorical coherence typechecker")
   (depends ocaml dune)
   (tags
-    (higher-categories dependent-type-theory)))
+    (higher-categories dependent-type-theory)))
+
+(package
+  (name catt-web)
+  (synopsis "Browser embedded version of the catt theorem prover")
+  (description "Browser embedded version of the catt theorem prover")
+  (depends ocaml dune)
+  (allow_empty)
+  (tags
+    (higher-categories dependent-type-theory)))

examples/eckmann-hilton-dimensions/eh2d.catt

@@ -0,0 +1,19 @@
+coh unitl (x(f)y) : comp (id _) f -> f
+coh unit (x) : comp (id x) (id x) -> id x
+coh lsimp (x) : (unitl (id x)) -> unit x
+coh Ilsimp (x) : I (unitl (id x)) -> I (unit x)
+coh exch (x(f(a)g)y(h(b)k)z) : comp (comp _ [b]) (id (comp f k)) (comp [a] _) -> comp [a] [b]
+
+coh eh1 (x(f(a)g(b)h)y) :
+comp a b -> comp (I (unitl f))
+                 (comp (comp _ [a]) (comp (unitl g) (I (op { 1 } (unitl g)))) (comp [b] _))
+                 (op { 1 } (unitl h))
+
+let eh2 (x : *) (a : id x -> id x) (b : id x -> id x) =
+comp [Ilsimp _]
+     [comp (comp _ [comp (comp [lsimp _] [op { 1 } (Ilsimp _)]) (U (unit _))] _)
+           (exch b a)]
+     [op { 1 } (lsimp _)]
+
+let eh (x : *) (a : id x -> id x) (b : id x -> id x) =
+comp (eh1 a b) (eh2 a b) (I (op { 1 } (eh2 b a))) (I (op { 1 } (eh1 b a)))

examples/eckmann-hilton-dimensions/eh3d.catt

@@ -0,0 +1,44 @@
+coh unitl (x(f)y) : comp (id _) f -> f
+coh unit (x) : comp (id x) (id x) -> id x
+coh lsimp (x) : (unitl (id x)) -> unit x
+coh Ilsimp (x) : I (unitl (id x)) -> I (unit x)
+
+coh sandwisk (x(f)y(g(a)h)z(k)w) : comp f g k -> comp f h k
+
+let sandwich (x : *) (y : *) (f : x -> y) (g : x -> y) (a : f -> g) = comp (I (unitl f)) (comp [id (id x)] [a]) (unitl g)
+coh uunitl (x(f(a)g)y) : a -> sandwich a
+
+coh step1 (x(f(a(m)b(n)c)g)y) : comp m n ->
+  comp (uunitl a) (comp (sandwich [m]) (comp (I (uunitl b)) (op { 1 } (uunitl b))) (op { 1 } (sandwich [n]))) (op { 1 } (I (uunitl c)))
+
+coh toaster (x) : comp (I (uunitl (id (id x)))) (op { 1 } (uunitl (id (id x)))) ->
+  comp
+  (comp [Ilsimp _] (comp [id (id x)] [id (id x)]) [lsimp _])
+  (comp [I (op { 1 } (Ilsimp _))] (comp [id (id x)] [id (id x)]) [I (op { 1 } (lsimp _))])
+
+coh unfocus (x(f)y(g)z(h)w(k)u) : comp f (comp g h) k -> comp (comp f g) (comp h k)
+
+let step21 (x : *) (m : id (id x) -> id (id x)) (n : id (id x) -> id (id x)) =
+  comp (sandwich [m]) [toaster _] (op { 1 } (sandwich [n]))
+
+let step23 (x : *) (m : id (id x) -> id (id x)) (n : id (id x) -> id (id x)) =
+  comp [sandwisk [Ilsimp x] (comp [id (id x)] [[m]]) [lsimp x]]
+  [I (sandwisk [I (op { 1 } (Ilsimp x))] (comp [[n]] [id (id x)]) [I (op { 1 } (lsimp x))])]
+
+coh sandswitch (x(f)y(g(a)h(b)k)z(l)w) : comp (sandwisk f a l) (sandwisk f b l) -> sandwisk f (comp a b) l
+
+let step24 (x : *) (m : id (id x) -> id (id x)) (n : id (id x) -> id (id x)) =
+  sandswitch (I (unit x)) (comp [id (id x)] [[m]]) (comp [[n]] [id (id x)]) (unit x)
+
+coh intch20 (x(f(a(n)b)g)y(h(c(m)d)k)z) : comp (comp [a] [[m]]) (comp [[n]] [d]) -> comp [[n]] [[m]]
+
+let step25 (x : *) (m : id (id x) -> id (id x)) (n : id (id x) -> id (id x)) =
+  sandwisk (I (unit x)) [intch20 n m] (unit x)
+
+let step2inner (x : *) (m : id (id x) -> id (id x)) (n : id (id x) -> id (id x)) =
+  comp (step21 m n) (unfocus (sandwich [m]) _ _ _ ) (step23 m n) (I (unfocus (comp [Ilsimp x] _ [lsimp x]) _ _ _)) (comp _ [comp (step24 m n) (step25 m n)] _)
+
+let step2 (x : *) (m : id (id x) -> id (id x)) (n : id (id x) -> id (id x)) =
+  comp (uunitl (id (id x))) [step2inner m n] (op { 1 } (I (uunitl (id (id x)))))
+
+let final (x : *) (m : id (id x) -> id (id x)) (n : id (id x) -> id (id x)) = comp (step1 m n) (step2 m n)