-
Notifications
You must be signed in to change notification settings - Fork 8
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
17 changed files
with
322 additions
and
201 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Empty file.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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> |
Empty file.
Empty file.
Empty file.
Empty file.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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) | ||
``` | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.