Infinity Types

Inductive Base Library

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

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

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 (μ 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

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