Are there any (known) definitions of equivalence that satisfy some groupoid laws judgmentally? For example, is there a definition of equivalence (maybe with infinitely many data) such that when you take the inverse twice, you get back what you started with, judgmentally? Is there one with strictly associative composition (or where composition is strictly associative if you strictify the associativity of concatenation of paths)? I don't think there can be a definition where p^-1 . p is judgmentally the identity equivalence, for this is not even true on the functions themselves.
-Jason
--
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 HomotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
Nice! Of course, this definition (1) goes up a universe and (2) is a
definition of Equiv without a corresponding definition of IsEquiv.
I'm not sure I understand the statement that it doesn't come with a corresponding notion of isEquiv. A notion of isEquiv should be a family of mere propositions, such that the objects satisfying this condition count as equivalences.
On Wed, Nov 12, 2014 at 12:53 PM, Peter LeFanu Lumsdaine
<p.l.lu...@gmail.com> wrote:
Peter's suggestion (with typos corrected) [and renamed for reference]:
>>> isTrackedByRelEquiv (f:A->B) := {
>>> R : RelationalEquiv A B
>>> g : B -> A;
>>> forall a:A, R a f(a);
>>> forall b:B, R g(b) b
>>> }
seems more plausible to me, although it's not immediately obvious that
this is a proposition. Is there an easy way to see that it is?
The question is about how you interpret this operation for the univalent universe. If there is an interpretation of such an operation then there is a way to define equivalences between types in an involutionary way.
On Thu, Nov 13, 2014 at 12:59 PM Vladimir Voevodsky <vlad...@ias.edu> wrote:
In general no. But their model is essentially syntactic and more or less complete. Or, to be more precise, I would expect it to
be more or less complete.V.
On Nov 13, 2014, at 9:55 PM, Peter LeFanu Lumsdaine <p.l.l...@gmail.com> wrote:
On Thu, Nov 13, 2014 at 12:04 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:The question is about how you interpret this operation for the univalent universe. If there is an interpretation of such an operation then there is a way to define equivalences between types in an involutionary way.I don’t follow why this should be the case. This shows that there is some notion of equivalence *in the model* (i.e. constructed in the meta-theory) which is strictly involutive. But there is no reason that this notion need be definable in the syntax of the object theory, is there?–p.--
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.
--
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.