There are two tasks:
subst obey the equations specified by .
In particular, the version you wrote for one type is the same as the version wrote for the other type with coercions inserted.
Or maybe itʼs the other way, the one you wrote with explicit coercions could have all just been identities in some parallel universe.List, Tsil, Array
Weʼre not going to go in depth here (thatʼs what the rest of this article is for!), but we need to set some ground rules. We start with two Haskell definitions of type-equality:
newtype Leibniz a b = EquiConvertable (forall f. f a -> f b)
data x :~: y where
Refl :: z :~: zUnfortunately, we really need dependent types to explain HoTT, so we canʼt just stick with Haskell and I will invoke Agda as necessary.
Mostly for syntactic convenience, since it is very helpful to have a coherent syntax to talk about the concepts and types we are discussing!
Note that the main difference is the roles of : and :: are flipped in Haskell vs Agda, as type annotation versus list constructor.I personally like the Agda convention better, but of course I say that as a type theorist 😉.
The substantial programs will still be in Haskell.
Here are two equivalent definitions in Agda:
data _≡_ (x : Type) : Type -> Type where
refl : x ≡ x
data _≡_ : Type -> Type -> Type where
refl : (x : Type) -> x ≡ xNote that coercions in the sense of Haskellʼs Coercible are a fascinating topic, but largely orthogonal to what we are talking about here!
We are going to ignore them for the rest of this article.
One could think of coercions as paths that compile down to the identity, but that requires referencing some underlying (runtime) model which we donʼt talk about in HoTT.
Instead we will talk about coercing along a path.
This means that given some path (p :: x :~: y) we can write (coe p :: x -> y) for the coercion along the path p.
Our goal is to explain path induction for types, which is also referred to as Axiom for historical reasons.
Hereʼs the type of Axiom (specialized to Type):
J :
(x : Type) ->
(P : (y : Type) -> x ≡ y -> Type) ->
P x refl ->
(y : Type) ->
(p : x ≡ y) ->
P y pThis says:
(x : Type),(P : (y : Type) -> x ≡ y -> Type) ranging over possible second types (y : Type) and equality proofs x ≡ y,P x refl holds,(y : Type)(p : x ≡ y),p too: P y p.
This is just from the fact that it held at refl, which is what everyone finds surprising!Letʼs pick this apart a bit more and put it into a programming context.
P is going to be like a schema for programs varying along an abstract interface.
For example, we could take P yx is the one that our programs expect to use, while y will be the type they are given.x ≡ y.Original monomorphic program. Type family that specifies what we want to target.
There are a few related meanings of functors that we need to disentangle before we go further.
The simplest meaning: anything of kind Type -> Type.
More broadly: any type-level function.
The next simplest is our beloved Functor typeclass:
class Functor f where
fmap :: forall a b. (a -> b) -> f a -> f b
There are also related classes: Contravariant, Invariant, Phantom.
Thereʼs a fifth I want to include for completeness: EquiFunctor, which I will explain later.
Itʼs a folklore result that any standard functor (in the first sense) will satisfy one of these classes.
class Contravariant f where
contramap :: forall a b. (a -> b) -> f b -> f a
class Invariant f where
invmap :: forall a b. (a -> b) -> (b -> a) -> f a -> f b
class Phantom (f :: Type -> Type) where
coerce :: forall a b. f a -> f b
class EquiFunctor (f :: Type -> Type) where
equimap :: forall a b. Leibniz a b -> f a -> f b
Finally we have the category-theoretic notion of Functor, which goes much much further. We will not try to model the full scope of this in Haskell, but it is good to know that there is an underlying concept that unifies all of the above.
Letʼs explore.