package anders
Install
Dune Dependency
Authors
Maintainers
Sources
md5=10bc0c65d9aabab5ceeba6245bf1e0c3
sha512=6bbab7ff3efcf1de5b6423f7e5b153e76f37cf3bf8513383162a73b9377771f0520fe1f1fe4cf53652b3a60fe42cef9d6054fa4ae888edd65696accbd0bac124
README.md.html
Anders
Homotopy Type System with Strict Equality.
Features
Homepage: https://groupoid.space/homotopy
Fibrant MLTT-style ΠΣ primitives with strict equality in 500 LOC
Cofibrant CHM-style I primitives with pretypes hierarchy Vₙ in 500 LOC
Generalized Transport and Homogeneous Composition core Kan operations
Partial Elements
Cubical Subtypes
Strict Equality on pretypes
Parser in 80 LOC
Lexer in 80 LOC
UTF-8 support including universe levels
Lean syntax for ΠΣ
Poor man's records as Σ with named accessors to telescope variables
1D syntax with top-level declarations
Groupoid Infinity CCHM base library: https://groupoid.space/math
Best suited for academic papers and fast type checking
Setup
$ opam install anders
Samples
You can find some examples in the share
directory of the Anders package.
def comp-Path⁻¹ (A : U) (a b : A) (p : Path A a b) :
Path (Path A a a) (comp-Path A a b a p (<i> p @ -i)) (<_> a) :=
<k j> hcomp A (∂ j ∨ k) (λ (i : I), [(j = 0) → a, (j = 1) → p @ -i ∧ -k, (k = 1) → a]) (p @ j ∧ -k)
def kan (A : U) (a b c d : A) (p : Path A a c) (q : Path A b d) (r : Path A a b) : Path A c d :=
<i> hcomp A (∂ i) (λ (j : I), [(i = 0) → p @ j, (i = 1) → q @ j]) (r @ i)
def comp (A : I → U) (r : I) (u : Π (i : I), Partial (A i) r) (u₀ : (A 0)[r ↦ u 0]) : A 1 :=
hcomp (A 1) r (λ (i : I), [(r = 1) → transp (<j>A (i ∨ j)) i (u i 1=1)]) (transp(<i> A i) 0 (ouc u₀))
def ghcomp (A : U) (r : I) (u : I → Partial A r) (u₀ : A[r ↦ u 0]) : A :=
hcomp A (∂ r) (λ (j : I), [(r = 1) → u j 1=1, (r = 0) → ouc u₀]) (ouc u₀)
$ anders check library/path.anders
CCHM
Anders was built by strictly following these publications:
CTT: a constructive interpretation of the univalence axiom [Cohen, Coquand, Huber, Mörtberg]
On Higher Inductive Types in Cubical Type Theory [Coquand, Huber, Mörtberg]
Canonicity and homotopy canonicity for cubical type theory [Coquand, Huber, Sattler]
Cubical Synthetic Homotopy Theory [Mörtberg, Pujet]
Unifying Cubical Models of Univalent Type Theory [Cavallo, Mörtberg, Swan]
Cubical Agda: A Dependently Typed PL with Univalence and HITs [Vezzosi, Mörtberg, Abel]
Gluing for type theory [Kaposi, Huber, Sattler]
Cubical Methods in HoTT/UF [Mörtberg]
We tried to bring in as little of ourselves as possible.
HTS
Type system with two identities.
A simple type system with two identity types [Voevodsky]
Two-level type theory and applications [Annenkov, Capriotti, Kraus, Sattler]
Syntax for two-level type theory [Bonacina, Ahrens]
Benchmarks
$ time make
real 0m1.254s
user 0m0.981s
sys 0m0.183s
$ time for i in library/* ; do ./anders.native check $i ; done
real 0m0.257s
user 0m0.231s
sys 0m0.028s
Acknowledgements
Univalent People
Authors
Siegmentation Fault
5HT