Homotopy Type Theory

Reducing all HIT’s to 1-HIT’s

Posted on 7 May 2012 by Peter LeFanu Lumsdaine

For a while, Mike Shulman and I (and others) have wondered on and off whether it might be possible to represent all higher inductive types (i.e. with constructors of arbitrary dimension) using just 1-HIT’s (0- and 1-cell constructors only), somewhat analogously with the reduction of all standard inductive types to a few specific instances — W-types, Id-types, etc. Recently we realised that yes, it can be done, and quite prettily. It’s perhaps most easily explained in pictures: here are a couple of 2-cells, represented using just 0- and 1-cells:

And here’s a 3-cell, similarly represented:

As a topologist would say it: the (n+1)-disc is the cone on the n-sphere. To implement this logically, we first construct the spheres as a 1-HIT, using iterated suspension:

Inductive Sphere : Nat -> Type :=
  | north (n:Nat) : Sphere n
  | south (n:Nat) : Sphere n
  | longitude (n:Nat) (x:Sphere n) : Paths (north (n+1)) (south (n+1)).

Then we define (it’s a little fiddly, but do-able) a way to, given any parallel pair s, t of n-cells in a space X, represent them as a map rep s t : Sphere n -> X. (I’m suppressing a bunch of implicit arguments for the lower dimensional sources/targets.)

Now, whenever we have an (n+1)-cell constructor in a higher inductive type

HigherInductive X : Type :=
  (…earlier constructors…)
  | constr (a:A) : HigherPaths X (n+1) (constr_s a) (constr_t a)
  (…later constructors…)

we replace it by a pair of constructors

  | constr_hub (a:A) : X
  | constr_spoke (a:A) (t : Sphere n) : Paths X (rep (s a) (t a)) (constr_hub a)

Assuming functional extensionality, we can give from this a derived term constr_derived : forall (a:A), HigherPaths (n+1) (constr_s a) (constr_t a); we use this for all occurences of constr in later constructors. The universal property of the modified HIT should then be equivalent to that of the original one.

(Here for readability X was non-dependent and constr had only one argument; but the general case has no essential extra difficulties.)

What can one gain from this? Again analogously with the traditional reduction of inductive types to a few special cases, the main use I can imagine is in constructing models: once you’ve modeled 1-HIT’s, arbitrary n-HIT’s then come for free. It also could be a stepping-stone for reducing yet further to a few specific 1-HIT’s… ideas, anyone?

On a side note, while I’m here I’ll take the opportunity to briefly plug two notes I’ve put online recently but haven’t yet advertised much:

Model Structures from Higher Inductive Types, which pretty much does what it says on the tin: giving a second factorisation system on syntactic categories C_T (using mapping cylinders for the factorisations), which along with the Gambino-Garner weak factorisation system gives C_T much of the structure of a model category — all but the completeness and functoriality conditions. The weak equivalences are, as one would hope, the type-theoretic Equiv we know and love.
Univalence in Simplicial Sets, joint with Chris Kapulkin and Vladimir Voevodsky. This gives essentially the homotopy-theoretic aspects of the construction of the univalent model in simplicial sets, and these aspects only — type theory isn’t mentioned. Specifically, the main theorems are the construction of a (fibrant) universe that (weakly) classifies fibrations, and the proof that it is (in a homotopy-theoretic sense) univalent. The results are not new, but are taken from Voevodsky’s Notes on Type Systems and Oberwolfach lectures, with some proofs modified; the aim here is to give an accessible and self-contained account of the material.

(Photos above by ne*, brandsvig, and JPott, via the flickr Creative Commons pool, licensed under CC-NonCom-Attrib-NoDerivs.)

Posted in Higher Inductive Types | 5 Comments

A type theoretical Yoneda lemma

Posted on 2 May 2012 by Egbert Rijke

In this blog post I would like to approach dependendent types from a presheaf point of view. This allows us to take the theory of presheaves as an inspiration for results in homotopy type theory. The first result from this direction is a type theoretical variant of the Yoneda lemma, stating that the fiber $P(a)$ of $P$ above $a$ is equivalent to the space of all local sections at $a$ of $P$ . In analogy with natural transformations from category theory we make the following definition:

Definition. If $P$ and $Q$ are dependent types over $A$ , we define

$\mathsf{hom}(P,Q):=\prod(x:A),\ P(x)\to Q(x)$

of which the terms are called dependent transformations. We will say that a transformation $\sigma:\mathsf{hom}(P,Q)$ is an equivalence if $\sigma(x):P(x)\to Q(x)$ is an equivalence for each $x:A$ .

