Definitions of equivalence satisfying judgmental/strict groupoid laws?

[Jason Gross]

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

[Alexander Altman]

The propositional truncation of quasi-inverses is a valid definition of equivalences (albeit one that relies on HITs), and I believe it has judgemental symmetry.

[Michael Shulman]

On Wed, Nov 12, 2014 at 8:41 AM, Alexander Altman
<alexand...@me.com> wrote:
> The propositional truncation of quasi-inverses is a valid definition of equivalences (albeit one that relies on HITs), and I believe it has judgemental symmetry.

Why do you say it has judgmental symmetry? I don't even see
immediately how to prove that that definition *is* symmetric without
going through one of the others.

[Peter LeFanu Lumsdaine]

The “relational” definition is judgementally symmetric if one has definitional eta for functions and for sums/records, if I’m not mistaken:

- a “relational equivalence” from A to B consists of a function E : A -> B -> Type, such that for each a:A, the type { b:B & E a b } is contractible, and similarly, so is the type { a:A & E a b} for each b:B.

–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 HomotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Michael Shulman]

Nice! Of course, this definition (1) goes up a universe and (2) is a
definition of Equiv without a corresponding definition of IsEquiv.

[Alexander Altman]

In rough Agda-like syntax:



record QInv (A B : Type) : Type where
inductive
constructor qinv
field
f : A -> B
g : B -> A
f&g-id : (x : B) -> f (g x) == x
g&f-id : (y : A) -> g (f y) == y

Equiv : Type -> Type -> Type
Equiv A B = || QInv A B ||

sym : {A B : Type} -> Equiv A B -> Equiv B A
sym | qinv f g fg-id gf-id | = | qinv g f gf-id fg-id |

sym&sym-id : {A B : Type} (e : Equiv A B) -> sym (sym e) == e
sym&sym-id _ = refl

> --
> You received this message because you are subscribed to a topic in the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this topic, visit https://groups.google.com/d/topic/HomotopyTypeTheory/FfiZj1vrkmQ/unsubscribe.
> To unsubscribe from this group and all its topics, send an email to HomotopyTypeThe...@googlegroups.com.

[Michael Shulman]

But the propositional truncation of "the type of functions equipped
with quasi-inverses" is not a definition of equivalence: the type of
equivalences between A and B should not be a proposition. The
definition that you can get in this way is a definition of IsEquiv(f)
by truncating "the type of quasi-inverses" of a given function f; to
get Equiv(A,B) you then have to sigma that up over f.

On Wed, Nov 12, 2014 at 9:16 AM, Alexander Altman

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

[Peter LeFanu Lumsdaine]

On Wed, Nov 12, 2014 at 6:07 PM, Michael Shulman <shu...@sandiego.edu> wrote:

Nice!  Of course, this definition (1) goes up a universe and (2) is a
definition of Equiv without a corresponding definition of IsEquiv.

Indeed, yes!  It can be improved to a definition of isEquiv while remaining judgementally symmetric, though it becomes very cumbersome indeed in the process:

isEquiv (f:A->B) := { 

   R : RelationalEquiv A B

   g : B -> A;

   forall x:A, R a f(a);

   forall y:B, R g(b) g

}

 

[excuse non-valid syntax]

[Egbert Rijke]

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. The condition

Relisequiv(R) := (forall b, isContr {a | R a b}) x (forall a, isContr {b | R a b})

meets these requirements and should count as a notion of isEquiv for relations from A to B. If you rather want to see isEquiv as a family of mere propositions over functions from A to B, then you could consider the function

functionsToRelations : (A -> B) -> A -> B -> Type

and require, as Peter now also suggested above, that

Relisequiv(functionsToRelations(f))

