The proof assistant Coq is based on a formal system called the “Predicative Calculus of (Co)Inductive Constructions” (pCiC). But before pCiC, there was the “Calculus of Constructions” (CoC), in which inductive types were not a basic object, but could be defined using impredicative polymorphism (i.e. universal quantification over a universe when defining a type existing in that same universe). In fact, higher inductive types can be defined in the same way (although this approach suffers the same drawbacks for higher inductive types as it does for ordinary ones).
As a basic example of how to define inductive types impredicatively, the natural numbers can be defined as
In other words, a natural number is a polymorphic function which assigns, to every type C equipped with a point (z, say) and an endomorphism (f, say), an element of C. One can then define
In other words, zero assigns z to every type C as above, while succ n asks what n would assign, then applies f to it. For these definitions one can then prove the non-dependent elimination rule for 
The current Coq system does not allow impredicative definitions by default, but it can be told to allow them (in the lowest universe Set) with the command-line argument -impredicative-set. Thus, in Coq with -impredicative-set, we can write the above definitions as
Definition nat : Set := forall (C:Set), C -> (C -> C) -> C. Definition zero : nat := fun C z f => z. Definition succ : nat -> nat := fun n C z f => f (n C z f).
It is perhaps not surprising that we can define higher inductive types as well using impredicative polymorphism. Here is an interval:
Definition interval : Set := forall (X : Set) (a b : X) (p : a ~~> b), X.
That is, an element of the interval is a polymorphic function which assigns, to any type X equipped with two points a, b, and a path p between them, a point of X. Note that this path type (a ~~> b is notation for paths a b) denotes the honest inductive family defined as usual, not its stand-in defined as above using impredicative polymorphism; thus this is actually a definition in CiC, the impredicative Calculus of (Co)Inductive Constructions. We could use the impredicatively defined path-type, but I doubt we could prove interval_compute_segment, below, without dependent elimination for paths.
The endpoints of the interval are easy to define.
Definition zero : interval := fun X a b p => a. Definition one : interval := fun X a b p => b.
The path between them is also straightforward, but since zero and one are now both functions, we need (dependent) functional extensionality.
Axiom funext_dep :
forall (X : Type) (P : X -> Type) (f g : forall x : X, P x),
(forall x : X, f x ~~> g x) -> f ~~> g.
Definition segment : zero ~~> one.
Proof.
apply funext_dep with (f := zero) (g := one); intro X.
apply funext_dep; intro a.
apply funext_dep; intro b.
apply funext_dep; intro p.
unfold zero, one; exact p.
Defined.
Defining the recursor is easy:
Definition interval_rec : forall (X : Set) (a b : X) (p : a ~~> b), interval -> X := fun X a b p i => i X a b p.
and it follows, as for ordinary inductive types, that the computation rules for the endpoints hold definitionally. Thus, we can prove function extensionality from eta (although it’s pretty silly to do so, since we needed to assume functional extensionality to define the interval in this way).
Axiom eta_dep_rule :
forall (A : Type) (P : A -> Type) (f : forall x : A, P x),
(fun x => f x) ~~> f.
Theorem interval_implies_funext_dep :
forall (X : Set) (P : X -> Set) (f g : forall x : X, P x),
(forall x : X, f x ~~> g x) -> f ~~> g.
Proof.
intros X P f g p.
set (mate := fun (i:interval) x => interval_rec _ _ _ (p x) i).
path_via (mate zero).
apply opposite.
path_via (fun x => f x).
apply eta_dep_rule.
path_via (mate one).
exact (map mate segment).
path_via (fun x => g x).
apply eta_dep_rule.
Defined.
The one thing missing is the computation rule for the segment:
Definition interval_compute_segment :
forall (X : Set) (a b : X) (p : a ~~> b),
map (interval_rec X a b p) segment ~~> p.
The proof is long, straightforward, and unenlightening, so I won’t post it, but I will note that I needed to use the “computation rule” for function extensionality:
Axiom funext_dep_compute :
forall (X : Type) (P : X -> Type) (f g : forall x : X, P x)
(p : forall x : X, f x ~~> g x) (x : X),
happly_dep (funext_dep X P f g p) x ~~> p x.
This is obviously a sensible thing to require. Moreover, Voevodsky proved that assuming funext_dep as above, one can find a (possibly) different inhabitant of the same type as funext_dep which does satisfy funext_dep_compute, so it is harmless to assume it.
So what does this tell us about higher inductive types? Note, first, that as for ordinary inductive types, we cannot (as far as I know) deduce the dependent version of the elimination rule in this way. And as for ordinary inductive types, the dependent elimination rules are really essential to the theory. For instance, they are necessary in order to prove that the interval is contractible, and in order to calculate 
However, I think this construction does provide additional evidence that HITs are “reasonable gadgets”. In particular, a type theorist should not think of HITs as a weird or radical thing that the homotopy theorists dreamed up. (-:
Instead, we can think about them as follows. The original CoC with impredicative Set allows the definition of inductive types, but was insufficient to prove all of their desired properties; hence first-class inductive types were introduced (and can also be added to a predicative theory). With HITs, we notice a somewhat more general class of definitions that we can make in CiC with impredicative Set (after adding first-class inductive types to CoC), but which again have desired properties that are not provable there (and are also predicative); hence we again need to make them first-class objects.
I also like this construction because identity types have no special role in the impredicative CiC. Perhaps there is a larger class of permissible definitions in CiC, which includes HITs but which can be defined without giving identity types any special role, and which we should try to make into first-class predicative objects with “dependent eliminators.”
On the other hand, I don’t know whether anyone has constructed a homotopy or groupoid model for impredicative CoC with identity types; is impredicative CoC even known to be consistent with the negation of UIP?
Homotopy Type Theory 
Thanks for posting this. Re: “For these definitions one can then prove the non-dependent elimination rule for , which satisfies its computation rule definitionally”: could you provide the proof?
The elimination rule is just evaluation. Since zero and one are defined as lambda expressions, their computation rules under evaluation are just beta-reduction. Is that sufficient, or do you want more details?
Yes, thank you. (I guess you mean zero and succ, since the remark was about nat.) What about proving the induction principles, nat_ind, …? (I guess that’s what I really wanted to ask.)
Yes, I did mean zero and succ, sorry. The induction principle is also just evaluation! If A is a type with a point z and an endomorphism f, then nat_rec should give us a function from nat to A. But given the definition of nat, an element n of nat can be evaluated at A, z, and f to produce an element of A; this is the value of nat_rec at n.
Actually it seems that induction is not derivable using the impredicative encoding. Strong elimination seems to be crucial to be able to derive such a principle.
There are people working on this problem. The key seems to be internalizing parametricity. When that is done, the strong eliminators seem to be derivable.
See for instance micro Agda. Part of the trick is figuring out how parametricity is supposed to behave computationally. And of course, I have no idea if internal parametricity is compatible with the univalence axiom.
Do you happen to have a link for that? I admit that my first instinct would be to think that a theory with internal parametricity would be inconsistent, or at least not omega-consistent…
Here is the micro Agda hackage page, and here is the publication list of its author. I think the Realizability and Parametricity in Pure Type Systems, and Proofs for Free papers are relevant. The abstract of the second says (I think) that it has a proof that parametricity is internally consistent with the logic, and a way to give it computational meaning.
This looks fascinating, thanks!
As I understand it, there’s no difficulty at all with adding parametricity axioms, since there are parametric models. The real difficulty is in coming with a version which computes.
Why is your instinct different?
I was confused I guess, I retract my remark (if I may). Some care should probably be taken in general though, as it seems that there are some choice principles that break parametricity.
I assumed he meant to ask about the non-dependent elimination rule, which is all I claimed that you could derive. Thanks for the link, though!
Here is a short derivation in Coq:
Definition Nat := forall X:Prop, X -> (X ->X) -> X.
Definition zero : Nat := fun X x f => x.
Definition succ (x : Nat) : Nat := fun Y y f => f (x Y y f).
Eval compute in succ zero.
Definition Iter : forall P : Prop, P -> (P -> P) -> Nat -> P :=
fun P z s x => x P z s.
Theorem Iter_is_elim : forall P z s, Iter P z s zero = z /\ forall n,
Iter P z s (succ n) = s (Iter P z s n).
Proof.
intros; split.
auto.
intros.
unfold Iter; simpl.
unfold succ; simpl.
reflexivity.
Qed.
Notice that only “computational” tactics (simpl, reflexivity) are used.
Thank you.
Here is a simple definition of the non-dependent eliminator (also called “iterator”) and a proof that it satisfies the required elimination rules.
Definition Iter : forall P : Prop, P -> (P -> P) -> Nat -> P :=
fun P z s x => x P z s.
Theorem Iter_is_elim : forall P z s, Iter P z s zero = z /\ forall n,
Iter P z s (succ n) = s (Iter P z s n).
Proof.
intros; split.
auto.
intros.
unfold Iter; simpl.
unfold succ; simpl.
reflexivity.
Qed.
Notice that one only uses computational rules in the proof.
How do I implement a homotopy type theory from scratch? Is the axiomatizing not figured out yet?
I’m not sure exactly what you mean. It’s not completely settled what axioms need to be added to ordinary dependent type theory to get a well-behaved homotopy theory; univalence is almost surely one, and higher inductive types are possibly another. I discussed the question of what axioms are missing in part V of my n-category Café series.
It’s also not set in stone exactly what the base “ordinary dependent type theory” should be. In practice we’ve mostly been working with Coq, which is essentially the *predicative Calculus of Constructions*.
On the other hand, most of the theoretical papers written on this have used *Martin-Löf type
theory* instead, as it’s in some ways easier to work with mathematically. For the main theory one probably wants to assume as constructors Id-/Path-types, dependent products, dependent sums, 0, 1, +, a universe, and possibly W-types. Or, more cleanly: dependent sums, inductive families, and a universe. But the papers typically assume smaller sets of constructors — just whatever’s needed for their specific work.
What exactly is the difference between pCoC and MLTT with inductive families?
Usually what is meant by pCoC is CoC with predicative Set, but impredicative Prop, which is absent from MLTT. Having impredicative propositions, even disallowing “strong eliminations” from them, is still much, much more powerful than not having it at all, as the latter can be proven to be consistent even in second order arithmetic whereas the former is of power comparable to weak set theories.
Okay, fair enough. I tend to forget about the existence of Prop, because we never use it in HoTT.
(-:So let me modify my question to: what is the difference between pCoC with Prop omitted, and MLTT with inductive families?Thanks for this post, Mike. That explained to me for the first time for a HIT should be.
It seems like related to non-free constructions, like a quotiented algebraic datatype. Basically, for you interval type you have two constructors with the extra condition that they must be equal. Similarly, one could encode the Integers with three constructors zero, succ, pred quotiented by succ . pred = pred . succ = id.
But asked the other way round: are their HITs that you cannot express as just inductive types/families under a quotient?
> Similarly, one could encode the Integers with three constructors zero, succ, pred quotiented by succ . pred = pred . succ = id.
Be careful, if you use the definition of the integers that you are suggesting, then there will be two different paths from succ (pred (succ n)) to succ n, so the type you will get will not be an h-set (it will not satisfy axiom K).
In order to get the correct type of the integers, you need to add higher coherence paths, or you can truncate it to h-level 2 in order to get an h-set.
That’s a good question! I’ll give two answers, and both of them are “yes”. (-:
Firstly, I would caution against drawing too much intuition from the translation in this post, because the main interest of HITs is in a homotopical/intensional type theory, and we don’t know whether there are any impredicative homotopical models. In particular, an HIT itself will generally not be an (h-)set; so as Guillaume points out, if you want to produce a set, you need to add some extra path-constructors forcing that.
Moreover, the meaning of “quotient” for non-hsets is somewhat slippery. So if by “quotient” you mean the ordinary notion of “quotient of a set by an equivalence relation to get another set”, then the answer to your question is certainly yes: take any HIT that is not a set. For instance, the circle. There are fancier notions of “quotient” in homotopy theory, but we don’t know how to formalize them in type theory yet, and I suspect that even with those meanings of “quotient” the answer will still be yes. That’s the first answer.
The second answer, however, is that there are even HITs that are h-sets which cannot be expressed as a quotient of an inductive type/family. You are quite right that at least within the world of h-sets, HITs are closely related to “less free” versions of the constructions that give inductive types. The catch is that an HIT allows you to define a type inductively and construct a quotient of it at the same time.
In particular, this means that with HITs, we can construct free algebras for any algebraic theory. (This is why I said “less free” rather than “non-free” above: the HIT itself is always still a free algebra; it’s the theory for which it’s an algebra that may not be free.) This is impossible with merely inductive types and quotients. In fact, even ZF is unable to construct free algebras for every algebraic theory! (ZFC can, of course.) So even in the world of h-sets, HITs are a step beyond inductive types and quotients.
Do you have an example of an algebraic theory where you really need HIT in order to construct the free algebras?
The fact that ZF cannot construct all free algebras is proven in the paper “Words, free algebras, and coequalizers” by Andreas Blass. It is based on a theorem of Gitik that (assuming the consistency of a proper class of strongly compact cardinals) it is consistent with ZF that every uncountable cardinal is singular. The counterexample is an algebraic theory with a 0-ary constant “0”, a unary operation “S”, and a
-ary operation “sup” and a list of five axioms. Blass proves that if every uncountable cardinal is singular, then an initial algebra for this theory would surject onto every ordinal number (roughly, since all limit ordinals have countable cofinality) and derives a contradiction with Hartog’s theorem.
s/their/there/
Pingback: Impredicative Encodings, Part 3 | Homotopy Type Theory