These notes concern the object HoTT, which has the core implementation of homotopy type theory.
The major components of homotopy type theory implemented in the object HoTT are
Inductive types, induction and recursion are in different objects as they are rather subtle. The other major way (also not in the HoTT object) of constructing non-composite types is to wrap scala types, possibly including symbolic algebra.
The core project contains code that is agnostic to how it is run. In particular this also compiles to scala-js.
We have a family of universes, but mostly use the first one denoted by Type. Given a type, we can construct symbolic objects of that type. We construct such a type A.
import provingground._, HoTT._
val A = "A" :: Type
A == Type.::("A")
We consider a symbolic object of the type A
val a = "a" :: A
Given types A and B, we have the function type A → B. An element of this is a function from A to B.
We can construct functions using λ's. Here, for the type A, we construct the identity on A using a lambda. We can then view this as a dependent function of A, giving the identity function.
In this definition, two λ's are used, with the method lmbda telling the TypecompilerType that the result is a (non-dependent) function.
val id = lambda(A)(lmbda(a)(a))
The type of the identity function is a mixture of Pi-types and function types. Which of these to use is determined by checking dependence of the type of the value on the varaible in a λ-definition.
id.typ
lmbda(a)(a).typ
lmbda(a)(a).typ.dependsOn(A)
The lambdas have the same effect at runtime. It is checked if the type of the value depends on the variable. The result is either LambdaFixed or Lambda accordingly.
val indep = lmbda(a)(a)
val dep = lambda(a)(a)
indep == dep
Note that we have alternative notation for lambdas, the maps to methods :-> and :~>.
For instance, we can define the identity using these.
assert(id == A :~> (a :-> a))
A new variable object, which has the same toString, is created in making lambdas. This is to avoid name clashes.
val l = dep.asInstanceOf[LambdaFixed[Term, Term]]
l.variable
l.variable == a
We construct Modus Ponens, as an object in Homotopy Type theory. Note that A ->: B is the function type A → B.
val B = "B" :: Type
val f = "f" :: (A ->: B)
val mp = lambda(A)(lambda(B)(lmbda(a)(lmbda(f)(f(a)))))
The type of Modus Ponens is again a mixture of Pi-types and function types.
mp.typ
We can apply modus ponens with the roles of A and B reversed. This still works because variable clashes are avoided.
val mpBA = mp(B)(A)
mpBA.typ == B ->: (B ->: A) ->: A
Lambdas do not depend on the name of the variable.
val aa = "aa" :: A
lmbda(aa)(aa) == lmbda(a)(a)
(lmbda(aa)(aa))(a) == a
Given a type family, we can construct the corresponding Pi-types and Sigma-types. We start with a formal type family, which is just a symbolic object of the appropriate type.
val Bs = "B(_ : A)" :: (A ->: Type)
In addition to the case class constructor, there is an agda/shapeless-like convenience method for constructing Pi-types. Namely, given a type expression that depends on a varaible a : A, we can construct the Pi-type correspoding to the obtained λ-expression.
Note that the !: method just claims and checks a type, and is useful (e.g. here) for documentation.
val fmly = (a !: A) ~>: (Bs(a) ->: A)
There is also a convenience method for defining Sigma types using λs.
Sgma(a !: A, Bs(a))
Sgma(a !: A, Bs(a) ->: Bs(a) ->: A)
Like functions and dependent functions, pairs and dependent pairs can be handled together. The mkPair function assignes the right type after checking dependence, choosing between pair types, pairs and dependent pairs.
val ba = "b(a)" :: Bs(a)
val b = "b" :: B
mkPair(A, B)
mkPair(a, b)
mkPair(a, b).typ
mkPair(a, ba).typ
mkPair(A, B).asInstanceOf[ProdTyp[Term, Term]]
We can also construct the plus type A plus B, which comes with two inclusion functions.
val AplusB = PlusTyp(A, B)
AplusB.incl1(a)
AplusB.incl2
In the above, a λ was used, with a variable automatically generated. These have names starting with $ to avoid collision with user defined ones.
We have an identity type associated to a type A, with reflexivity giving terms of this type.
val eqAa = IdentityTyp(A, a, a)
val ref = Refl(A, a)
ref.typ == eqAa
Finally, we have the types corresponding to True and False
Unit
Zero
Star !: Unit