The case where $P$ is the dependent space over $A$ with $P(x)=x\leadsto a$ for some fixed $a$ in $A$ is of special importance. We will denote this dependent type by $\mathscr{Y}(a)$ to emphasize on the similarity of the role it plays to the Yoneda embedding of $a$ in the category of presheaves over $A$ . Indeed, we will soon be able to prove that $P(a)\simeq\mathsf{hom}(\mathscr{Y}(a),P)$ . We call a transformation from $\mathscr{Y}(a)$ to $P$ also a local section of $P$ at $a$ .

Example. If $p:a\leadsto a^\prime$ is a path in $A$ , then there is the transformation $\mathscr{Y}(p):\mathsf{hom}(\mathscr{Y}(a),\mathscr{Y}(a^\prime))$ defined by $\lambda x.\lambda q.p\bullet q$ . So $\mathscr{Y}(p)$ sends for each $x:A$ the paths $q:x\leadsto a$ to the concatenation $p\bullet q$ .

Note that we didn’t require the naturality in our definition of transformations. This is, however, something that we get for free:

Lemma. Suppose that $P$ and $Q$ are dependent types over $A$ and that $\tau:\mathsf{hom}(P,Q)$ is a transformation from $P$ to $Q$ . Then the diagram

yoneda-diagram-01.pdf

commutes up to homotopy for every path $p:x\leadsto y$ in $A$ . Here, $P(p)$ denotes transportation along $p$ with respect to the dependent type $P$ . We define $\tau(p):=Q(p)\circ\tau(x)$ when $p:x\leadsto y$ and $\tau:\mathsf{hom}(P,Q)$ .

Proof. Let $D(x,y,p)$ be the type $Q(p)\circ\sigma(x)\leadsto\sigma(y)\circ P(p)$ . Since $P(\mathrm{id}_{x})=\mathrm{id}_{P(x)}$ it follows that $D(x,x,\mathrm{id}_{x})$ is inhabited by the canonical term $d(x):=\mathrm{id}_{\sigma(x)}$ . The assertion follows now by the induction principle for identity types.
QED.

Transformations of dependent types may be composed and just as in the case with natural transformations this is done pointwise.

Lemma (Yoneda lemma for dependent types). Assuming function extensionality we have: for any dependent type $P$ over $A$ and any $a:A$ there is an equivalence

$\alpha_{P,a}:P(a)\simeq\mathsf{hom}(\mathscr{Y}(a),P)$

for each $a:A$ and $P:A\to\mathsf{Type}$ . The equivalences $\alpha_{P,a}$ are natural in the sense that the diagram

yoneda-diagram-02.pdf

commutes for every $p:a\leadsto a^\prime$ and $\tau:\mathsf{hom}(P,P^\prime)$ .

Originally, I had a two page long proof featuring some type theoretical relatives of the key ideas of the proof of the categorical Yoneda lemma, like considering $\tau_a(\mathrm{id}_a)\in P(a)$ for a presheaf $P$ on a category $\mathcal{C}$ and a natural transformation $\tau:\mathscr{Y}(a)\Rightarrow P$ . But as I wrote this blog post, the following short proof occured to me:

Proof. Note that if $x\leadsto a$ is inhabited, then $P(x)$ is equivalent to $P(a)$ . Hence we have

$\mathsf{hom}(\mathscr{Y}(a),P)$
$= \prod(x:A),\ (x\leadsto a)\to P(x)$
$\simeq \prod(x:A),\ (x\leadsto a)\to P(a)$
$\simeq \big(\sum(x:A),\ x\leadsto a\big)\to P(a)$
$\simeq P(a).$

In the last equivalence, we used that $\sum(x:A),\ x\leadsto a$ is contractible.

By looking at what each of the equivalences does, it is not so hard to see that the equivalence $\mathsf{hom}(\mathscr{Y}(a),P)\simeq P(a)$ is the map

$\lambda\tau.\tau(a,\mathrm{id}_a)$ .

Following the above commutative square from the top right first to the left and then downwards, we get for a transformation $\tau:\mathsf{hom}(\mathscr{Y}(a),P)$ , a path $p:a^\prime\leadsto a$ and a transformation $\sigma:\mathsf{hom}(P,P^\prime)$ , we get the term

$P^\prime(p)(\sigma(a)(\tau(a,\mathrm{id}_a)))$ of $P^\prime(a^\prime)$ .

Going first downwards and then to the left we get the term $\sigma(a^\prime)(\tau(a^\prime,p))$ . Induction on $p$ reveals that there is a path between the two.
QED.

Corollary. Taking $\mathscr{Y}(b)$ for $P$ we get the equivalence $\mathsf{hom}(\mathscr{Y}(a),\mathscr{Y}(b))\simeq a\leadsto b$ .

Loosely speaking, every function which takes $x:A$ and $p:x\leadsto a$ to a path from $x$ to $b$ is itself a path from $a$ to $b$ . Using the Yoneda lemma, we can derive three basic adjunctions from presheaf theory:

$\exists_f\vdash f^\ast$
$f^\ast\vdash\forall_f$
$(-)\times P\vdash (-)^P$

We will use the remainder of this post to state and prove them. Hopefully, we can distill a good notion of adjunction in the discussion thread below.

Definition. Suppose that $f:A\to B$ and let $f^\ast$ be the function from $(B\to\mathsf{Type})$ to $(A\to\mathsf{Type})$ given by substitution along $f$ , i.e. $f^\ast(Q)(a)=Q(f(a))$ for $Q:B\to A$ . We may also define the function $\exists_f:(A\to\mathsf{Type})\to(B\to\mathsf{Type})$ given by

$\exists_f(P)(b)=\sum(x:A),\ (f(x)\leadsto b)\times P(x).$

Remark. Consider the projection $\mathsf{proj_1}:B\times Y\to B$ . Then

$\exists_{\mathsf{proj_1}}(P)(b)$
$=\sum(\langle b^\prime,y\rangle:B\times Y),\ (b^\prime\leadsto b)\times P(b^\prime,y)$
$\simeq \sum(b^\prime:B)(y:Y),\ (b^\prime\leadsto b)\times P(b,y)$
$\simeq \sum(y:Y),\ P(b,y)\times \left(\sum(b^\prime :B),\ b^\prime\leadsto b\right)$
$\simeq \sum(y:Y),\ P(\langle b,y\rangle).$

We have used that the space $\sum(b^\prime:B),\ b^\prime\leadsto b$ is contractible. What this shows is that $\exists_f$ is equivalent to our original dependent sum when $f$ is a projection.

Lemma. For all $P:A\to\mathsf{Type}$ and $Q:B\to\mathsf{Type}$ we have the equivalence

$\mathsf{hom}(\exists_f(P),Q)\simeq\mathsf{hom}(P,f^\ast(Q)).$

Proof. We use the Yoneda lemma:

$\mathsf{hom}(\exists_f(P),Q)$
$= \prod(b:B),\ \left(\sum(a:A),\ (f(a)\leadsto b)\times P(a)\right)\to Q(b)$
$\simeq \prod(b:B)(a:A),\ ((f(a)\leadsto b)\times P(a))\to Q(b)$
$\simeq \prod(a:A),\ P(a)\to\prod(b:B),\ (b\leadsto f(a))\to Q(b)$
$\simeq \prod(a:A),\ P(a)\to Q(f(a))$
$= \mathsf{hom}(P,f^\ast(Q)).$
QED.

Definition. Suppose that $f:A\to B$ is a function. Define the function $\forall_f:(A\to\mathsf{Type})\to(B\to\mathsf{Type})$ given by

$\forall_f(P)(b)=\prod(a:A),\ (f(a)\leadsto b)\to P(a).$

Remark. Again, we may consider the map $\mathsf{proj_1}:B\times Y\to B$ to verify that $\forall_\mathsf{proj_1} (P)(b)\simeq\prod(y:Y),\ P(b,y)$ .

$\forall_\mathsf{proj_1}(P)(b)$
$=\prod(\langle b^\prime,y\rangle:B\times Y),\ (b^\prime\leadsto b)\to P(b^\prime,y)$
$\simeq \prod(b^\prime:B)(y:Y),\ (b^\prime\leadsto b)\to P(b,y)$
$\simeq \left(\sum(b^\prime:B),\ b^\prime\leadsto b\right)\to \prod(y:Y),\ P(b,y)$
$\simeq \prod(y:Y),\ P(b,y).$

Thus, $\forall_f$ generalizes the original dependent product construction.

Lemma. For all $P:A\to\mathsf{Type}$ and $Q:B\to\mathsf{Type}$ we have the equivalence

$\mathsf{hom}(f^\ast(Q),P)\simeq\mathsf{hom}(Q,\forall_f(P)).$

Proof. In a similar calculation as before, we derive

