Update documentation

Author: fizruk

docs/docs/examples/recId.rzk.md

@@ -13,34 +13,34 @@ We begin by introducing common HoTT definitions:
 #lang rzk-1
 
 -- A is contractible there exists x : A such that for any y : A we have x = y.
-#def iscontr (A : U) : U
+#define iscontr (A : U) : U
   := ∑ (a : A), (x : A) -> a =_{A} x
 
 -- A is a proposition if for any x, y : A we have x = y
-#def isaprop (A : U) : U
+#define isaprop (A : U) : U
   := (x : A) -> (y : A) -> x =_{A} y
 
 -- A is a set if for any x, y : A the type x =_{A} y is a proposition
-#def isaset (A : U) : U
+#define isaset (A : U) : U
   := (x : A) -> (y : A) -> isaprop (x =_{A} y)
 
 -- Non-dependent product of A and B
-#def prod (A : U) (B : U) : U
+#define prod (A : U) (B : U) : U
   := ∑ (x : A), B
 
 -- A function f : A -> B is an equivalence
 -- if there exists g : B -> A
 -- such that for all x : A we have g (f x) = x
 -- and for all y : B we have f (g y) = y
-#def isweq (A : U) (B : U) (f : A -> B) : U
+#define isweq (A : U) (B : U) (f : A -> B) : U
   := ∑ (g : B -> A), prod ((x : A) -> g (f x) =_{A} x) ((y : B) -> f (g y) =_{B} y)
 
 -- Equivalence of types A and B
-#def weq (A : U) (B : U) : U
+#define weq (A : U) (B : U) : U
   := ∑ (f : A -> B), isweq A B f
 
 -- Transport along a path
-#def transport
+#define transport
     (A : U)
     (C : A -> U)
     (x y : A)
@@ -55,7 +55,7 @@ We can now define relative function extensionality. There are several formulatio
 
 ```rzk
 -- [RS17, Axiom 4.6] Relative function extensionality.
-#def relfunext : U
+#define relfunext : U
   := (I : CUBE)
   -> (psi : I -> TOPE)
   -> (phi : psi -> TOPE)
@@ -65,7 +65,7 @@ We can now define relative function extensionality. There are several formulatio
   -> (t : psi) -> A t [ phi t |-> a t]
 
 -- [RS17, Proposition 4.8] A (weaker) formulation of function extensionality.
-#def relfunext2 : U
+#define relfunext2 : U
   := (I : CUBE)
   -> (psi : I -> TOPE)
   -> (phi : psi -> TOPE)
@@ -92,13 +92,13 @@ First, we define how to restrict an extension type to a subshape:
 #variable A : {t : I | psi t \/ phi t} -> U
 
 -- Restrict extension type to a subshape.
-#def restrict_phi
+#define restrict_phi
     (a : {t : I | phi t} -> A t)
   : {t : I | psi t /\ phi t} -> A t
   := \t -> a t
 
 -- Restrict extension type to a subshape.
-#def restrict_psi
+#define restrict_psi
     (a : {t : I | psi t} -> A t)
   : {t : I | psi t /\ phi t} -> A t
   := \t -> a t
@@ -108,13 +108,13 @@ Then, how to reformulate an `a` (or `b`) as an extension of its restriction:
 
 ```rzk
 -- Reformulate extension type as an extension of a restriction.
-#def ext-of-restrict_psi
+#define ext-of-restrict_psi
     (a : {t : I | psi t} -> A t)
   : (t : psi) -> A t [ psi t /\ phi t |-> restrict_psi a t ]
   := a  -- type is coerced automatically here
 
 -- Reformulate extension type as an extension of a restriction.
-#def ext-of-restrict_phi
+#define ext-of-restrict_phi
     (a : {t : I | phi t} -> A t)
   : (t : phi) -> A t [ psi t /\ phi t |-> restrict_phi a t ]
   := a  -- type is coerced automatically here
