package anders

  1. Overview
  2. Docs
CCHM homotopy system type checker with strict equality

Install

Dune Dependency

Authors

Maintainers

Sources

0.12.1.tar.gz
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:

We tried to bring in as little of ourselves as possible.

HTS

Type system with two identities.

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

OCaml

Innovation. Community. Security.