Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

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 internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology 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 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

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: function extensionality

Bottom of Page

1 to 67 of 67

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeNov 25th 2011
    • CommentRowNumber2.
    • CommentAuthorTobyBartels
    • CommentTimeNov 29th 2011

    I put in a simpler Idea section.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeDec 6th 2011
    • (edited Dec 6th 2011)

    I have tried to polish the statements about function extensuionality at intensional type theory and extensional type theory, making explicit the distinction between function extensionality that holds by identities and that which holds by equivalences.

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeDec 12th 2011

    So, this is not the only meaning of extensional/intensional as applied to type theories. Many people, especially in the HoTT community (like me), use it to refer to the behavior of identity types, not the behavior of function types. According to this usage, type theory is extensional if all identity types are (-1)-truncated, and intensional otherwise. This distinction is orthogonal to the question of function extensionality. OTOH many type theorists do seem to use the words in the way that you did. I think the former usage is more useful when talking about HoTT, but perhaps our pages should mention both usages for disambiguation.

    Also, I don’t understand what you mean by the difference between function extensionality holding by identities and holding by equivalences. The function extensionality principle says that if ∀x,f(x)=g(x)\forall x, f(x) = g(x), then f=gf=g. Of course we interpret the == signs by identity types; I don’t see any other option. If the theory is intensional/homotopic then we think of the identity types as path types, but the formal statement of function extensionality is the same. Can you explain further what you’re thinking of?

    (There are also different “strong”, “weak”, “dependent” and “non-dependent” flavors of function extensionality, but that seems to be an orthogonal question….)

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeDec 12th 2011

    Hi Mike,

    thanks for the comment.

    What happend was that I saw somewhere the definition of “extensional type theory” as one which has function extensionality. Then I noticed that this is in conflict with function extensionality in HoTT and concluded that what must be meant is that in the latter case function extensionality holds by terms of “intensional identity types” (equivalences) instead of by terms of “extensional identity types”.

    So thanks for the clarification. I have tried to reword the intro at extensional type theory accordingly, but please check.

    I can certify that the literature on this point is not very helpful to newcomers. So it would be good if eventually the nnLab could improve on this situation.

    One aspect that keeps bugging me: I have no idea why the English words “extensional” and “intensional” have been chosen. (This and the completely intransparent term “univalence” were quite a hinderance for me at the beginning to get a quick feel for what all the type theory speak is about. It’s a bit of a secret language at the beginning, that gives little hints to the outsider.)

    The only English sense that I can make of “extensional” is as in “an argument-wise identity of functions extends to an identity of the functions themselves”. But by what you just said, this is precisely not the right interpretation. :-/

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeDec 12th 2011

    In general, “extensional” means that something is determined by its extension, which is to say how it behaves on the collection of things to which it applies. Thus the axiom of extensionality in set theory means that a set is determined by its extension — the collection of things that belong to it. Function extensionality means that a function is determined by its meaning on its extension — its values on all possible inputs (the collection of things to which it applies). Extensional identity types mean that an identity type is determined by its extension — the collection of points xx and yy such that x=yx=y. They are not entirely parallel (for instance, in HoTT with function extensionality, identity types are extensional as functions A→A→TypeA\to A\to Type), but there is some consistency at least. I’ve edited extensional type theory some; intensional type theory still needs some work.

    I do agree that terminology in type theory is difficult for newcomers! I was in that boat not too long ago (and still am, in some respects). I explained the origin of the term “univalence” in my blog post about it, but I’ve now also added a summary thereof to univalence axiom. It’s perhaps not the most evocative word, but at least for me it doesn’t conjure up any other meanings, so I have no trouble remembering what it means.

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeDec 12th 2011
    • (edited Dec 12th 2011)

    In general, “extensional” means that something is determined by its extension,

    Ah, I see. I didn’t know this use of the word “extension” at all.

    I have made extension (semantics) an nnLab stub, for future use.

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeDec 12th 2011

    Okay, I updated intensional type theory too.

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeJan 13th 2017

    A question:

    Given that it is still open whether HoTT+UV strictHoTT+UV_{strict} has interpretation in (suitable model categories presenting) any ∞\infty-stack ∞\infty-topos, and since the problematic piece is just the UV strictUV_{strict}, how about modelling the weaker axiom of function extensionality?

    Does HoTT+FunExtHoTT + FunExt have interpretation in (suitable model categories presenting) any ∞\infty-stack ∞\infty-topos?

    Is this easy to see? If not, what’s a sticking point?

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeJan 13th 2017

    Yes, the constructions of Cisinski-Shulman and Gepner-Kock give right proper Cisinski model categories, and those support funext too. Categorically, funext means that dependent product along fibrations preserves acyclic fibrations, which follows in a Cisinski model category from the fact that pullback preserves monomorphisms.

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeJan 13th 2017

    Thanks!

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeJan 13th 2017

    Categorically, funext means that dependent product along fibrations preserves acyclic fibrations,

    This I need to think about. That’s neat. We should spell this out on the nnLab.

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeJan 13th 2017
    • (edited Jan 13th 2017)

    Oh, sorry, now I see that this is of course in your arXiv.1203.3253, around p. 27. I’ll have a closer look…

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeJan 13th 2017
    • (edited Jan 13th 2017)

    So I have recorded this cool statement here and here.

    Too bad that I had missed this all along.

    There are loads of proofs that use FunExt but not full UV. Such as most of Felix Wellen’s results. Now I see that all this provably has interpretation in all the ∞\infty-toposes. I could have saved myself some headaches had I appreciated this earlier.

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeJan 14th 2017

    Note, though, that the problem is not just with univalence, but with strict universe objects. The type theory used by Coq and Agda has strict universes, so formally speaking it is not known to be interpretable in an arbitrary ∞-topos, even if you don’t use univalence. Sometimes it is obvious that the universes are not really being used and essentially the same proof could be written in a type theory (with funext but) without any universes at all (which is what we can interpret in any locally cartesian closed (∞,1)-category, modulo the initiality conjecture for type theory), but other times the universe is actually playing a role even if it isn’t univalent.

    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeJan 14th 2017

    but other times the universe is actually playing a role even if it isn’t univalent.

    Is it hard to say this precisely?

    I am thinking: the plain universe is used to get type families essentially equivalent to dependent types, and so its strictness is the strictness of the pullbacks in the model, and that is part of the coherence/rectification business which we think of as being packaged away and solved independently as we speak.

    Is that it, or is there more to it?

    • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeJan 20th 2017

    Yes, there’s more. (Sorry, I didn’t notice this until now.) Sometimes in type theory we really do use the fact that the universe is a type, not just that maps into it have strict composition. One of the most common instances of this in when mapping into it with the eliminator of an inductive type; for a HIT this requires the universe to be univalent, but for an ordinary inductive type it doesn’t. In particular, without a universe, it’s not possible to prove in type theory that 0≠10\neq 1.

    • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeJan 20th 2017

    And any time you say in formalized type theory something like “a group is a type together with …”, formally what you are doing is making a ∑\sum-type over the universe, which therefore has to be a type. And any time you prove a theorem in type theory like “for any type AA…”, formally you are quantifying over the universe, i.e. defining an element of a ∏\prod-type over the universe. Often (usually?) one can imagine circumlocutions and meta-theoretic ways of saying equivalent things without a universe, but the fact remains that an actual formalization in existing proof assistants technically uses universes all over the place.

    • CommentRowNumber19.
    • CommentAuthorTobyBartels
    • CommentTimeJan 21st 2017

    In particular, without a universe, it’s not possible to prove in type theory that 0≠10\neq 1.

    This seems like an odd way to put it. Assuming that by 00 and 11 you mean the empty and trivial types (rather than the natural numbers, which would make this an even odder thing to say), then without a universe for these types to belong to and to have its own equality types, you cannot formally state 0≠10 \ne 1. But to the extent that you can state it, you can prove it.

    For example, Martin-Löf type theory has equality judgements between types, independently of any universes (which in some versions of his theory don't exist, at least not at all levels). So you can state 0=10 = 1 (but not 0≠10 \ne 1) in this way, and then you can derive a contradiction from that. Therefore, 00 does not equal 11.

    Similarly, in ZFC, you cannot state Ord≠CardOrd \ne Card, because you cannot speak about the proper classes OrdOrd and CardCard, but you can prove ¬(∀x,O(x)⇔K(x))\neg\;(\forall x,\; O(x) \;\Leftrightarrow\; K(x)), where O(x)O(x) and K(x)K(x) are translations of x∈Ordx \in Ord and x∈Cardx \in Card into proper ZFC. But it would be odd to explain the usefulness of GNB by saying that you cannot prove Ord≠CardOrd \ne Card in ZFC. It would be even odder to explain the usefulness of MK in this way, to the point of being downright wrong, since MK is a stronger theory whose additional strength is not necessary to prove this theorem.

    Circumlocutions for the examples in #18 are also possible, and the one for

    And any time you prove a theorem in type theory like “for any type AA…”, formally you are quantifying over the universe, i.e. defining an element of a ∏\prod-type over the universe.

    is bog standard. You absolutely can write AType⊢⋯A Type \vdash \cdots without universes. You may or may not allow introduction of type variables on the left side of a sequent, but you can allow it without promoting TypeType to a type.

    All of this is important, because it speaks to the strength of the theory. Just as MKMK is stronger than ZFCZFC (but NBGNBG is not), so type theory with universes (even just one level) is stronger than type theory without them. But if you think that this means that type theory without universes is too weak to prove 0≠10 \ne 1, anything about groups, or anything about all types, then that is not so. If you just want a convenient language and don't care about proof-theoretic strength, then sure, use universes. But if you do care about strength (and lots of people do), then you shouldn't say that you need universes for something that can be said in another way without them.

    • CommentRowNumber20.
    • CommentAuthorMike Shulman
    • CommentTimeJan 21st 2017

    By 00 and 11 I meant the natural numbers. It is actually true that type theory without universes cannot prove that the natural numbers 0 and 1 are unequal. I don’t know about formal “proof-theoretic strength”, but type theory without universes has posetal models in which in fact 0=1:ℕ0=1:\mathbb{N}.

    Martin-Löf type theory has equality judgements between types, independently of any universes (which in some versions of his theory don't exist, at least not at all levels). So you can state 0=10 = 1 (but not 0≠10 \ne 1) in this way, and then you can derive a contradiction from that.

    This is I guess true in some way, but it’s not formally completely analogous to ¬(∀x,O(x)⇔K(x))\neg\;(\forall x,\; O(x) \;\Leftrightarrow\; K(x)), since the latter is a single theorem of ZFC, whereas a judgmental equality cannot be hypothesized inside MLTT. You can prove a meta-theorem like “in MLTT augmented with an additional rule allowing us to judge Empty≡UnitEmpty \equiv Unit, we can derive an inhabitant of EmptyEmpty,” but that’s not just a restatement of a theorem inside the theory that Empty≠UnitEmpty \neq Unit. For instance, inside MLTT we can prove that EmptyEmpty has no elements, but it is a very different thing to say meta-theoretically that there are no terms of MLTT that can be judged to be of type EmptyEmpty; the latter is a consistency statement about the theory that requires a substantial amount of work, whereas the former is essentially trivial by the internal definition of EmptyEmpty and “no elements”.

    You may or may not allow introduction of type variables on the left side of a sequent, but you can allow it without promoting TypeType to a type.

    Well, to start with, even that falls substantially short of the things we can (and often do) do with a universe (even before assuming univalence). For instance, if we want to prove “if excluded middle holds, then …”, we are hypothesizing a statement of the form “for all propositions/types AA, …”, which simply having type variables on the left of a sequent doesn’t allow. Similarly, the theory of modalities involves universal properties, which are also quantifications over all types; so any time you want to assume that something has a universal property, you are out of luck if all you can do is put type variables on the left of a sequent.

    But most relevantly to the original point, the type theory that we know how to model in arbitrary ∞-toposes does not allow type variables on the left of a sequent. I’ve occasionally thought about whether we could model such a theory, but I haven’t come up with any ideas for how to do that without essentially modeling universes. So these examples are relevant to Urs’s real question of what type-theoretic arguments we know how to internalize in all ∞-toposes.

    • CommentRowNumber21.
    • CommentAuthorTobyBartels
    • CommentTimeJan 22nd 2017
    • (edited Jan 22nd 2017)

    It is actually true that type theory without universes cannot prove that the natural numbers 0 and 1 are unequal.

    Can you explain what you mean by ‘type theory without universes’? Since you speak of its models, you presumably have something specific in mind. (I guess that you mean a theory that can be internalized in all ∞\infty-toposes.) There exist type theories without universes but with Peano (or Heyting) arithmetic, which is what your comment at first seems to deny; but if by ‘type theory without universes’ you mean a specific theory, then my remarks may be out of order.

    (Ironically, it seems to have been fashionable in the middle of the 20th century for formal systems in constructive mathematics to define ¬P\neg{P} as P⇒(0= ℕ1)P \Rightarrow (0 =_{\mathbb{N}} 1), out of a desire to avoid admitting ⊥\bot to the ambient propositional calculus. Then ¬(0= ℕ1)\neg(0 =_{\mathbb{N}} 1) becomes very easy to prove. But as far as I know, this was never incorporated into any type theories.)

    For instance, if we want to prove “if excluded middle holds, then …”, we are hypothesizing a statement of the form “for all propositions/types AA, …”

    When I write something like that, I'm definitely thinking ‹If we allow ourselves to use excluded middle in our reasoning›, which formally is much more like adding an additional rule to the theory than making a hypothesis within the theory. Or if we think about internalizing things in [higher] categories, a statement that begins ‘if excluded middle holds’ isn't a statement that I intend to internalize; it's saying that I intend to internalize whatever follows only in categories with this additional feature. You make it sound like saying ‘if excluded middle holds’ while doing constructive math is analogous to saying ‘if the Riemann hypothesis holds’ (or perhaps, saying ‘if P=NP\mathrm{P} = NP’) when doing number theory; but to me it indicates that I'm not doing constructive math anymore, at least temporarily.

    • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeJan 22nd 2017

    Yes, by “type theory without universes” I mean the type theory that we know how to model in ∞-toposes: MLTT with ∑,∏,+,0,1,Id,ℕ\sum,\prod,+,0,1,Id,\mathbb{N} and function extensionality, but no universes. Any Heyting algebra also models it.

    • CommentRowNumber23.
    • CommentAuthorMike Shulman
    • CommentTimeJan 22nd 2017

    Perhaps excluded middle was a bad example to make my point. How about instead “if f:A→Bf:A\to B is left orthogonal to all ◯\bigcirc-modal types”?

    • CommentRowNumber24.
    • CommentAuthorTobyBartels
    • CommentTimeJan 23rd 2017

    Yes, that example works better.

    MLTT usually has universes, so even ‘MLTT with ∑,∏,+,0,1,Id,ℕ\sum,\prod,+,0,1,Id,\mathbb{N} and function extensionality, but no universes’ is a little unclear, since what you get upon removing an axiom depends on how you present it. (For instance, you might think that removing the axiom of choice from ETCS leaves you with the theory of a well-pointed Boolean topos with an NNO, but if you follow the presentation of Lawvere's original paper, then you can't even prove that you have a topos without Choice.) Since even this theory has type formation judgements, then arguably such judgements should be allowed in the elimination rules of inductive types, which allows you to prove ¬0= ℕ1\neg\; 0 =_{\mathbb{N}} 1 and the like. But then that can't be modelled in a Heyting algebra or a topos (and while I don't know ∞\infty-toposes so well, I wouldn't expect them to fix this).

    But if you use MLTT without universes and only allow judgements of the form a:Aa\colon A (where AA is a type) in the elimination rules, then I agree, you cannot prove ¬0= ℕ1\neg\; 0 =_{\mathbb{N}} 1, or indeed the negation of any equality.

    (Allowing type formation judgements in the elimination rules lets you define families of types and so is like the axiom of replacement in set theory. So a step up in strength, albeit less of a step up than a full-fledged universe.)

    • CommentRowNumber25.
    • CommentAuthorMike Shulman
    • CommentTimeJan 23rd 2017

    Right, assuming “large elims” as basic recovers some of the strength of a universe. However, I’ve never seen “MLTT” presented with large elims as basic, so I would never assume that they were still there upon removing the universes from MLTT. But you’re right that it’s always better to be specific.

    • CommentRowNumber26.
    • CommentAuthorTobyBartels
    • CommentTimeJan 23rd 2017

    I haven't seen that either, but I've only ever seen it presented with universes. (He did reportedly have a version with only one (predicative) universe, but I haven't seen that one.) I have seen it presented with judgemental identity in elimination rules, however, in versions where identity is intensional, and I would argue that a version without universes should include type formation judgements on the same principle.

    Anyway, I know what theory you meant, and we're not disagreeing about that.

    • CommentRowNumber27.
    • CommentAuthorMike Shulman
    • CommentTimeJan 24th 2017

    Wow, I’ve never seen judgmental equality in elimination rules. That’s also wrong homotopically.

    • CommentRowNumber28.
    • CommentAuthorTobyBartels
    • CommentTimeJan 25th 2017

    Can you explain briefly why it's wrong homotopically?

    • CommentRowNumber29.
    • CommentAuthorMike Shulman
    • CommentTimeJan 25th 2017

    The elimination rule for the identity type, in particular, is generally interpreted categorically by a weak factorization system such as (acyclic cofibrations, fibrations). This only works to eliminate into other fibrations, since the elimination is a lifting according to the factorization system. But judgmental equality is generally interpreted by the categorical diagonal, which is not a fibration at all. Voevodsky’s HTS has a distinction between “fibrant types” and “non-fibrant types”, with judgmental equality reified as a non-fibrant “strict equality” type, and only fibrant types can be eliminated into by the rules of other fibrant types.

    Actually, wouldn’t eliminating from the identity type into judgmental equalities internally imply the reflection rule and make the type theory extensional?

    • CommentRowNumber30.
    • CommentAuthorTobyBartels
    • CommentTimeJan 27th 2017

    Eliminating from Γ⊢p:eq A(x,y)\Gamma \vdash p\colon eq_A(x, y) to Γ⊢x=y:A\Gamma \vdash x = y\colon A would make the theory extensional, but I don't think that that's supposed to happen.

    The rules that should appear here (going by intuition, not memory) should be like

    ⊢z:A+B;x:A⊢u= Cv;y:B⊢u= Cv⊢u= Cv. \frac{\vdash z\colon A + B;\; x\colon A \vdash u =_C v;\; y\colon B \vdash u =_C v} {\vdash u =_C v} .

    That is, if either a term of type AA or a term of type BB is sufficient to judge uu qnd vv identical of type CC, then a term of type A+BA + B should also be sufficient.

    Actually, the full version of that rule (with all terms and types dependent on the full context) would be

    ⊢z:A+B;x:A⊢s[x]= C[x]t[x];y:B⊢u[y]= D[y]v[y]⊢match(z,s,u)= match(z,C,D)match(z,t,v). \frac{\vdash z\colon A + B;\; x\colon A \vdash s[x] =_{C[x]} t[x];\; y\colon B \vdash u[y] =_{D[y]} v[y]} {\vdash match (z, s, u) =_{match (z, C, D)} match (z, t, v)} .

    (Incidentally, match(z,C,D)match (z, C, D) is the type guaranteed by my type formation elimination rule if there is no universe to do it in.)

    The abbreviated (non-dependent) version of the equality-type elimination rule would be:

    x:A⊢u= Cv;⊢p:eq A(a,b)⊢u= Cv, \frac{x\colon A \vdash u =_C v;\; \vdash p\colon eq_A(a,b)} {\vdash u =_C v} ,

    which doesn't say anything; and here's the full (dependent) version:

    x:A⊢u[x,x,refl x]= C[x,x,refl x]v[x,x,refl x];⊢p:eq A(a,b)⊢u[a,b,p]= C[a,b,p]v[a,b,p]. \frac{x\colon A \vdash u[x,x,refl_x] =_{C[x,x,refl_x]} v[x,x,refl_x];\; \vdash p\colon eq_A(a,b)} {\vdash u[a,b,p] =_{C[a,b,p]} v[a,b,p]} .

    OK, I agree that this is a problem; if C[x,y,q]≔AC[x,y,q] \coloneqq A, u[x,y,q]≔xu[x,y,q] \coloneqq x, and v[x,y,q]≔yv[x,y,q] \coloneqq y, then from p:eq A(a,b)p\colon eq_A(a,b), this proves a= Aba =_A b.

    The best thing that I can say now, without remembering where I saw this done, is that you just shouldn't include this rule; leave out the elimination rule for identity judgements from equality types.

    • CommentRowNumber31.
    • CommentAuthorMike Shulman
    • CommentTimeJan 28th 2017

    For consistency, one ought then to leave out the elimination rule for identity judgments from any type, no?

    • CommentRowNumber32.
    • CommentAuthorTobyBartels
    • CommentTimeJan 28th 2017

    Maybe. Although equality types are different from other inductive types (or at least the other common ones), so there is a general rule that could be applied here. I'm not sure what the philosophy was behind the system where I saw this.

    I can tell you something of the system that I was going to put on my personal web, but never did (since I decided that HoTT was a better approach to foundations). Here, I not only rejected universes (which was just to keep things simple, and in fact I also considered how to add them as an optional feature) but also rejected equality types (which was the main point). So I needed my elimination rules to produce both type formation judgements and identity judgements (actually I ended up using non-symmetric convertibility judgements). And since I didn't have equality types (in general, I allowed only restricted inductive families in the sense of this paper by Dybjer & Setzer, although that is not where I learnt about them), this did not cause any problems.

    • CommentRowNumber33.
    • CommentAuthorUrs
    • CommentTimeFeb 7th 2017
    • (edited Feb 7th 2017)

    Thanks for all the reactions to #9! (Belated thanks, sorry.)

    I see. So I am back to being frustrated then. :-)

    What happend to the claim that if one looks closely enough at the code, then the universes in Coq actually are weak Tarskian?

    I believe Peter Lumsdaine told me about this. This was at the beginning of last year, during the HoTT meeting in Bonn. Do you know what this is referring to?

    • CommentRowNumber34.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 7th 2017

    No, I never understood what Peter meant by that. I’ve never looked at the source code of Coq, but to a user the universes certainly seem Russellian.

    • CommentRowNumber35.
    • CommentAuthorUrs
    • CommentTimeFeb 7th 2017
    • (edited Feb 7th 2017)

    No, I never understood what Peter meant by that.

    All right, I’ll try to ask Peter then.

    I’ve never looked at the source code of Coq, but to a user the universes certainly seem Russellian.

    If the claim is that down at the level of the kernel of Coq the universe is weak Tarskian, but then by some interfacing it is made to look strict Russelian to the user, this might just be the syntactic version of the sought-after claim (that all ∞\infty-toposes have a presentation in which the object classifier interprets a strict Russelian universe).

    I’ll check with Peter.

    • CommentRowNumber36.
    • CommentAuthorspitters
    • CommentTimeFeb 8th 2017
    • (edited Feb 8th 2017)

    Here’s Peter Lumsdaine’s observation, with my addition for Sigma.

    At first this seems to contradict Coq’s rules for subtyping. The point is that Coq lacks universe polymorphism for inductives. Amin Timani is working to fix this.

    (Sorry, I cannot get the layout to work exactly as I want.)

    Set Universe Polymorphism. Set Printing Universes. Set Printing All.

    Section Cml_List_commute.

    Section list. Universe i. Inductive myList (A : Type@{i}) : Type@{i} := | myNil : myList A | myCons (a:A) (l : myList A). End list.

    Universes u0 v0.

    Hypothesis A : (Type@{u0} : Type@{v0}). (* This adds the constraint [ u0 < v0 ], so Coq cannot later silently add the constraint [ u0 = v0 ]. *)

    Lemma myList_commute_up (x : myList@{u0} A) : myList@{v0} A. Proof. try exact x. (* FAILS! *) induction x as [ | a l IH]. apply myNil. apply myCons; auto. Defined.

    (* So Coq does not seem to validate ( cml_u^v list_{u} A ) = list_{v} (cml_u^v A) *)

    End Cml_List_commute.

    (* For Sigma *)

    Section Cml_Sig_commute.

    Section Sig.
    Print sig.
    Universe i.
    Inductive mysig (A : Type@{i})(P : forall _ : A, Type@{i})
    Type@{i} := myexist : forall (proj1_sig : A) (_ : P proj1_sig), @mysig@{i} A P. End Sig.

    Universes u0 v0.

    Hypothesis A : (Type@{u0} : Type@{v0}). Variable P: forall _ : A, Type@{u0}. (* This adds the constraint [ u0 < v0 ], so Coq cannot later silently add the constraint [ u0 = v0 ]. *)

    Lemma mysig_commute_up (x : mysig@{u0} A P) : mysig@{v0} A P. Proof. try exact x. (* FAILS! *) induction x as [a p]. exact (myexist A P a p). Defined.

    (* So Coq does not seem to commute commutativity with Sigma either. *)

    • CommentRowNumber37.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 8th 2017

    Okay, so when you construct an inductive type, it matters which universe you do it in. That’s certainly something that’s true about weak Tarski universes and not true about strong Tarski universes as usually defined. However, Coq’s universes do have many other properties that are true about strong Tarski universes and not true about weak Tarski universes, such as:

    • Π\Pi-types do have strict cumulativity, i.e. they don’t care which universe you construct them in, and
    • Whichever universe you construct an inductive type in, it has an eliminator with judgmental computation rule (for a weak Tarski universe this is only true for the inductive types constructed “outside of all universes”; which the ones inside universes are only equivalent to).
    • CommentRowNumber38.
    • CommentAuthorUrs
    • CommentTimeFeb 8th 2017

    Oh, I see. I thought something stronger was meant.

  39. Added link to extensionality

    Anonymous

    diff, v18, current

  40. Moving the parts in the ’type theory’ subsection of the ’definitions’ section about the categorical semantics of function extensionality into its own subsection under the ’properties’ section called ’categorical semantics’

    Anonymous

    diff, v19, current

  41. Added a section about function extensionality in set theory and expanded the category theory section with the generalization of the set theory definition

    Anonymous

    diff, v19, current

  42. Added second set theoretic definition of function equality, which will become important later in the type theoretic section for defining definitional function extensionality in higher observational type theory

    Anonymous

    diff, v19, current

  43. Added second definition of happly and function extensionality to the type theory section.

    Anonymous

    diff, v19, current

  44. Added section on definitional function extensionality

    Anonymous

    diff, v19, current

  45. Adding reference

    Anonymous

    diff, v19, current

    • CommentRowNumber46.
    • CommentAuthorUrs
    • CommentTimeOct 20th 2022

    Fixed the title again: from

    Towards a Third-Generation HOTT Part 1

    to

    Towards Third-Generation HOTT – Part 1

    diff, v21, current

  47. 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

    diff, v22, current

    • CommentRowNumber48.
    • CommentAuthorUrs
    • CommentTimeDec 28th 2022

    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:

    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:

    diff, v25, current

    • CommentRowNumber49.
    • CommentAuthorUrs
    • CommentTimeDec 28th 2022

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

    diff, v26, current

    • CommentRowNumber50.
    • CommentAuthorUrs
    • CommentTimeDec 28th 2022
    • (edited Dec 28th 2022)

    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 “[fx=gx][f x = g x]” for ∑ xId Y(f(x),g(x))\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.

    diff, v26, current

    • CommentRowNumber51.
    • CommentAuthorUrs
    • CommentTimeDec 28th 2022

    added pointer to the original announcement that univalence implies funext:

    diff, v26, current

    • CommentRowNumber52.
    • CommentAuthorGuest
    • CommentTimeDec 28th 2022

    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.

    • CommentRowNumber53.
    • CommentAuthorUrs
    • CommentTimeDec 28th 2022

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

    • CommentRowNumber54.
    • CommentAuthorUrs
    • CommentTimeDec 29th 2022
    • (edited Dec 29th 2022)

    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…”).

    diff, v27, current

    • CommentRowNumber55.
    • CommentAuthorUrs
    • CommentTimeDec 29th 2022

    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.

    diff, v27, current

    • CommentRowNumber56.
    • CommentAuthorUrs
    • CommentTimeJan 3rd 2023

    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?

    diff, v28, current

    • CommentRowNumber57.
    • CommentAuthormaxsnew
    • CommentTimeJan 19th 2023

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

    diff, v32, current

  58. 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 AA and BB and elements of the function set f∈B Af \in B^A and g∈B Ag \in B^A, if for all elements a∈Aa \in A, ev(f,a)=ev(g,a)\mathrm{ev}(f, a) = \mathrm{ev}(g, a), then f=gf = g.

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

  59. replacing “action of” with “function application to” in the article

    Anonymous

    diff, v33, current

  60. exponential -> exponential object

    exponential redirects to exponential map from analysis

    Anonymous

    diff, v33, current

  61. 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

    diff, v34, current

    • CommentRowNumber62.
    • CommentAuthormaxsnew
    • CommentTimeJan 20th 2023

    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.

    diff, v37, current

    • CommentRowNumber63.
    • CommentAuthorGuest
    • CommentTimeJan 20th 2023

    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.

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

    Anonymous

    diff, v38, current

    • CommentRowNumber65.
    • CommentAuthorGuest
    • CommentTimeJan 20th 2023

    @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.

    • CommentRowNumber66.
    • CommentAuthorGuest
    • CommentTimeJan 20th 2023

    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

    • CommentRowNumber67.
    • CommentAuthorUrs
    • CommentTimeJan 21st 2023

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

    diff, v41, current

1 to 67 of 67

  1.