Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf sheaves simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorTodd_Trimble
   • CommentTimeJan 15th 2012
   • (edited Jan 15th 2012)
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexI hate to ask a stupid question, but the statement of [[function extensionality]] is confusing to me. Does it have something to do with the potential discrepancy between the exponential of an identity type $(P Y)^X$, and the identity type of an exponential $P(Y^X)$? In other words, one can exhibit a map $P(Y^X) \to P(Y)^X$, so that a term $p: [f = g]$ gives rise to a map $X \to P(Y)$, i.e., a family of paths in $Y$ continuously varying over $X$. But there's no obvious way (to me) of getting from $P(Y)^X$ to $P(Y^X)$ without some further assumption. Is that the idea? Is the idea even stronger: that these two objects should be equivalent? Somewhat bothersome to me is the notation > happly f g p: forall x: X, f x == g x because I think of "forall" as an operator applied to propositions or (-1)-truncated objects. That only adds to my confusion.

   I hate to ask a stupid question, but the statement of function extensionality is confusing to me. Does it have something to do with the potential discrepancy between the exponential of an identity type $(P Y)^X$, and the identity type of an exponential $P(Y^X)$?

   In other words, one can exhibit a map $P(Y^X) \to P(Y)^X$, so that a term $p: [f = g]$ gives rise to a map $X \to P(Y)$, i.e., a family of paths in $Y$ continuously varying over $X$. But there’s no obvious way (to me) of getting from $P(Y)^X$ to $P(Y^X)$ without some further assumption. Is that the idea? Is the idea even stronger: that these two objects should be equivalent?

   Somewhat bothersome to me is the notation

   happly f g p: forall x: X, f x == g x

   because I think of “forall” as an operator applied to propositions or (-1)-truncated objects. That only adds to my confusion.

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeJan 15th 2012
   • PermaLink
   Author: Urs
   Format: MarkdownItexMike will give the expert reply, but I'll try to reply anyway. > I think of "forall" as an operator applied to propositions or (-1)-truncated objects. The definition directly extends, though to all types. Didn't you and me edit the diagram at _[[universal quantifier]]_ that shows, conversely, how the general definition restricts to $(-1)$-types? This is, anyway, what is meant here: forall x : X, P x is interpreted as the type of internal sections of the dependent type $P$.

   Mike will give the expert reply, but I’ll try to reply anyway.

   I think of “forall” as an operator applied to propositions or (-1)-truncated objects.

   The definition directly extends, though to all types. Didn’t you and me edit the diagram at universal quantifier that shows, conversely, how the general definition restricts to $(-1)$-types?

   This is, anyway, what is meant here:

   forall x : X, P x
   

   is interpreted as the type of internal sections of the dependent type $P$.