$\mathsf{hom}(Q,\forall_f(P))$
$=\prod(b:B),\ Q(b)\to\prod(a:A),\ (f(a)\leadsto b)\to P(a)$
$\simeq \prod(a:A)(b:B),\ Q(b)\to(f(a)\leadsto b)\to P(a)$
$\simeq \prod(a:A),\ \big(\sum(b:B),\ Q(b)\times (f(a)\leadsto b)\big)\to P(a)$
$\simeq \prod(a:A),\ \big(\sum(b:B),\ Q(f(a))\times (f(a)\leadsto b)\big)\to P(a)$
$\simeq \prod(a:A),\ Q(f(a))\times\big(\sum(b:B),\ f(a)\leadsto b)\big)\to P(a)$
$\simeq \prod(a:A),\ Q(f(a))\to P(a)$
$= \mathsf{hom}(f^\ast(Q),P)$
QED.

Definition. We may define the dependent type $Q^P$ over $A$ by

$Q^P(a)=\mathsf{hom}(\mathscr{Y}(a)\times P,Q)$

The product $P^\prime\times P$ of two dependent types over $A$ is defined pointwise as $(P^\prime\times P)(a)=P^\prime(a)\times P(a)$ .

Lemma. For any triple $P$ , $Q$ and $R$ of dependent types over $A$ there is an equivalence

$\mathsf{hom}(R,Q^P)\simeq\mathsf{hom}(R\times P,Q).$

Proof. Note that if there is a path from $y$ to $x$ , then the spaces $P(y)$ and $P(x)$ are equivalent. Thus we can make the following calculation proving the assertion:

$\mathsf{hom}(R,Q^P)$
$= \prod(x:A),\ R(x)\to\mathsf{hom}(\mathscr{Y}(x)\times P,Q)$
$= \prod(x:A),\ R(x)\to\left(\prod(y:A),\ (y\leadsto x)\times P(y)\to Q(y)\right)$
$\simeq \prod(x:A),\ R(x)\to\left(\prod (y:A),\ (y\leadsto x)\times P(x)\to Q(y)\right)$
$\simeq \prod(x:A),\ R(x)\to P(x)\to \left(\prod(y:A),\ (y\leadsto x)\to Q(y)\right)$
$\simeq \prod(x:A),\ R(x)\times P(x)\to Q(x)$
$= \mathsf{hom}(R\times P,Q).$
QED.

Remark. That the categorical definition of exponentiation doesn’t fail is no surprise. But actually we could get exponentiation easier by defining $P\to Q$ to be the dependent type over $A$ given by $(P\to Q)(a):=P(a)\to Q(a)$ . The correspondence

$\mathsf{hom}(R,P\to Q)\simeq\mathsf{hom}(R\times P,Q)$

is then immediate. By taking $R$ to be $\mathscr{Y}(a)$ and using the Yoneda lemma, we get

$(P\to Q)(a)\simeq\mathsf{hom}(\mathscr{Y}(a),P\to Q)\simeq\mathsf{hom}(\mathscr{Y}(a)\times P,Q)=Q^P(a).$

Hence the dependent types $P\to Q$ and $Q^P$ are equivalent, which comes down to the fact that we could have gotten away with the naive approach regarding exponentiation.

Posted in Foundations | 2 Comments

HoTT Updates

Posted on 29 April 2012 by Steve Awodey

Many updates have been made to the various other pages on the site: Code, Events, Links, People, References. For example, there are several new items on models of the Univalence Axiom on the References page.

Posted in Uncategorized | Leave a comment

A direct proof of Hedberg’s theorem

Posted on 30 March 2012 by Nicolai Kraus

In his article published 1998, Michael Hedberg has shown that a type with decidable equality also features the uniqueness of identity proofs property. Reading through Nils Anders Danielsson’s Agda formalization, I noticed that the statement “A has decidable equality”, i.e. $\forall x, y : A . (x \leadsto y) + (x \leadsto y \rightarrow \bot)$ , looks pretty similar to “A is contractible”, i.e. $\exists x : A . \forall y : A. x \leadsto y$ . Therefore, it is not at all surprising that a slight modification of the proof that the h-level is upwards closed works as a more direct proof for Hedberg’s theorem than the original one, but I want to share my Coq-Code anyway.

There is also a simple slight improvement of the theorem, stating that “local decidability of equality” implies “local UIP”. I use the definition of the identity type and some basic properties from Andrej Bauer’s github.

A file containing the complete Coq code (inclusive the lines that are necessary to make the code below work) can be found here.

