Provingground - HoTT

These notes concern the object HoTT, which has the core implementation of homotopy type theory. Implementation details are (rather, will be) in the scaladocs.

The major components of homotopy type theory implemented in the object HoTT are

  • Terms, types and Universes.
  • Function and dependent function types.
  • Ī»s.
  • Pairs and Dependent pairs.
  • Disjoint union types.
  • Types 0 and 1 and an object in the latter.
  • Identity types

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.

In [1]:
import $ivy.`io.github.siddhartha-gadgil::provingground-core-jvm:0.1.0`
Out[1]:
import $ivy.$

Universes, Symbolic types

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.

In [2]:
import provingground._
repl.pprinter.bind(translation.FansiShow.fansiPrint)
import HoTT._
val A ="A" :: Type
A == Type.::("A")
Out[2]:
import provingground._

import HoTT._

A: Typ[Term] = A
res1_4: Boolean = true

We consider a symbolic object of the type A

In [3]:
val a ="a" :: A
Out[3]:
a: Term = a

Function types, lambdas, Identity

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.

In [4]:
val id = lambda(A)(lmbda(a)(a))
Out[4]:
id: FuncLike[Typ[Term], Func[Term, Term]] = (A : š’° ) ā†¦ (a : 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.

In [5]:
id.typ
lmbda(a)(a).typ
lmbda(a)(a).typ.dependsOn(A)
Out[5]:
res4_0: Typ[FuncLike[Typ[Term], Func[Term, Term]]] = āˆ(A : š’° ){ (A ā†’ A) }
res4_1: Typ[Func[Term, Term]] = (A ā†’ A)
res4_2: Boolean = true

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.

In [6]:
val indep = lmbda(a)(a)
val dep = lambda(a)(a)
indep == dep
Out[6]:
indep: Func[Term, Term] = (a : A) ā†¦ a
dep: FuncLike[Term, Term] = (a : A) ā†¦ a
res5_2: Boolean = true

Hygiene for λs

A new variable object, which has the same toString, is created in making lambdas. This is to avoid name clashes.

In [7]:
val l = dep.asInstanceOf[LambdaFixed[Term, Term]]
l.variable
l.variable == a
Out[7]:
l: LambdaFixed[Term, Term] = (a : A) ā†¦ a
res6_1: Term = a
res6_2: Boolean = false

Modus Ponens

We construct Modus Ponens, as an object in Homotopy Type theory. Note that A ->: B is the function type A ā†’ B.

In [8]:
val B = "B" :: Type

val f = "f" :: (A ->: B)

val mp = lambda(A)(lambda(B)(lmbda(a)(lmbda(f)(f(a)))))
Out[8]:
B: Typ[Term] = B
f: Func[Term, Term] = f
mp: FuncLike[Typ[Term], FuncLike[Typ[Term], Func[Term, Func[Func[Term, Term], Term]]]] = (A : š’° ) ā†¦ (B : š’° ) ā†¦ (a : A) ā†¦ (f : (A ā†’ B)) ā†¦ f(a)

The type of Modus Ponens is again a mixture of Pi-types and function types.

In [9]:
mp.typ
Out[9]:
res8: Typ[FuncLike[Typ[Term], FuncLike[Typ[Term], Func[Term, Func[Func[Term, Term], Term]]]]] = āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ ((A ā†’ B) ā†’ B)) } }

We can apply modus ponens with the roles of A and B reversed. This still works because variable clashes are avoided.

In [10]:
val mpBA = mp(B)(A)
mpBA.typ == B ->: (B ->: A) ->: A
Out[10]:
mpBA: Func[Term, Func[Func[Term, Term], Term]] = (a : B) ā†¦ (f : (B ā†’ A)) ā†¦ f(a)
res9_1: Boolean = true

Equality of λs

Lambdas do not depend on the name of the variable.

In [11]:
val aa = "aa" :: A
lmbda(aa)(aa) == lmbda(a)(a)
(lmbda(aa)(aa))(a) == a
Out[11]:
aa: Term = aa
res10_1: Boolean = true
res10_2: Boolean = true

Dependent types

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.

In [12]:
val Bs = "B(_ : A)" :: (A ->: Type)
Out[12]:
Bs: Func[Term, Typ[Term]] = B(_ : A)

Pi-Types

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.

In [13]:
val fmly = (a !: A) ~>: (Bs(a) ->: A)
Out[13]:
fmly: GenFuncTyp[Term, Func[Term, Term]] = āˆ(a : A){ (B(_ : A)(a) ā†’ A) }

Sigma-types

There is also a convenience method for defining Sigma types using Ī»s.

In [14]:
Sgma(a !: A, Bs(a))
Out[14]:
res13: SigmaTyp[Term, Term] = āˆ‘(a : { B(_ : A)(a) }
In [15]:
Sgma(a !: A, Bs(a) ->: Bs(a) ->: A)
Out[15]:
res14: SigmaTyp[Term, Func[Term, Func[Term, Term]]] = āˆ‘(a : { (B(_ : A)(a) ā†’ (B(_ : A)(a) ā†’ A)) }

Pair types

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.

In [16]:
val ba = "b(a)" :: Bs(a)
val b = "b" :: B
mkPair(A, B)
mkPair(a, b)
mkPair(a, b).typ
mkPair(a, ba).typ
Out[16]:
ba: Term = b(a)
b: Term = b
res15_2: AbsPair[Term, Term] = AƗB
res15_3: AbsPair[Term, Term] = (a , b)
res15_4: Typ[U] = AƗB
res15_5: Typ[U] = āˆ‘(a : { B(_ : A)(a) }
In [17]:
mkPair(A, B).asInstanceOf[ProdTyp[Term, Term]]
Out[17]:
res16: ProdTyp[Term, Term] = AƗB

Plus types

We can also construct the plus type A plus B, which comes with two inclusion functions.

In [18]:
val AplusB = PlusTyp(A, B)
Out[18]:
AplusB: PlusTyp[Term, Term] = A + B
In [19]:
AplusB.incl1(a)
Out[19]:
res18: PlusTyp.FirstIncl[Term, Term] = FirstIncl(PlusTyp(A,B),a)
In [20]:
AplusB.incl2
Out[20]:
res19: Func[Term, PlusTyp.ScndIncl[Term, Term]] = ($gr : B) ā†¦ ScndIncl(PlusTyp(A,B),$gr)

In the above, a Ī» was used, with a variable automatically generated. These have names starting with $ to avoid collision with user defined ones.

Identity type

We have an identity type associated to a type A, with reflexivity giving terms of this type.

In [21]:
val eqAa = IdentityTyp(A, a, a)
val ref = Refl(A, a)
Out[21]:
eqAa: IdentityTyp[Term] = a = a
ref: Refl[Term] = Refl(A,a)
In [22]:
ref.typ == eqAa
Out[22]:
res21: Boolean = true

The Unit and the Nought

Finally, we have the types corresponding to True and False

In [23]:
Unit
Zero
Star !: Unit
Out[23]:
res22_0: Unit.type = Unit
res22_1: Zero.type = Zero
res22_2: Term = Star