3. • CommentRowNumber3.
   • CommentAuthorTodd_Trimble
   • CommentTimeJan 15th 2012
   • (edited Jan 15th 2012)
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexOh, right, of course. So a term of that type would simply be a section of (in this case) $[f x = g x] \to X$, which in turn would amount to a map $X \to P(Y)$ which projects down to the pair $\langle f, g \rangle \colon X \to Y \times Y$. Which gives a term $1 \to P(Y)^X$ which projects to the term $1 \to (Y \times Y)^X$ that names the pair $\langle f, g \rangle$, as I was suggesting in #1. We are trying to lift that term through the map $P(Y^X) \to P(Y)^X$, if I'm not mistaken.

   Oh, right, of course. So a term of that type would simply be a section of (in this case) $[f x = g x] \to X$, which in turn would amount to a map $X \to P(Y)$ which projects down to the pair $\langle f, g \rangle \colon X \to Y \times Y$. Which gives a term $1 \to P(Y)^X$ which projects to the term $1 \to (Y \times Y)^X$ that names the pair $\langle f, g \rangle$, as I was suggesting in #1. We are trying to lift that term through the map $P(Y^X) \to P(Y)^X$, if I’m not mistaken.

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeJan 15th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI think your understanding is right, Todd. Function extensionality is roughly "if the values of two functions are equal at every point, then the two functions are equal as functions". There are several different versions of this. I call "naive" function extensionality the assertion that there is some (arbitrary) map $P(Y)^X \to P(Y^X)$ over $Y^X\times Y^X$; this implements the quoted statement and is sufficient in extensional type theory—but in homotopy type theory we want to say something stronger, that (as you said) those types should be equivalent. I call that "strong" function extensionality. In fact, it turns out that from naive function extensionality (for *dependent* functions, i.e. spaces of sections) we can *prove* strong function extensionality! I think this observation is originally due to Voevodsky; Peter Lumsdaine's HoTT blog post linked at [[function extensionality]] discusses the proof (though it may not be so readable for the non-initiate (-: ).

   I think your understanding is right, Todd. Function extensionality is roughly “if the values of two functions are equal at every point, then the two functions are equal as functions”. There are several different versions of this. I call “naive” function extensionality the assertion that there is some (arbitrary) map $P(Y)^X \to P(Y^X)$ over $Y^X\times Y^X$; this implements the quoted statement and is sufficient in extensional type theory—but in homotopy type theory we want to say something stronger, that (as you said) those types should be equivalent. I call that “strong” function extensionality.

   In fact, it turns out that from naive function extensionality (for dependent functions, i.e. spaces of sections) we can prove strong function extensionality! I think this observation is originally due to Voevodsky; Peter Lumsdaine’s HoTT blog post linked at function extensionality discusses the proof (though it may not be so readable for the non-initiate (-: ).

5. • CommentRowNumber5.
   • CommentAuthorTodd_Trimble
   • CommentTimeJan 15th 2012
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexThanks, Mike! I find this formulation much easier to follow. Can we arrange an algebra map $P(Y)^X \to P(Y^X)$, where the algebra structure on $P(Y)^X$ is the expected $(Y \to P(Y))^X$ (in the slice over $(Y \times Y)^X$)? Follow-up: if there is an interval object $I$, according to your (and Peter's?) higher inductive type definition, then can we say $P(Y)$ and $Y^I$ are equivalent? I didn't quite see that in your blog post, but it would explain function extensionality pretty naturally. :-)

   Thanks, Mike! I find this formulation much easier to follow. Can we arrange an algebra map $P(Y)^X \to P(Y^X)$, where the algebra structure on $P(Y)^X$ is the expected $(Y \to P(Y))^X$ (in the slice over $(Y \times Y)^X$)?

   Follow-up: if there is an interval object $I$, according to your (and Peter’s?) higher inductive type definition, then can we say $P(Y)$ and $Y^I$ are equivalent? I didn’t quite see that in your blog post, but it would explain function extensionality pretty naturally. :-)

6. • CommentRowNumber6.
   • CommentAuthorTobyBartels
   • CommentTimeJan 15th 2012
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexI expect that the use of `forall` here derives from its use in Coq, which I've never really liked. One can always read it as a dependent product.

   I expect that the use of forall here derives from its use in Coq, which I’ve never really liked. One can always read it as a dependent product.

7. • CommentRowNumber7.
   • CommentAuthorTodd_Trimble
   • CommentTimeJan 15th 2012
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexI have tried to incorporate the above discussion into [[function extensionality]]. This should however be checked by an expert.

   I have tried to incorporate the above discussion into function extensionality. This should however be checked by an expert.