I first prove a (local) lemma, namely that any identity proof is equal to one that can be extracted from the decidability term dec. Of course, this is already nearly the complete proof. I do that as follows: given $x$ and $y \in A$ and a proof $p$ that they are equal, I check what $\mathtt{dec}$ “thinks” about $x$ and $y$ (as well as $x$ and $x$ ). If $\mathtt{dec}$ tells me they are not equal, I get an obvious contradiction. Otherwise, $\mathtt{dec}$ precisely says that they are in the same “contractible component”, so I can just go on as in the proof that the h-level is upwards closed. With this lemma at hand, the rest is immediate.

Theorem hedberg A : dec_equ A -> uip A.
Proof.
  intros A dec x y.

  assert ( 
    lemma :
    forall proof : x ~~> y,  
    match dec x x, dec x y with
    | inl r, inl s => proof ~~> !r @ s
    | _, _ => False
    end
  ).
  Proof.
    induction proof.
    destruct (dec x x) as [pr | f].
    apply opposite_left_inverse.
    exact (f (idpath x)).

  intros p q.
  assert (p_given_by_dec := lemma p).
  assert (q_given_by_dec := lemma q).
  destruct (dec x x).
  destruct (dec x y).
  apply (p_given_by_dec @ !q_given_by_dec).
  contradiction.
  contradiction.
Qed.

Christian Sattler has pointed out to me that the above proof can actually be used to show the following slightly stronger version of Hedberg’s theorem (again, see here), stating that “local decidability implies local UIP”:

Theorem hedberg_strong A (x : A) : 
  (forall y : A, decidable (x ~~> y)) -> 
  (forall y : A, proof_irrelevant (x ~~> y)).

Posted in Code | 5 Comments

Modeling Univalence in Inverse Diagrams

Posted on 15 March 2012 by Mike Shulman

I have just posted the following preprint, which presents new set-theoretic models of univalence in categories of simplicial diagrams over inverse categories (or, more generally, diagrams over inverse categories starting from any existing model of univalence).

The univalence axiom for inverse diagrams.

For completeness, I also included a sketch of how to use a universe object to deal with coherence in the categorical interpretation of type theory, and of the meaning of various basic notions in homotopy type theory under categorical semantics in homotopy theory.

An inverse category is one that contains no infinite composable strings $\to\;\to\;\to\;\cdots$ of nonidentity arrows. An equivalent, but better, definition is that the relation “x receives a nonidentity arrow from y” on its objects is well-founded.

This means that we can use well-founded induction to construct diagrams, and morphisms between diagrams, on an inverse category. Homotopy theorists have exploited this to define the Reedy model structure for diagrams indexed on an inverse category in any model category. The Reedy cofibrations and weak equivalences are levelwise, and a diagram $A\colon I\to C$ is Reedy fibrant if for each $x\in I$ , the map from $A_x$ to the limit of the values of $A$ on “all objects below $x$ ” is a fibration. The Reedy model structure for $C=$ simplicial sets is a presentation of the $(\infty,1)$ -presheaf topos $(\infty Gpd)^I$ .

For example, if $I$ is the arrow category $(1\to 0)$ , then a diagram $A_1 \to A_0$ is Reedy fibrant if the following two conditions hold.

$A_0\to 1$ is a fibration (i.e. $A_0$ is fibrant). Here 1 is the limit of the empty diagram (there being no objects below $0\in I$ )
$A_1 \to A_0$ is a fibration. Here $A_0$ is the limit of the corresponding singleton diagram, since 0 is the unique object below $1\in I$ .

The central observation which makes this useful for modeling type theory is that

Reedy fibrant diagrams on an inverse category can be identified with certain contexts in type theory.

For instance, in a Reedy fibrant diagram on the arrow category, we have firstly a fibrant object $A_0$ , which represents a type, and then we have a fibration $A_1 \to A_0$ , which represents a type dependent on $A_0$ . Thus the whole diagram can be considered as a context of the form

$a_0\colon A_0 ,\; a_1\colon A_1(a_0)$

Similar interpretations are possible for all inverse categories (possibly involving “infinite contexts” if the category is infinite). This view of contexts as diagrams appears in Makkai’s work on “FOLDS”, and seems likely to have occurred to others as well.

Using this observation, we can inductively build a (Reedy fibrant) universe in $C^I$ out of a universe in $C$ . For instance, suppose $U$ is a fibrant object representing a universe in $C$ , and let $I$ be the arrow category $(1\to 0)$ . Then the universe we obtain in $C^I$ is the fibration $U^{(1)} \to U$ that is the universal dependent type. Regarded as a dependent type in context, this fibration is