@@ -124,7 +124,7 @@ Now, assuming relative function extensionality, we construct a path between rest
 
 ```rzk
 -- Transform extension of an identity into an identity of restrictions.
-#def restricts-path
+#define restricts-path
     (a_psi : (t : psi) -> A t)
     (a_phi : (t : phi) -> A t)
     (e : {t : I | psi t /\ phi t} -> a_psi t = a_phi t)
@@ -144,7 +144,7 @@ Finally, we bring everything together into `recId`:
 -- A weaker version of recOR, demanding only a path between a and b:
 -- recOR(psi, phi, a, b) demands that for psi /\ phi we have a == b (definitionally)
 -- (recId psi phi a b e) demands that e is the proof that a = b (intensionally) for psi /\ phi
-#def recId uses (r) -- we declare that recId is using r on purpose
+#define recId uses (r) -- we declare that recId is using r on purpose
     (a_psi : (t : psi) -> A t)
     (a_phi : (t : phi) -> A t)
     (e : {t : I | psi t /\ phi t} -> a_psi t = a_phi t)
@@ -172,7 +172,7 @@ whenever we can show that they are equal on the intersection of shapes:
 ```rzk
 -- If two extension types are equal along two subshapes,
 -- then they are also equal along their union.
-#def id-along-border
+#define id-along-border
     (r : relfunext2)
     (I : CUBE)
     (psi : I -> TOPE)

docs/docs/reference/builtins/directed-interval.rzk.md

@@ -0,0 +1,64 @@
+# Unit type
+
+Since [:octicons-tag-24: v0.5.1][Unit support]
+
+```rzk
+#lang rzk-1
+```
+
+In the syntax, only `Unit` (the type) and `unit` (the only inhabitant) are provided. Everything else should be available from computation rules.
+More specifically, `rzk` takes the uniqueness property of the `Unit` type (see Section 1.5 of the HoTT book[^1]) as the computation rule, meaning that any (well-typed) term of type Unit reduces to unit.
+This means in particular, that induction and uniqueness can be defined very easily:
+
+```rzk
+#define ind-Unit
+  (C : Unit -> U)
+  (C-unit : C unit)
+  (x : Unit)
+  : C x
+  := C-unit
+
+#define uniq-Unit
+  (x : Unit)
+  : x = unit
+  := refl
+
+#define isProp-Unit
+  (x y : Unit)
+  : x = y
+  := refl
+```
+
+As a non-trivial example, here is a proof that `Unit` is a Segal type:
+
+```rzk
+#section isSegal-Unit
+
+#variable extext : ExtExt
+
+#define iscontr-Unit : isContr Unit
+  := (unit, \_ -> refl)
+
+#define isContr-Δ²→Unit uses (extext)
+  : isContr (Δ² -> Unit)
+  := (\_ -> unit, \k -> eq-ext-htpy extext
+    (2 * 2) Δ² (\_ -> BOT)
+    (\_ -> Unit) (\_ -> recBOT)
+    (\_ -> unit) k
+    (\_ -> refl)
+    )
+
+#define isSegal-Unit uses (extext)
+  : isSegal Unit
+  := \x y z f g -> isRetract-ofContr-isContr
+    (∑ (h : hom Unit x z), hom2 Unit x y z f g h)
+    (Δ² -> Unit)
+    (\(_, k) -> k, (\k -> (\t -> k (t, t), k), \_ -> refl))
+    isContr-Δ²→Unit
+
+#end isSegal-Unit
+```
+
+[Unit support]: https://github.com/fizruk/rzk/releases/tag/v0.5.1
+
+[^1]: The Univalent Foundations Program (2013). _Homotopy Type Theory: Univalent Foundations of Mathematics._ <https://homotopytypetheory.org/book>

docs/docs/reference/builtins/unit.rzk.md

@@ -0,0 +1,29 @@
+# Cube layer
+
+```rzk
+#lang rzk-1
+```
+
+All cubes live in `#!rzk CUBE` universe.
+
+There are two built-in cubes:
+
+1. `#!rzk 1` cube is a unit cube with a single point `#!rzk *_1`
+2. `#!rzk 2` cube is a [directed interval](../builtins/directed-interval.rzk.md) cube with points `#!rzk 0_2` and `#!rzk 1_2`
+
+It is also possible to have `#!rzk CUBE` variables and make products of cubes:
+
+1. `#!rzk I * J`  is a product of cubes `#!rzk I` and `#!rzk J`
+2. `#!rzk (t, s)` is a point in `#!rzk I * J` if `#!rzk t : I` and `#!rzk s : J`
+3. if `#!rzk ts : I * J`, then `#!rzk first ts : I` and `#!rzk second ts : J`
+
+You can usually use `#!rzk (t, s)` both as a pattern, and a construction of a pair of points:
+
+```rzk
+-- Swap point components of a point in a cube I × I
+#define swap
+    (I : CUBE)
+  : (I * I) -> I * I
+  := \(t, s) -> (s, t)
+```
+

