> The univalance axiom is a stipulated property of type equivalence.
If so, I don't really see the difference between saying "univalence says that equivalence of types is (equivalent to) equality of types" and saying "univalence says that equivalence of types obeys the universal property of equality of types".
It seems to me that no one is paying attention to what I said:
> the majority of applications of univalence *require* type equality,
> and require moreover that it is the "same sort" of equality as all
> other equalities. Specifically, they involve defining type families
> by recursion on higher inductive types, and the recursion principle
> of a HIT requires specifying equalities in the codomain.
In particular, as I said, it's important for these applications that
the "type equality" which is identified by univalence with equivalence
IS the pre-existing notion of equality, because the pre-existing
notion of equality is what appears in the elimination rules for HITs.
I disagree with your claim that, without UA, type equality as given by the usual ("path induction") rule for Id_U is “practiaclally meaningless”.
On 08/08/14 22:17, Michael Shulman wrote:Maybe what Martin meant to say (certainly what I took him to be
saying) is "almost completely undetermined" rather than "almost
meaningless".
Yes, this is what I mean.
Also:On Fri, Aug 8, 2014 at 2:07 PM, Steve Awodey <awo...@cmu.edu> wrote:I disagree with your claim that, without UA,
I didn't say without UA. I said "without UA or K (or whatever you can come up with)".
I know of *no* interesting (=non-trivial?) theorem about ID U A B without further axioms.
Semantically, this is closely analogous to the fact that an
(oo,1)-topos can be defined either by the existence of "object
classifiers" or by the fact that colimits satisfy "descent". The
former is like having univalent universes; the latter is like having
large elims for HITs. Descent is likewise not intrinsic to the notion
of colimit; it expresses a stronger property of the ambient category.
I agree that there are some nice things about separating large elims
from universes. However, I still maintain that large elims for HITs
should be regarded as an aspect of univalence, which merely happens to
be expressible without a universe.
I agree that there are some nice things about separating large elims
from universes. However, I still maintain that large elims for HITs
should be regarded as an aspect of univalence, which merely happens to
be expressible without a universe.
[…]
Semantically, this is closely analogous to the fact that an
(oo,1)-topos can be defined either by the existence of "object
classifiers" or by the fact that colimits satisfy "descent". The
former is like having univalent universes; the latter is like having
large elims for HITs. Descent is likewise not intrinsic to the notion
of colimit; it expresses a stronger property of the ambient category.
On Aug 13, 2014 2:43 AM, "Martin Escardo" <m.es...@cs.bham.ac.uk> wrote:
> The invariance under equivalence is much
> weaker than (2). We know that J is equivalent to transport + the
> contractibility of "singletons" (the Sigma types of paths from a given
> point). But invariance under equivalence is only the transport part.
I think it depends on what you mean by "invariance". It seems to me that J is itself a stronger sort of invariance, which is entirely reasonable to ask for in the case of equivalences.
On Aug 15, 2014 10:37 AM, "Martin Escardo" <m.es...@cs.bham.ac.uk> wrote:
> It seems (but I don't promise without further analysis) that there is
> no problem in defining n-type using equivalence rather than Id U.
Well, you could define the statement "U is an n-type" using equivalence instead of Id U, but then it won't be an instance of the general notion of "n-type" any more, so you won't be proving the same theorem.
>>> email to HomotopyTypeTheory+unsub...@googlegroups.com.
>>> For more options, visit https://groups.google.com/d/optout.
>>
>
> --
> Martin Escardo
> http://www.cs.bham.ac.uk/~mhe
>
> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsub...@googlegroups.com.