$A\colon \mathrm{Type} \;\vdash\; (A \to \mathrm{Type}) \colon \mathrm{Type}_1$

We can then prove, essentially working only in the internal type theory of $C$ , that the objects of $C^I$ classified by this universe are closed under all the type forming operations, and moreover that this universe inherits univalence from the universe we started with in $C$ . In particular, starting with Voevodsky’s universal Kan fibration for $C=$ simplicial sets, we obtain a model of univalence in simplicial diagrams on $I$ , hence in the $(\infty,1)$ -presheaf topos $(\infty Gpd)^I$ .

Combining this with my previous idea, we should be able to get models in $(\infty,1)$ -toposes of sheaves for any topology on an inverse category. But unfortunately, inverse categories don’t seem likely to support very many interesting topologies.

So far, I haven’t been able to generalize this beyond inverse categories. The Reedy model structure exists whenever $I$ is a Reedy category, which is more general than an inverse category. But in the general case, the cofibrations are no longer levelwise, and the dependent products seem to involve equalizers, and I haven’t been able to get a handle on things. A different idea is to use diagrams on inverse categories to “bootstrap” our way up to other models, but I haven’t been able to get anything like that to work yet either.

Posted in Models, Paper, Univalence | 5 Comments

Univalence versus Extraction

Posted on 22 January 2012 by Mike Shulman

From a homotopical perspective, Coq’s built-in sort Prop is like an undecided voter, wooed by both the extensional and the intensional parties. Sometimes it leans one way, sometimes the other, at times flirting with inconsistency.

Continue reading →

Posted in Uncategorized | 18 Comments

Inductive Types in HoTT

Posted on 19 January 2012 by Steve Awodey

With all the excitement about higher inductive types (e.g. here and here), it seems worthwhile to work out the theory of conventional (lower?) inductive types in HoTT. That’s what Nicola Gambino, Kristina Sojakova and I have done, as we report in the following paper that’s just been posted on the archive:

Inductive types in Homotopy Type Theory, S. Awodey, N. Gambino, K. Sojakova, January 2012, arXiv:1201.3898v1.

The main theorem is that in HoTT, what we call the rules for homotopy W-types are equivalent to the existence of homotopy-initial algebras for polynomial functors. The required definitions are as follows:

the rules for homotopy W-types: the usual rules for W-types of formation, introduction, (dependent) elimination, and computation — but the latter is formulated as a propositional rather than a definitional equality.
a weak map of algebras $(A, s_A) \to (B, s_B)$ is a map $f:A\to B$ together with an identity proof $f\circ s_A \sim s_B\circ Pf$ , where $P$ is the polynomial functor, and a $P$ -algebra is just a map $s_A : PA\to A$ , as usual.
an algebra $(C, s_C)$ is homotopy-initial if for every algebra $(A, s_A)$ , the type of all weak maps $(C, s_C) \to (A, s_A)$ is contractible.

So in brief, the extensional situation where “W-type = initial $P$ -algebra” now becomes “homotopy W-type = homotopy-initial $P$ -algebra”. Perhaps not very surprising, once one finds the right concepts; but satisfying nonetheless.

We focus mainly on W-types because most conventional inductive types like $\mathsf{Nat}$ can be reduced to these; in fact, the possibility of such reductions is itself part of our investigation. There are some results in extensional type theory (cited in the paper) showing that many inductive types are reducible to W-types, and there is some literature (also cited) showing how such reductions can fail in the purely intensional theory. We show that in HoTT some of these reductions go through, provided both the W-types and the inductive types are understood in the appropriate “homotopical” way, with propositional computation rules. The detailed investigation of more such reductions is left as future work.

Of course, the entire development has been formalized in Coq. The files are available in the HoTT repo on GitHub:

https://github.com/HoTT/HoTT/tree/master/Coq/IT

There are also some slides (and even a video somewhere) from a talk I recently gave about this at the MAP Workshop, at the Lorentz Center in Leiden. These can be found here.

Posted in Code, Foundations, Paper | 9 Comments

Homotopy Type Theory

Reducing all HIT’s to 1-HIT’s

A type theoretical Yoneda lemma

HoTT Updates

A direct proof of Hedberg’s theorem

Modeling Univalence in Inverse Diagrams

Univalence versus Extraction

Inductive Types in HoTT

Recent Posts

Recent Comments

Categories

Archives

Blogroll

Meta

Follow “Homotopy Type Theory”