This library is dedicated to cubical-compatible typecheckers based on homotopy interval [0,1] and MLTT as a core. The base library is founded on top of 5 core modules: proto (composition, id, const), path (subst, trans, cong, refl, singl, sym), propset (isContr, isProp, isSet), equiv (fiber, eqiuv) and iso (lemIso, isoPath). This machinery is enough to prove univalence axiom.
(i) The library has rich recursion scheme primitives in lambek module, while very basic nat, list, stream functionality. (ii) The very basic theorems are given in pi, iso_pi, sigma, iso_sigma, retract modules. (iii) The library has category theory theorems from HoTT book in cat, fun and category modules. (iv) The library also includes some impredicative categorical encoding sketches in coproduct_set. lambek also includes inductive semantics modeled with cata/ana recursion and fixpoint adjoints in/out.
This library is best to read with HoTT book.
Base Library Modules
R ND *
- N: Not a
- R: Recursive
- D: Dependent
- +: Coproducts
- *: Products
Inductive types are the dependent version of generalized algebraic data types used in ML. With inductive and coinductive types you can model polynomial higher order functors that define generic trees and their constructors.
data unit = star
bool is run-time version of the boolean logic you may use in your general purpose applications.
data bool = false | true
Pointed Unary System is a category nat with the terminal object and a carrier nat having morphism [zero: 1nat → nat, succ: nat → nat]. The initial object of nat is called Natural Number Object and models Peano axiom set.
data nat = zero | succ (n: nat)
Maybe has representing functor MA(X) = 1 + A. It used for wrapping values with optional nothing consdtructor. In ML-style languages this type is called Option (Miranda, ML). There is an isomorphims between (fix maybe) and nat.
data maybe (A: U) = nothing | just (x: A)
either is a representation for sum types or disjunction.
data either (A B: U) = left (x: A) | right (y: B)
The data type of list over a given set A can be represented as the initial algebra (μ LA, in) of the functor LA(X) = 1 + (A × X). Denote μ LA = List(A). The constructor functions nil: 1 → List(A) and cons: A × List(A) → List(A) are defined by nil = in ◦ inl and cons = in ◦ inr, so in = [nil,cons].
data list (A: U) = nil | cons (x:A) (xs: list A) len (A: U): list A -> integer ++ (A: U): list A -> list A -> list A map (A B: U): (A -> B) -> list A -> list B filter (A: U): (A -> bool) -> list A -> list A
vector is the inductive defintion of limited length list. Through it depends on term nat it can be used on reasoning about single discrete dimention of the space, bringing very basic inductive logic. It can be used for reasoning about sqrt, as latter for any fractional exponent has correspondent number of roots inscribed in a circle on a complex surface. When vector is not dependent on nat its encoding should match with regular list.
data vector (A: U) (n: nat) = nil | cons (x: A) (xs: vector A (pred n))
When you need to inspect the addendums of inductive tree defintions you can name the agruments of the constructor, these arguments called elements of the tuple or fields of the record. In this chapter we will use record Inf syntax, we only show how record and data are equal in example of unit and prod which are primitive forms of coinductive constructions.
prod is a representation for non-dependent product types or conjunction.
data prod (A B: U) = mk (x: A) (y: B) prod (A B: U) (x: A) (y: B): (_: A) * B = (x,y)
stream is a record form of the list's cons constructor. It models the infinity list that has no terminal element.
data stream (A : U) = cons (x : A) (xs : stream A)
functor_ (F: U -> U): U = (A B: U) -> (A -> B) -> F A -> F B
Functor carried with theorem fields.
functor (F: U -> U): U = (fmap: (A B: U) -> (A -> B) -> F A -> F B) * (id: (A: U) -> (x: F A) -> Path (F A) (fmap A A (idfun A) x) x) * (compose: (A B C: U) (f: B -> C) (g: A -> B) (x: F A) -> Path (F C) (fmap A C (o A B C f g) x) * Unit
data fix (F: U -> U) = Fix (point: F (fix F)) data freeF (F: U -> U) (A B: U) = ReturnF (a: A) | BindF (f: F B) data cofreeF (F: U -> U) (A B: U) = CoBindF (a: A) (f: F B) data free (F: U -> U) (A: U) = Free (_: fix (freeF F A)) data cofree (F: U -> U) (A: U) = CoFree (_: fix (cofreeF F A)) pure (A: U) (F: U -> U): U = (return: A -> F A) * Unit applicative (F: U -> U): U = (pure_: (A: U) -> pure A F) * (functor_: functor F) * (ap: (A B: U) -> F (A -> B) -> F A -> F B) * Unit
monad (F: U -> U): U = (pure_: (A: U) -> pure A F) * (functor_: functor F) * (join: (A B: U) -> F (F A) -> F B) * Unit comonad (F: U -> U): U = (pure_: (A: U) -> pure A F) * (functor_: functor F) * (extract: (A: U) -> F A -> A) * (duplicate: (A: U) -> F A -> F (F A)) * (extend: (A B: U) -> (F A -> B) -> F A -> F B) * Unit
Basic Theories: Equality, Congruence, Categories, Setoid.
Sigma is a generalization or dependent version of Prod.
Sigma (A: U) (B: A -> U): U make (A: U) (B: A -> U) (a: A) (b: B a): Sigma A B pr1 (A: U) (B: A -> U) (x: Sigma A B): A pr2 (A: U) (B: A -> U) (x: Sigma A B): B (pr1 A B x)
Pi is a dependent version of a function f: A -> B.
Pi (A: U) (P: A -> U): U intro (A: U) (B: A -> U) (a: A) (b: B a): A -> B a app (A: U) (B: A -> U) (a: A) (f: A -> B a): B a
idfun (A: U) (a: A): A constfun (A B: U) (a: A) (b: B): A o (A B C: U) (f: B -> C) (g: A -> B): A -> C and (A B: U): U = (_: A) * B
Path (A: U) (a b: A) : U sym (A: U) (a b: A) (p: Path A a b): Path A b a refl (A: U) (a: A) : Path A a a singl (A: U) (a: A) : U trans (A B: U) (p: Path U A B) (a: A) : B subst (A: U) (P: A -> U) (a b: A) (p: Path A a b) (e: P a): P b mapOnPath (A B: U) (f: A -> B) (a b: A) (p: Path A a b): Path B (f a) (f b) composition (A: U) (a b c: A) (p: Path A a b) (q: Path A b c): Path A a c
isContr (A: U): U = (x: A) * ((y: A) -> Path A x y) isProp (A: U): U = n_grpd A Z isSet (A: U): U = n_grpd A (S Z)
fiber (A B: U) (f: A -> B) (y: B): U = (x: A) * Path B y (f x) isEquiv (A B: U) (f: A -> B): U = (y: B) -> isContr (fiber A B f y) equiv (A B: U): U = (f: A -> B) * isEquiv A B f
Square (A : U) (a0 a1 b0 b1 : A) (u : Path A a0 a1) (v : Path A b0 b1) (r0 : Path A a0 b0) (r1 : Path A a1 b1) : U lemIso (A B : U) (f : A -> B) (g : B -> A) (s : (y : B) -> Path B (f (g y)) y) (t : (x : A) -> Path A (g (f x)) x) (y : B) (x0 x1 : A) (p0 : Path B y (f x0)) (p1 : Path B y (f x1)): Path (fiber A B f y) (x0,p0) (x1,p1) isoToEquiv (A B: U) (f: A -> B) (g: B -> A) (s: (y: B) -> Path B (f (g y)) y) (t: (x: A) -> Path A (g (f x)) x): isEquiv A B f isoPath (A B: U) (f: A -> B) (g: B -> A) (s: (y: B) -> Path B (f (g y)) y) (t: (x: A) -> Path A (g (f x)) x): Path U A B
isPrecategory (C: cat): U = (id: (x: C.1) -> C.2 x x) * (c: (x y z: C.1) -> C.2 x y -> C.2 y z -> C.2 x z) * (homSet: (x y: C.1) -> isSet (C.2 x y)) * (left: (x y: C.1) -> (f: C.2 x y) -> Path (C.2 x y) (c x x y (id x) f) f) * (right: (x y: C.1) -> (f: C.2 x y) -> Path (C.2 x y) (c x y y f (id y)) f) * ( (x y z w: C.1) -> (f: C.2 x y) -> (g: C.2 y z) -> (h: C.2 z w) -> Path (C.2 x w) (c x z w (c x y z f g) h) (c x y w f (c y z w g h)))
Setoid in essence is a type with an equality. Type theory has its own equality type, which could be treated as the simplest non-trivial dependent type, however the behavior of this kind of equality is defined with additional axioms, that may be optional in minimal type theory. The neat thing about Setoid is that categorical constructions on setoids give us equality on all (Co)inductive types, which is not dependent on properties of underlying type theory.
Setoid (A: U): U = (Carrier: A) * (Equ: (a b: A) -> Path A a b) * (Refl: (x: A) -> Equ x x) * (Trans: (x₁,x₂,x₃: A) -> Equ x₁ x₂ -> Equ x₂ x₃ -> Equ x₁ x₃) * (Sym: (x₁,x₂: A) -> Equ x₁ x₂ -> Equ x₂ x₁)
Groupoid is a multidimensional generalization of Setoid type, which has equalities on equalities and operations between them. Gropoid was introduced in algebraїс topology for the purposes of homotopy theory and has the potential to replace the notion of topological space since groupoid covers all the properties of topological space from the homotopy perspective. The ultimate equality on universum of all types was shown in HoTT setting, thus type theory became successful for reasoning about homotopies. Iterating a Groupoid record over infinity number of universes that hold objects and homomorphisms gives us a concept of ∞-Groupoid.
inf_grpd (A: U): U = (carrier: A) * (eq: (a b: A) -> Path A a b) * ((a b: A) -> inf_grpd (Path A a b))