on functions f : A -> B. (It's not so cumbersome.)

With kind regards,

Egbert

[Peter LeFanu Lumsdaine]

On Wed, Nov 12, 2014 at 9:25 PM, Egbert Rijke <e.m....@gmail.com> wrote:

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.

As I took it, the desideratum here was that isEquiv should be a predicate on A -> B, equivalent to the usual definition of isEquiv, such that Equiv := { f : A -> B & isEquiv f } gives a judgementally symmetric definition of equivalence.

–p.

[Michael Shulman]

On Wed, Nov 12, 2014 at 12:53 PM, Peter LeFanu Lumsdaine
<p.l.lu...@gmail.com> wrote:
> As I took it, the desideratum here was that isEquiv should be a predicate on
> A -> B, equivalent to the usual definition of isEquiv, such that Equiv := {
> f : A -> B & isEquiv f } gives a judgementally symmetric definition of
> equivalence.

Yes, that's what I was wondering about, although Jason's original
question didn't specify this. The suggestion
Relisequiv(functionsToRelations(f)) does not, as far as I can see,
have a judgmentally involutive symmetry (which is a more precise way
to say what we're talking about that "judgmentally symmetric"), since
when you make it into Relisequiv(functionsToRelations(f^-1)) you have
to change the underling relation. Peter's suggestion (with typos
corrected):

>>> isEquiv (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?

[Peter LeFanu Lumsdaine]

On Wed, Nov 12, 2014 at 10:26 PM, Michael Shulman <shu...@sandiego.edu> wrote:

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?

If you accept that “RelationalEquiv” together with the map extracting a function from it is a correct definition of equivalence, then yes.  The forgetful map from {R,f,g,α,β} as above to just R is an equivalence (since the space of pairs {f,α} is contractible, likewise {g,β}).  So { f & isTrackedByRelEquiv f } is a correct definition of equivalence, under the map that extracts a function from its relation.  But that function is equal to f; so { f & isTrackedByRelEquiv(f) }, with the first projection to f, is again correct; i.e. isTrackedByRelEquiv is correct.

–p.

[Michael Shulman]

On Wed, Nov 12, 2014 at 1:39 PM, Peter LeFanu Lumsdaine
<p.l.lu...@gmail.com> wrote:
> If you accept that “RelationalEquiv” together with the map extracting a
> function from it is a correct definition of equivalence, then yes. The
> forgetful map from {R,f,g,α,β} as above to just R is an equivalence (since
> the space of pairs {f,α} is contractible, likewise {g,β}). So { f &
> isTrackedByRelEquiv f } is a correct definition of equivalence, under the
> map that extracts a function from its relation. But that function is equal
> to f; so { f & isTrackedByRelEquiv(f) }, with the first projection to f, is
> again correct; i.e. isTrackedByRelEquiv is correct.

Nice, thanks. Maybe this could be recorded in the solution to
Exercise 4.2 in exercise_solutions.tex in the book repository? The
proof given there doesn't mention this symmetric version of IsEquiv,
although it comes close to it.

[Vladimir Voevodsky]

Thierry  must have a judgementally symmetric definition of equivalence since in his new version of cubical sets 

there is an inversion of paths that is a strict involution.

V.

[Thierry Coquand]

We add an operation

1 - i

on names/dimensions, such that 1 - (1 -i) = i.
This provides a direct interpretation of

inv : Id A a0 a1 -> Id A a1 a0

inv p = <i> p @ (1-i)

where <i> is name abstraction and @ application of a path to a name (using notations
from nominal sets)
This operation satisfies then in a judgmental way (using eta-equalities)

inv (inv p) = p

Thierry

[Vladimir Voevodsky]

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.

V.

[Thierry Coquand]

A line A in the universe in the direction i is given by a presheaf over

C^{opp}/ I with I = {i}

where C is the base category (where objects are finite sets
of symbols) and together with Kan operations.


Concretely A is given by a family of sets A_f indexed by f : I -> J
with restriction operations A_f -> A_{fg} if g : J -> K and Kan operations
(which are given on each A_f and satisfy some compatibility conditions).

We can think of it as a type A(i) depending on the name i.

In general, if we have a map f : I -> J, we can define its restriction
Af presheaf over C^{opp}/J; we take Af_g = A_{fg}.

This satisfies (Af) g = A (fg) and A1 = A.

The special case where f is the map I -> I, i |--> 1-i gives us
the operation of changing direction. Intuitively, starting from A(i), we get A(1-i).

We then have (Af) f = A(ff) = A1 = A.

Thierry

[Peter LeFanu Lumsdaine]

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. 

[Vladimir Voevodsky]

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.

[Jason Gross]

Resurrecting this thread from many years ago, because I was thinking about it again recently, it seems to me that although { f & isTrackedByRelEquiv(f) } satisfies the rule sym (sym e) = e judgmentally, it doesn't satisfy the rule that sym id = id judgmentally.  (In particular, I am not sure what relational equivalence to use for the identity equivalence which does not change judgmentally when I flip the order of its arguments.)  Is there a version of equivalence which simultaneously satisfies that the inverse of the identity is judgmentally the identity, and that inverting an equivalence twice judgmentally gives you what you started with?

-Jason

[Martín Hötzel Escardó]

On 17/08/2019 01:14, Jason Gross wrote:

> Resurrecting this thread from many years ago, because I was thinking

> about it again recently, it seems to me that although { f &

> isTrackedByRelEquiv(f) } satisfies the rule sym (sym e) = e

> judgmentally, it doesn't satisfy the rule that sym id = id

> judgmentally.  (In particular, I am not sure what relational equivalence

> to use for the identity equivalence which does not change judgmentally

> when I flip the order of its arguments.)  Is there a version of

> equivalence which simultaneously satisfies that the inverse of the

> identity is judgmentally the identity, and that inverting an equivalence

> twice judgmentally gives you what you started with?

>

> -Jason

I am not sure this answer will be of the kind you are expecting.

First I will consider the identity type and then the equivalence type

using the same idea.

I will use "=" for definitional equality.

(1) If you have some identity type (_≡_, refl , J) with

    _≡_ : {X : 𝓤} → X → X → 𝓤

    refl : {X : 𝓤 } (x : X) → x ≣ x

    J : (X : 𝓤) (A : (x y : X) → x ≡ y → 𝓤)

     → ((x : X) → A x x (refl x))

     → (x y : X) (p : x ≡ y) → A x y p

then you can define another identity type (_≡'_ , refl' , J') by

    x ≡' y = Σ (z : X), (z ≡ x) × (z ≡ y)

(which is equivalent to the diagonal fiber of (x,y) and also to x ≡ y

(both in pure MLTT))

    refl' x = x , refl x , refl x

    J' X A f x y (z , p , q) = γ z x p y q

     where

      φ :  (x y : X) (q : x ≡ y) → A x y (x , refl x , q)

      φ = J X (λ x y q → A x y (x , refl x , q)) f

      γ : (z x : X) (p : z ≡ x) (y : X) (q : z ≡ y) → A x y (z , p , q)

      γ = J X (λ z x p → (y : X) (q : z ≡ y) → A x y (z , p , q)) φ

so that

    J' X A f x x (refl' x) = f x

definitionally using the original J's computation rule.

For this new identity type, we can define

    ≡'-sym : {X : 𝓤 ̇ } {x y : X} → x ≡' y → y ≡' x

    ≡'-sym (a , p , q) = (a , q , p)

so that

   ≡'-sym (refl' x) = refl' x

and

  ≡'-sym (≡'-sym p') = p',

both definitionally.

(2) Similarly we can define an equivalence type _≃'_ from an equivalence type _≃_ by

    X ≃' Y = Σ (Z : 𝓤), (Z ≃ X) × (Z ≃ X)

with the analogous identity equivalence and symmetrization operation

so that the definitional equalities you want hold.

This is related to the relational definition of equivalence as

follows. The type

   X × Y → 𝓤

of type-valued relations is in canonical bijection with the "slice type"

  Σ (Z : 𝓤), Z → X × Y

by a well-known construction, and in turn to

  Σ (Z : 𝓤), (Z → X) × (Z → Y).

When you restrict to relations R such that for all x:X and y:Y the types

  Σ (x : X), R x y

and

  Σ (y : Y), R x y

are contractible, the type Σ (Z : 𝓤), (Z → X) × (Z → Y) gets restricted to

  Σ (Z : 𝓤), (Z ≃ X) × (Z ≃ X)

by the canonical equivalence

 (X × Y → 𝓤) ≃ Σ (Z : 𝓤), (Z → X) × (Z → Y).

(3) If you want composition of identifications to be definitionally

associative with refl definitionally neutral on both sides, you can

consider the alternative identity type defined by

   x ≡'' y  = (z : X) → (z ≡ x) → (z ≡ y)

which is again equivalent to the original identity type x ≡ y (which

amounts to Yoneda),

   refl'' x = (z : X) → λ (p : x ≡ z) , p

because composition of identifications is given by function

composition, which is definitionally associative with the identity

function as its definitionally neutral element (assuming the η rule).

  (Exercise: write down J''.)

(4) I don't know how to get the definitional equalities of (1) and (3)

together by a suitable modification of the identity type. The

constructions (1) and (3) are kind of dual.

Martin

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.

For more options, visit https://groups.google.com/d/optout.

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