8. • CommentRowNumber8.
   • CommentAuthorUrs
   • CommentTimeJan 15th 2012
   • (edited Jan 15th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexI have added to your addition some hyperlinks, and mentioned, with link, the dependent product explicitly.

   I have added to your addition some hyperlinks, and mentioned, with link, the dependent product explicitly.

9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeJan 15th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexTodd, what do you mean by "algebra map"? Algebra for what? And yes, $P(Y)$ and $Y^I$ are equivalent... but only because both of them are equivalent to $Y$. Unfortunately, we can't in the type theory make $Y^I \to Y\times Y$ into a fibration (dependent type), so we can't show directly that it has the same universal property as $P(Y)$. But that intuition is certainly what motivated the proof that an interval implies funext. @Toby: I didn't like Coq's use of `forall` for dependent products at first either. But it's grown on me. After all, what is an element of the dependent product $\Pi_{a\colon A} B(a)$? It consists, of *for all* $a\colon A$, an element of $B(a)$. In everyday language, we do use "for all" and "for each" to refer to stuff and structure, not just properties.

   Todd, what do you mean by “algebra map”? Algebra for what?

   And yes, $P(Y)$ and $Y^I$ are equivalent… but only because both of them are equivalent to $Y$. Unfortunately, we can’t in the type theory make $Y^I \to Y\times Y$ into a fibration (dependent type), so we can’t show directly that it has the same universal property as $P(Y)$. But that intuition is certainly what motivated the proof that an interval implies funext.

   @Toby: I didn’t like Coq’s use of forall for dependent products at first either. But it’s grown on me. After all, what is an element of the dependent product $\Pi_{a\colon A} B(a)$? It consists, of for all $a\colon A$, an element of $B(a)$. In everyday language, we do use “for all” and “for each” to refer to stuff and structure, not just properties.

10. • CommentRowNumber10.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 16th 2012
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexMike, I meant algebra in the sense that $P(Y^X)$ is an "initial algebra" (inductive type) for the endofunctor constant at $Y^X \to Y^X \times Y^X$. Have I made a mistake somewhere? And yes, I did mean to ask whether $P(Y)$ and $Y^I$ were equivalent as fibrations, but you've answered that; thanks.

    Mike, I meant algebra in the sense that $P(Y^X)$ is an “initial algebra” (inductive type) for the endofunctor constant at $Y^X \to Y^X \times Y^X$. Have I made a mistake somewhere?

    And yes, I did mean to ask whether $P(Y)$ and $Y^I$ were equivalent as fibrations, but you’ve answered that; thanks.

11. • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeJan 16th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItex> I meant algebra in the sense that $P(Y^X)$ is an "initial algebra" (inductive type) Ah, I see. In that case, I think it depends on what you mean by "arrange" — since function extensionality is, after all, something that we need to *add* to the type theory. We can assert that there exists such an algebra map; I think this is one of the variants of function extensionality considered in Richard Garner's paper. The map that we get from naive or strong funext, however, is not a strict algebra map (though it is a weak algebra map, i.e. up to homotopy).

    I meant algebra in the sense that $P(Y^X)$ is an “initial algebra” (inductive type)

    Ah, I see. In that case, I think it depends on what you mean by “arrange” — since function extensionality is, after all, something that we need to add to the type theory. We can assert that there exists such an algebra map; I think this is one of the variants of function extensionality considered in Richard Garner’s paper. The map that we get from naive or strong funext, however, is not a strict algebra map (though it is a weak algebra map, i.e. up to homotopy).

12. • CommentRowNumber12.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 16th 2012
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexMike, thanks very much for the information. "Arrange" meant starting from a weaker form of function extensionality (e.g., mere existence of a map $P(Y)^X \to P(Y^X)$ in the slice over $Y^X \times Y^X$, as you were saying), is there ("can we arrange") such a map with even nicer properties like being an algebra map? The idea I had in mind at the time of writing is that if the specified algebra map $P(Y^X) \to P(Y)^X$ has a section which is an algebra map, then those two algebra maps form an equivalence between $P(Y^X)$ and $P(Y)^X$. Does the edit I made at [[function extensionality]] look alright to you?

    Mike, thanks very much for the information. “Arrange” meant starting from a weaker form of function extensionality (e.g., mere existence of a map $P(Y)^X \to P(Y^X)$ in the slice over $Y^X \times Y^X$, as you were saying), is there (“can we arrange”) such a map with even nicer properties like being an algebra map? The idea I had in mind at the time of writing is that if the specified algebra map $P(Y^X) \to P(Y)^X$ has a section which is an algebra map, then those two algebra maps form an equivalence between $P(Y^X)$ and $P(Y)^X$.

    Does the edit I made at function extensionality look alright to you?

13. • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeJan 16th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexAh, I see. I don't quite understand the remark "(although this can be derived from the global element formulation by using the Yoneda lemma together with currying and uncurrying tricks)". Can you elaborate?

    Ah, I see.

    I don’t quite understand the remark “(although this can be derived from the global element formulation by using the Yoneda lemma together with currying and uncurrying tricks)”. Can you elaborate?

14. • CommentRowNumber14.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 16th 2012
    • (edited Jan 16th 2012)
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexMike, I have to admit that I didn't check this super-carefully. Given a map $f_1: Z \to P(Y)^X$ in $\mathcal{C}/Y^X \times Y^X$, I want to produce a map $Z \to P(Y^X)$ in the same category; with fingers crossed, you get back the first map (or at least something equivalent to the first map) when you post-compose with the algebra map $P(Y^X) \to P(Y)^X$. Curry the first map to get a map $f_2: 1 \to (P(Y)^X)^Z$ or equivalently a map $f_3: 1 \to P(Y)^{X \times Z}$ in the slice $\mathcal{C}/Y^{X \times Z} \times Y^{X \times Z}$. By the global elements formulation of function extensionality (1), we can lift this to a map $f_4: 1 \to P(Y^{X \times Z})$. (Remark that liftings in the underlying category are liftings in slices.) Now post-compose this with the canonical map $P(Y^{X \times Z}) \to P(Y^X)^Z$ to get a map $f_5: 1 \to P(Y^X)^Z$, again in this slice. Finally, we can uncurry this to arrive at a map $f_6: Z \to P(Y^X)$, this time in the slice over $Y^X \times Y^X$. Now I think when you post-compose $f_6$ with $P(Y^X) \to P(Y)^X$, you get something equivalent to the map $f_1$ we started with. This ought to be deducible by considering $P(Y^{X \times Z})$ as an initial algebra (2). Namely, there may be various algebra maps $P(Y^{X \times Z}) \to (P(Y)^X)^Z$, e.g., the evident string of maps $$P(Y^{X \times Z}) \to P(Y)^{X \times Z} \cong (P(Y)^X)^Z$$ or the evident string of maps $$P(Y^{X \times Z}) \cong P((Y^X)^Z) \to P(Y^X)^Z \to (P(Y)^X)^Z,$$ but any two such algebra maps are equivalent. Applied to the global element $f_4$, the first string sends it to $f_2$. The second string sends it to the value of the map $P(Y^X)^Z \to (P(Y)^X)^Z$ applied to $f_5$. When you put all this together in the uncurried picture, where $f_2$ uncurries to $f_1$ and $f_5$ to $f_6$, you should get the first sentence of this paragraph, unless I've goofed somewhere. Finally, in Yoneda fashion, apply all this to the case where $f_1$ is the identity map on $P(Y)^X$. Notes: (1) "Global elements formulation of function extensionality", that you can lift elements $1 \to P(Y)^W$ through $P(Y^W) \to P(Y)^W$, is the statement that I get when I take what was written on that page (in the Definition section, before my edit) _literally_, even though, as I suggested in my edit, I don't think we want to constrain ourselves to global elements. The argument I have tried to give here purports to derive a stronger-looking statement from the global elements formulation. (2) I have to say that a lot of this stuff only made sense to me after your first private email to me, explaining the initial algebra or inductive type meaning of identity types -- that together with your Math Camp notes on induction for equality. For example, all the type-theoretic stuff about dependent elimination, $J$, etc., were things I didn't grok at all before placing it in the simple and clean framework of initial algebras, which is something I can really sink my teeth into! Your reaction in #9 suggests that I am expressing myself in ways that might be considered idiosyncratic to the HoTT experts, but anyway "initial algebras" have become for me a vital key of entry into this area, and I'm not sure why others aren't expressing themselves more in this kind of way. Induction over equality is really mind-blowing, and much more wonderful than the invention of sliced bread! You grow up thinking that equality is this simple and obvious thing, but it sometimes seems there is nothing in mathematics so simple that you can't make something of it on a much deeper level. :-)

    Mike,

    I have to admit that I didn’t check this super-carefully. Given a map $f_1: Z \to P(Y)^X$ in $\mathcal{C}/Y^X \times Y^X$, I want to produce a map $Z \to P(Y^X)$ in the same category; with fingers crossed, you get back the first map (or at least something equivalent to the first map) when you post-compose with the algebra map $P(Y^X) \to P(Y)^X$.

    Curry the first map to get a map $f_2: 1 \to (P(Y)^X)^Z$ or equivalently a map $f_3: 1 \to P(Y)^{X \times Z}$ in the slice $\mathcal{C}/Y^{X \times Z} \times Y^{X \times Z}$. By the global elements formulation of function extensionality (1), we can lift this to a map $f_4: 1 \to P(Y^{X \times Z})$. (Remark that liftings in the underlying category are liftings in slices.) Now post-compose this with the canonical map $P(Y^{X \times Z}) \to P(Y^X)^Z$ to get a map $f_5: 1 \to P(Y^X)^Z$, again in this slice. Finally, we can uncurry this to arrive at a map $f_6: Z \to P(Y^X)$, this time in the slice over $Y^X \times Y^X$.

    Now I think when you post-compose $f_6$ with $P(Y^X) \to P(Y)^X$, you get something equivalent to the map $f_1$ we started with. This ought to be deducible by considering $P(Y^{X \times Z})$ as an initial algebra (2). Namely, there may be various algebra maps $P(Y^{X \times Z}) \to (P(Y)^X)^Z$, e.g., the evident string of maps

    $$P(Y^{X \times Z}) \to P(Y)^{X \times Z} \cong (P(Y)^X)^Z$$

    or the evident string of maps

    $$P(Y^{X \times Z}) \cong P((Y^X)^Z) \to P(Y^X)^Z \to (P(Y)^X)^Z,$$

    but any two such algebra maps are equivalent. Applied to the global element $f_4$, the first string sends it to $f_2$. The second string sends it to the value of the map $P(Y^X)^Z \to (P(Y)^X)^Z$ applied to $f_5$. When you put all this together in the uncurried picture, where $f_2$ uncurries to $f_1$ and $f_5$ to $f_6$, you should get the first sentence of this paragraph, unless I’ve goofed somewhere.

    Finally, in Yoneda fashion, apply all this to the case where $f_1$ is the identity map on $P(Y)^X$.

    Notes:

    (1) “Global elements formulation of function extensionality”, that you can lift elements $1 \to P(Y)^W$ through $P(Y^W) \to P(Y)^W$, is the statement that I get when I take what was written on that page (in the Definition section, before my edit) literally, even though, as I suggested in my edit, I don’t think we want to constrain ourselves to global elements. The argument I have tried to give here purports to derive a stronger-looking statement from the global elements formulation.

    (2) I have to say that a lot of this stuff only made sense to me after your first private email to me, explaining the initial algebra or inductive type meaning of identity types – that together with your Math Camp notes on induction for equality. For example, all the type-theoretic stuff about dependent elimination, $J$, etc., were things I didn’t grok at all before placing it in the simple and clean framework of initial algebras, which is something I can really sink my teeth into! Your reaction in #9 suggests that I am expressing myself in ways that might be considered idiosyncratic to the HoTT experts, but anyway “initial algebras” have become for me a vital key of entry into this area, and I’m not sure why others aren’t expressing themselves more in this kind of way.

    Induction over equality is really mind-blowing, and much more wonderful than the invention of sliced bread! You grow up thinking that equality is this simple and obvious thing, but it sometimes seems there is nothing in mathematics so simple that you can’t make something of it on a much deeper level. :-)

15. • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeJan 17th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexOkay, I think I believe that. Thanks! > Global elements formulation of function extensionality"... is the statement that I get when I take what was written on that page (in the Definition section, before my edit) literally Ah, I see. Actually, anything which is "said in type theory" is automatically "internalized". So even though the statement in type theory of function extensionality looks as though it is referring only to global elements, actually it is referring to arbitrary elements, Yonedified, just as in any other sort of internal categorical logic. I see that this is not very clear from the current state of the page, however! > Your reaction in #9 suggests that I am expressing myself in ways that might be considered idiosyncratic to the HoTT experts I wouldn't read that much into it; I just didn't draw the connection between the words. Perhaps I was having an off day. (-: Maybe type theorists don't talk so much about initial algebras explicitly when doing pure type theory (as opposed to its categorical semantics), but initial algebras are also a big part of the way I think about inductive types, and almost always the way that I try to explain them to homotopy theorists and category theorists. I think this may have even become more true for me over the past year or so. This might be a good time to mention that I've posted the [slides](http://www.math.ucsd.edu/~mshulman/papers/indcell.pdf) from my talk about higher inductive types at the joint meetings homotopy theory session. Since this was a 20min talk for homotopy theorists without any knowledge of type theory, it necessarily skims quite lightly over the surface. But note the frequent use of initial algebras. (-: > Induction over equality is really mind-blowing, and much more wonderful than the invention of sliced bread! I agree entirely!

    Okay, I think I believe that. Thanks!

    Global elements formulation of function extensionality”… is the statement that I get when I take what was written on that page (in the Definition section, before my edit) literally

    Ah, I see. Actually, anything which is “said in type theory” is automatically “internalized”. So even though the statement in type theory of function extensionality looks as though it is referring only to global elements, actually it is referring to arbitrary elements, Yonedified, just as in any other sort of internal categorical logic. I see that this is not very clear from the current state of the page, however!

    Your reaction in #9 suggests that I am expressing myself in ways that might be considered idiosyncratic to the HoTT experts

    I wouldn’t read that much into it; I just didn’t draw the connection between the words. Perhaps I was having an off day. (-: Maybe type theorists don’t talk so much about initial algebras explicitly when doing pure type theory (as opposed to its categorical semantics), but initial algebras are also a big part of the way I think about inductive types, and almost always the way that I try to explain them to homotopy theorists and category theorists. I think this may have even become more true for me over the past year or so.

    This might be a good time to mention that I’ve posted the slides from my talk about higher inductive types at the joint meetings homotopy theory session. Since this was a 20min talk for homotopy theorists without any knowledge of type theory, it necessarily skims quite lightly over the surface. But note the frequent use of initial algebras. (-:

    Induction over equality is really mind-blowing, and much more wonderful than the invention of sliced bread!

    I agree entirely!