added (here) the statement in the generality of dependent functions and highlighted its analogy to the extensionality principle for dependent pairs.

]]>I think the confusion among the guests above stems from the fact that while the internal logic of a locally cartesian closed category with pullbacks is a dependent type theory with dependent function types, dependent pair types, identity types, and equality reflection making the type theory into an extensional type theory, in general, most dependent type theories aren’t the internal logic of a locally cartesian closed category with pullbacks. This has implications regarding function extensionality not being provable in dependent type theories except for the case for judgmental equality.

John Masi

]]>@63

MLTT isn’t the internal logic of a Heyting pretopos either because dependent products of families of propositions are only propositions in MLTT if and only if function extensionality holds.

]]>added actual type theoretic notion of function extensionality to the set theory paragraph: one needs to use a family of sets $(\Delta_{A}(x, y))_{x \in A, y \in A}$ such that the set $\{p \in \Delta_{A}(x, y) \vert x \in A, y \in A\}$ is the diagonal subset of $A$; this represents the internal notion of equality in set theory, rather than the external notion of equality in set theory.

Anonymous

]]>So then what category does Martin-Löf type theory with propositional truncations and quotient sets but without function extensionality result in? Clearly it is not a Pi-W-pretopos because function extensionality fails.

]]>Revert part of the last edit, which again claims that a type theory with function extensionality is modeled only by well-pointed categories. This is not the case, as function extensionality is valid in topos models that are not well-pointed as described already.

]]>added the notion of function extensionality for elements of function sets in set theory; this, rather than the other notion of function extensionality for morphisms in hom-sets, is the notion that corresponds to function extensionality in type theory, since functions in type theory are elements of function types.

Anonymous

]]>exponential -> exponential object

exponential redirects to exponential map from analysis

Anonymous

]]>replacing “action of” with “function application to” in the article

Anonymous

]]>In the set theory section, function extensionality refers to the function sets in the set theory, rather than the external homs themselves. This means that for all sets $A$ and $B$ and elements of the function set $f \in B^A$ and $g \in B^A$, if for all elements $a \in A$, $\mathrm{ev}(f, a) = \mathrm{ev}(g, a)$, then $f = g$.

It is not what is currently stated, that for all functions $f:A \to B$ and $g:A \to B$, if for all elements $a \in A$, $f(a) = g(a)$, then $f = g$. That is well-pointedness.

]]>Add a discussion of the difference between function extensionality and well-pointedness.

]]>Ever since revision 19 (20 Oct 2022, by “Anonymous”) the entry has a broken link to “singleton contractibility” (here)

I guess this means to be pointing to *singleton induction*?

I have merged the sections “Categorical semantics” and “Homotopy categorical semantics” (now jointly here), as they are really about the same issue: the former talked about what it means, and the latter (which contained nothing but a single Proposition) talked about when that holds.

]]>have re-written and re-typeset most of the section “Categorical semantics” (here)

(up to and excluding the sentence starting with “Of course we are…”).

]]>Thanks for pointing this out, fair enough. I’ll try to streamline that paragraph tomorrow morning, when I am more awake than now.

]]>The text was already there prior to revision 19; the only thing revision 19 did was separate it into a separate section called “Categorical semantics”. The text first appeared in revision 7 by Todd Trimble on January 15, 2012 and was modified into its current state in revision 9 by Urs Schreiber on January 15, 2012.

]]>added pointer to the original announcement that univalence implies funext:

- Vladimir Voevodsky, p. 8 of:
*Univalent Foundations Project*(2010) [pdf, Voevodsky-UFP2010.pdf:file]

I notice that the section “Categorical semantics” (here, from Anonymous revision 19) starts out somewhat awkwardly:

It refers to a “term $\eta$” which was never introduced and claims that this “gives” what the following lines evidently mean to be a *choice* of a global element.

Also the notation “$[f x = g x]$” for $\sum_{x} Id_Y\big( f(x) , g(x) \big)$ is maybe unnecessarily odd.

I could adjust this myself, but maybe I am out of steam for the moment.

]]>I have touched wording, hyperlinking and the math typesetting in the section *Definition – In type theory* (here)

I have re-arranged the list of references (here), to bring in some logical order

in the process I have added publication data to this item:

- Richard Garner,
*On the strength of dependent products in the type theory of Martin-Löf*Annals of Pure and Applied Logic**160**1 (2009) 1-12 [arXiv:0803.4466, doi:10.1016/j.apal.2008.12.003]

By the way, the two pointers to `Funext.v`

in the Coq/HoTT repository were both dead, so I have deleted them for the moment. If anyone has a working link, let’s add it back in.

In this vein, I added pointer to discussion in Agda:

]]>adding proof that the interval type with judgmental computation rules implies function extensionality, and why the proof fails with typal computational rules for the interval type.

Anonymous

]]>Fixed the title again: from

Towards a Third-Generation HOTT Part 1

to

]]>

Towards Third-Generation HOTT – Part 1

Adding reference

- Mike Shulman,
*Towards a Third-Generation HOTT Part 1*(slides, video)

Anonymous

]]>Added section on definitional function extensionality

Anonymous

]]>