# Article

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

- N: Not a

- R: Recursive

- D: Dependent

- +: Coproducts

- *: Products

# Coproducts

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.

## Unit

```
data unit = star
```

## Bool

**bool** is run-time version of the boolean logic you
may use in your general purpose applications.

```
data bool = false | true
```

## Nat

Pointed Unary System is a category nat with the terminal object
and a carrier **nat** having morphism **[zero:
1 _{nat} → 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

Maybe has representing functor M_{A}(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

**either** is a representation for sum types or disjunction.

```
data either (A B: U) = left (x: A) | right (y: B)
```

## List

The data type of **list** over a given set A can
be represented as the initial algebra (μ L_{A}, in)
of the functor L_{A}(X) = 1 + (A × X).
Denote μ L_{A} = 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

**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))
```

# Products

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

**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

**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

Runtime functor.

`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
```

## Control

```
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

```
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
```

# Logic

Basic Theories: Equality, Congruence, Categories, Setoid.

## Sigma

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

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
```

## Proto

```
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

```
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
```

## Propset

```
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)
```

## Equiv

```
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
```

## Iso

```
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
```

## Cat

```
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

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

**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))
```