docs/docs/reference/commands/check.rzk.md

@@ -0,0 +1,17 @@
+# Extension types
+
+
+4. Extension types \(\left\langle \prod_{t : I \mid \psi} A \vert ^{\phi} _{a} \right\rangle\) are written as `#!rzk {t : I | psi t} -> A [ phi |-> a ]`
+    - specifying `#!rzk [ phi |-> a ]` is optional, semantically defaults to `#!rzk [ BOT |-> recBOT ]` (like in RSTT);
+    - specifying `#!rzk psi` in `#!rzk {t : I | psi}` is mandatory;
+    - values of function types are \(\lambda\)-abstractions written in one of the following ways:
+        - `#!rzk \t -> <body>` — this is usually fine;
+        - `#!rzk \{t : I | psi} -> <body>` — this sometimes helps the typechecker;
+
+5. Types of functions from a shape \(\prod_{t : I \mid \psi} A\) are a specialised variant of extension types and are written `#!rzk {t : I | psi} -> A`
+    - specifying the name of the argument is mandatory; i.e. `#!rzk {I | psi} -> A` is invalid syntax!
+    - values of function types are \(\lambda\)-abstractions written in one of the following ways:
+        - `#!rzk \t -> <body>` — this is usually fine;
+        - `#!rzk \{t : I | psi} -> <body>` — this sometimes helps the typechecker;
+
+[^1]: Emily Riehl & Michael Shulman. _A type theory for synthetic ∞-categories._ Higher Structures 1(1), 147-224. 2017. <https://arxiv.org/abs/1705.07442>

docs/docs/reference/commands/compute.rzk.md

