116 views

Skip to first unread message

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

to homotopyt...@googlegroups.com

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

Nov 12, 2014, 11:41:11 AM11/12/14

to HomotopyT...@googlegroups.com

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.

Nov 12, 2014, 11:52:48 AM11/12/14

to Alexander Altman, HomotopyT...@googlegroups.com

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

immediately how to prove that that definition *is* symmetric without

going through one of the others.

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.

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

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.

definition of Equiv without a corresponding definition of IsEquiv.

Nov 12, 2014, 12:16:54 PM11/12/14

to Michael Shulman, HomotopyT...@googlegroups.com

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.

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.

Nov 12, 2014, 12:29:49 PM11/12/14

to Alexander Altman, HomotopyT...@googlegroups.com

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

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

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

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

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

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

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

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

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.

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

to Vladimir Voevodsky, HomotopyT...@googlegroups.com

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

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

to Thierry Coquand, Prof. Vladimir Voevodsky, HomotopyT...@googlegroups.com

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.

of such an operation then there is a way to define equivalences between types in an involutionary way.

V.

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

to Vladimir Voevodsky, HomotopyT...@googlegroups.com

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

Nov 13, 2014, 1:55:46 PM11/13/14

to Vladimir Voevodsky, Thierry Coquand, HomotopyT...@googlegroups.com

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.

Nov 13, 2014, 3:59:18 PM11/13/14

to Peter LeFanu Lumsdaine, Prof. Vladimir Voevodsky, Thierry Coquand, HomotopyT...@googlegroups.com

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.

Aug 16, 2019, 8:14:48 PM8/16/19

to Vladimir Voevodsky, Peter LeFanu Lumsdaine, Thierry Coquand, HomotopyT...@googlegroups.com

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

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

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu