# Definitions of equivalence satisfying judgmental/strict groupoid laws?

116 views

### Jason Gross

Nov 12, 2014, 2:54:32 AM11/12/14

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

Nov 12, 2014, 11:41:11 AM11/12/14
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

Nov 12, 2014, 11:52:48 AM11/12/14
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

Nov 12, 2014, 11:55:50 AM11/12/14
to Michael Shulman, Alexander Altman, HomotopyT...@googlegroups.com
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.

### Michael Shulman

Nov 12, 2014, 12:07:45 PM11/12/14
to Peter LeFanu Lumsdaine, Alexander Altman, HomotopyT...@googlegroups.com
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

Nov 12, 2014, 12:16:54 PM11/12/14
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

Nov 12, 2014, 12:29:49 PM11/12/14
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

Nov 12, 2014, 3:10:22 PM11/12/14
to Michael Shulman, Alexander Altman, HomotopyT...@googlegroups.com
On Wed, Nov 12, 2014 at 6:07 PM, Michael Shulman 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

Nov 12, 2014, 3:25:19 PM11/12/14
to Peter LeFanu Lumsdaine, Michael Shulman, Alexander Altman, HomotopyT...@googlegroups.com
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

Nov 12, 2014, 3:53:22 PM11/12/14
to Egbert Rijke, Michael Shulman, Alexander Altman, HomotopyT...@googlegroups.com
On Wed, Nov 12, 2014 at 9:25 PM, Egbert Rijke 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

Nov 12, 2014, 4:26:25 PM11/12/14
to Peter LeFanu Lumsdaine, Egbert Rijke, Alexander Altman, HomotopyT...@googlegroups.com
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

Nov 12, 2014, 4:39:47 PM11/12/14
to Michael Shulman, Egbert Rijke, Alexander Altman, HomotopyT...@googlegroups.com
On Wed, Nov 12, 2014 at 10:26 PM, Michael Shulman 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

Nov 12, 2014, 4:51:32 PM11/12/14
to Peter LeFanu Lumsdaine, Egbert Rijke, Alexander Altman, HomotopyT...@googlegroups.com
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.

Nov 13, 2014, 3:51:16 AM11/13/14
to Peter LeFanu Lumsdaine, Thierry Coquand, Prof. Vladimir Voevodsky, Egbert Rijke, Michael Shulman, Alexander Altman, HomotopyT...@googlegroups.com
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

Nov 13, 2014, 4:02:13 AM11/13/14

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

Nov 13, 2014, 4:04:42 AM11/13/14
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

Nov 13, 2014, 4:22:59 AM11/13/14

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

Nov 13, 2014, 1:55:46 PM11/13/14
On Thu, Nov 13, 2014 at 12:04 PM, Vladimir Voevodsky 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.

Nov 13, 2014, 3:59:18 PM11/13/14
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

Aug 16, 2019, 8:14:48 PM8/16/19
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ó

Sep 11, 2019, 9:45:35 PM9/11/19
to Homotopy Type Theory

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