@@ -0,0 +1,72 @@
+# Introduction
+
+`rzk` is an experimental proof assistant for synthetic ∞-categories.
+`rzk-1` is an early version of the language supported by `rzk`.
+The language is based on Riehl and Shulman's «Type Theory for Synthetic ∞-categories»[^1]. In this section, we introduce syntax, discuss features and some of the current limitations of the proof assistant.
+
+Overall, a program in `rzk-1` consists of a language pragma (specifying that we use `rzk-1` and not one of the other languages[^2]) followed by a sequence of commands. For now, we will only use `#define` command.
+
+Here is a small formalisation in an MLTT subset of `rzk-1`:
+
+```rzk
+#lang rzk-1
+
+-- Flipping the arguments of a function.
+#define flip
+    (A B : U)                         -- For any types A and B
+    (C : (x : A) -> (y : B) -> U)     -- and a type family C
+    (f : (x : A) -> (y : B) -> C x y) -- given a function f : A -> B -> C
+  : (y : B) -> (x : A) -> C x y       -- we construct a function of type B -> A -> C
+  := \y x -> f x y    -- by swapping the arguments
+
+-- Flipping a function twice is the same as not doing anything
+#define flip-flip-is-id
+    (A B : U)                         -- For any types A and B
+    (C : (x : A) -> (y : B) -> U)     -- and a type family C
+    (f : (x : A) -> (y : B) -> C x y) -- given a function f : A -> B -> C
+  : f = flip B A (\y x -> C x y)
+          (flip A B C f)              -- flipping f twice is the same as f
+  := refl                             -- proof by reflexivity
+```
+
+Let us explain parts of this code:
+
+1. `#!rzk #lang rzk-1` specifies that we are in using `#!rzk rzk-1` language;
+2. `#!rzk --` starts a comment line (until the end of the line);
+3. `#!rzk #define «name» : «type» := «term»` defines a name `«name»` to be equal to `«term»`; the proof assistant will typecheck `«term»` against type `«type»`;
+4. We define two terms here — `flip` and `flip-flip-is-id`;
+5. `flip` is a function that takes 4 arguments and returns a function of two arguments.
+6. `flip-flip-is-id` is a function that takes two types, a type family, and a function `f` and returns a value of an identity type `flip ... (flip ... f) = f`, indicating that flipping a function `f` twice gets us back to `f`.
+
+Similarly to the three layers in Riehl and Shulman's type theory, `rzk-1` has 3 universes:
+
+- `CUBE` is the universe of cubes, corresponding to the cube layer;
+- `TOPE` is the universe of topes, corresponding to the tope layer;
+- `U` is the universe of types, corresponding to the types and terms layer.
+
+These are explained in the following sections.
+
+## Soundness
+
+`rzk-1` assumes "type-in-type", that is `U` has type `U`.
+This is known to make the type system unsound (due to Russell and Curry-style paradoxes), however,
+it is sometimes considered acceptable in proof assistants.
+And, since it simplifies implementation, `rzk-1` embraces this assumption, at least for now.
+
+Moreover, `rzk-1` does not prevent cubes or topes to depend on types and terms. For example, the following definition typechecks:
+
+```rzk
+#define weird
+    (A : U)
+    (I : A -> CUBE)
+    (x y : A)
+  : CUBE
+  := I x * I y
+```
+
+This likely leads to another inconsistency, but it will probably not lead to bugs in actual proofs of interest,
+so current version embraces this lax treatment of universes.
+
+[^1]: Emily Riehl & Michael Shulman. _A type theory for synthetic ∞-categories._ Higher Structures 1(1), 147-224. 2017. <https://arxiv.org/abs/1705.07442>
+
+[^2]: In version [:octicons-tag-24: v0.1.0](https://github.com/fizruk/rzk/releases/tag/v0.1.0), `rzk` has supported simply typed lambda calculus, PCF, and MLTT. However, those languages have been removed.

docs/docs/reference/commands/define-postulate.rzk.md

@@ -64,15 +64,15 @@ Topes are visualised with <span style="color: orange">**orange**</span> color:
 
 ```rzk
 -- 2-simplex
-#def Δ² : (2 * 2) -> TOPE
+#define Δ² : (2 * 2) -> TOPE
   := \(t, s) -> s <= t
 ```
 <br><br>
 Boundary of a tope:
 
 ```rzk
 -- boundary of a 2-simplex
-#def ∂Δ² : Δ² -> TOPE
+#define ∂Δ² : Δ² -> TOPE
   := \(t, s) -> s === 0_2 \/ t === 1_2 \/ s === t
 ```
 
@@ -81,14 +81,14 @@ The busiest tope diagram involves the entire 3D cube:
 
 ```rzk
 -- 3-dim cube
-#def 2³ : (2 * 2 * 2) -> TOPE
+#define 2³ : (2 * 2 * 2) -> TOPE
   := \_ -> TOP
 ```
 <br><br><br>
 
 ```rzk
 -- 3-simplex
-#def Δ³ : (2 * 2 * 2) -> TOPE
+#define Δ³ : (2 * 2 * 2) -> TOPE
   := \((t1, t2), t3) -> t3 <= t2 /\ t2 <= t1
 ```
 
@@ -100,7 +100,7 @@ Types are visualised with <span style="color: blue">**blue**</span> color. Recog
 ```rzk
 -- [RS17, Definition 5.1]
 -- The type of arrows in A from x to y.
-#def hom
+#define hom
   (A : U)   -- A type.
   (x y : A) -- Two points in A.
   : U                   -- (hom A x y) is a 1-simplex (an arrow)
@@ -113,7 +113,7 @@ Types are visualised with <span style="color: blue">**blue**</span> color. Recog
 ```rzk
 -- [RS17, Definition 5.2]
 -- the type of commutative triangles in A
-#def hom2
+#define hom2
   (A : U)           -- A type.
   (x y z : A)       -- Three points in A.
   (f : hom A x y)   -- An arrow in A from x to y.
@@ -134,7 +134,7 @@ Terms (with non-trivial labels) are visualised with <span style="color: red">**r
 We can visualise terms that fill a shape:
 
 ```rzk
-#def square
+#define square
   (A : U)
   (x y z : A)
   (f : hom A x y)
@@ -148,7 +148,7 @@ We can visualise terms that fill a shape:
 If a term is extracted as a part of a larger shape, generally, the whole shape will be shown (in gray):
 
 ```rzk
-#def face
+#define face
   (A : U)
   (x y z : A)
   (f : hom A x y)