Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [HoTT] A definition of equivalence where the identity is a unit on both sides for composition
@ 2020-08-16 19:08 Jasper Hugunin
  2020-08-17 13:48 ` [HoTT] " alexr...@gmail.com
  0 siblings, 1 reply; 3+ messages in thread
From: Jasper Hugunin @ 2020-08-16 19:08 UTC (permalink / raw)
  To: HomotopyTypeTheory

[-- Attachment #1: Type: text/plain, Size: 3394 bytes --]

I was thinking about various definitions of equivalence, and the various
equations we could ask them to satisfy up to definitional equality. (They
are of course all the same when looking at propositional equality.)

Looking at composition, all the definitions of equivalence I have seen
before satisfy at most one of the two equations id o p = p or p o id = p
(for p : A equiv B and _o_ composition).

By adapting the definition by bi-invertible maps, we can get a definition
of equivalence where both the above equations hold, and additionally we get
definitional associativity (p o q) o r = p o (q o r).

-----

Recall the bi-invertible map definition of equivalence is
A equiv B =
  (f : A -> B) x
  (gl : B -> A) x
  (gr : B -> A) x
  (linv : forall a, gl(f(a)) = a) x
  (rinv : forall b, f(gr(b)) = b)
Then the identity is (id, id, id, refl, refl).

When composing (f1, gl1, gr1, linv1, rinv1) with (f2, gl2, gr2, linv2,
rinv2),
we can take f = f1 o f2, gl = gl2 o gl1, gr = gr2 o gr1, but linv and
rinv require path induction (essentially to compose instantiations of linv1
and linv2). Since path composition in an arbitrary type only satisfies one
of the two unit equations definitionally, I don't believe it is possible to
satisfy both id o p and p o id for this definition.

However, we can modify the definitions of linv and rinv inspired by the
symmetric coinductive definition of equivalence (that A equiv B = (f : A ->
B) x (g : B -> A) x forall a b, (f a = b) equiv (a = g b)).

So we take linv : forall a b, f a = b -> a = gl b, and rinv : forall a b, a
= gr b -> f a = b.

(Notice that (b : B) x (f a = b) and (a : A) x (a = gr b) are contractible,
so this definition is equivalent to the bi-invertible map definition, and
thus a real definition of equivalence.)

Then for the identity, we take linv = rinv = id.
Thus for composition, we can take linv = linv2 o linv1 and rinv = rinv1 o
rinv2, and exploit the fact that the identity function is definitionally a
two-sided unit for function composition.

Q.E.D.

-----

Has anyone seen this definition or other definitions with this property
used before?

This definition does not behave particularly nicely with respect to
inversion. I know a few definitions with definitional involutive inversion,
and most definitions seem to satisfy id^-1 = id, but I don't think I know
any definitions where p^-1 o p = id or p o p^-1 = id.

There is such a wide variety of possible choices with respect to the
definition of equivalence, I am interested in what additional properties we
can ask of it to narrow down the scope of a "good" definition, and what
unavoidable trade offs exist.
Some good properties I am thinking about are:
1) Decomposition into (f : A -> B) x isEquiv f
2) Definitional groupoid equations.
Currently (1) seems to be incompatible with involutive inversion, but as
shown here we can have both (1) and definitional equations for everything
except inversion. Can we be more greedy?

Sincerely,
- Jasper Hugunin

-- 
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+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAGTS-a9Qo5jTP7bMsHkQGgBp9y46icJ1m1bB0qiSiHUS%2BJxQGw%40mail.gmail.com.

[-- Attachment #2: Type: text/html, Size: 4273 bytes --]

^ permalink raw reply	[flat|nested] 3+ messages in thread

* [HoTT] Re: A definition of equivalence where the identity is a unit on both sides for composition
  2020-08-16 19:08 [HoTT] A definition of equivalence where the identity is a unit on both sides for composition Jasper Hugunin
@ 2020-08-17 13:48 ` alexr...@gmail.com
  2020-08-17 15:59   ` Jasper Hugunin
  0 siblings, 1 reply; 3+ messages in thread
From: alexr...@gmail.com @ 2020-08-17 13:48 UTC (permalink / raw)
  To: Homotopy Type Theory


[-- Attachment #1.1: Type: text/plain, Size: 5184 bytes --]

Hi Jasper,

I have also thought about these sort of structures a bit, and in fact this 
sort of "trick" of decomposing something of passing in an equality also 
works in a variety of situations where composition involves transitivity of 
equality. For example, you might be interested in Martin Escardo's version 
of this for equality <https://www.cs.bham.ac.uk/~mhe/yoneda/yoneda.html> 
which contains a fair bit of discussion on the topic. I have also done some 
work on this sort of idea related to groups which can be found here 
<https://alexarice.github.io/posts/sgtuf/Strict-Group-Theory-UF.html> and 
submitted a pull request to agda standard library with a similar idea to 
this for quasi-inverses <https://github.com/agda/agda-stdlib/pull/1156>. 

With respect to the questions at the end, I'm afraid I am not aware of any 
definition for which inverses are strict and I expect that (2) (at least in 
it's full generality) is not possible as this would imply that 
\infty-groupoids are equivalent to strict \infty-groupoids. For involution 
you could perhaps do a similar trick that is done in category theory 
libraries like agda-categories where you store the data for both 
directions. More precisely, if we let your definition be called biEquiv 
then you could let

A involutiveBiEquiv B = A biEquiv B x B biEquiv A

and then let inverting be given by swapping the order of the product. I 
believe this should maintain the nice compositional properties of biEquiv 
and adds involutive inverses for "free".

Hope some of this was useful/interesting.
Alex

On Sunday, 16 August 2020 at 20:08:47 UTC+1 jas...@cs.washington.edu wrote:

> I was thinking about various definitions of equivalence, and the various 
> equations we could ask them to satisfy up to definitional equality. (They 
> are of course all the same when looking at propositional equality.)
>
> Looking at composition, all the definitions of equivalence I have seen 
> before satisfy at most one of the two equations id o p = p or p o id = p 
> (for p : A equiv B and _o_ composition).
>
> By adapting the definition by bi-invertible maps, we can get a definition 
> of equivalence where both the above equations hold, and additionally we get 
> definitional associativity (p o q) o r = p o (q o r).
>
> -----
>
> Recall the bi-invertible map definition of equivalence is
> A equiv B =
>   (f : A -> B) x
>   (gl : B -> A) x
>   (gr : B -> A) x
>   (linv : forall a, gl(f(a)) = a) x
>   (rinv : forall b, f(gr(b)) = b)
> Then the identity is (id, id, id, refl, refl).
>
> When composing (f1, gl1, gr1, linv1, rinv1) with (f2, gl2, gr2, linv2, 
> rinv2),
> we can take f = f1 o f2, gl = gl2 o gl1, gr = gr2 o gr1, but linv and 
> rinv require path induction (essentially to compose instantiations of linv1 
> and linv2). Since path composition in an arbitrary type only satisfies one 
> of the two unit equations definitionally, I don't believe it is possible to 
> satisfy both id o p and p o id for this definition.
>
> However, we can modify the definitions of linv and rinv inspired by the 
> symmetric coinductive definition of equivalence (that A equiv B = (f : A -> 
> B) x (g : B -> A) x forall a b, (f a = b) equiv (a = g b)).
>
> So we take linv : forall a b, f a = b -> a = gl b, and rinv : forall a b, 
> a = gr b -> f a = b.
>
> (Notice that (b : B) x (f a = b) and (a : A) x (a = gr b) are 
> contractible, so this definition is equivalent to the bi-invertible map 
> definition, and thus a real definition of equivalence.)
>
> Then for the identity, we take linv = rinv = id.
> Thus for composition, we can take linv = linv2 o linv1 and rinv = rinv1 o 
> rinv2, and exploit the fact that the identity function is definitionally a 
> two-sided unit for function composition.
>
> Q.E.D.
>
> -----
>
> Has anyone seen this definition or other definitions with this property 
> used before?
>
> This definition does not behave particularly nicely with respect to 
> inversion. I know a few definitions with definitional involutive inversion, 
> and most definitions seem to satisfy id^-1 = id, but I don't think I know 
> any definitions where p^-1 o p = id or p o p^-1 = id.
>
> There is such a wide variety of possible choices with respect to the 
> definition of equivalence, I am interested in what additional properties we 
> can ask of it to narrow down the scope of a "good" definition, and what 
> unavoidable trade offs exist.
> Some good properties I am thinking about are:
> 1) Decomposition into (f : A -> B) x isEquiv f
> 2) Definitional groupoid equations.
> Currently (1) seems to be incompatible with involutive inversion, but as 
> shown here we can have both (1) and definitional equations for everything 
> except inversion. Can we be more greedy?
>
> Sincerely,
> - Jasper Hugunin
>

-- 
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+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/02e9d6bd-3ce7-485a-a6e4-cb29ca02abecn%40googlegroups.com.

[-- Attachment #1.2: Type: text/html, Size: 6273 bytes --]

^ permalink raw reply	[flat|nested] 3+ messages in thread

* Re: [HoTT] Re: A definition of equivalence where the identity is a unit on both sides for composition
  2020-08-17 13:48 ` [HoTT] " alexr...@gmail.com
@ 2020-08-17 15:59   ` Jasper Hugunin
  0 siblings, 0 replies; 3+ messages in thread
From: Jasper Hugunin @ 2020-08-17 15:59 UTC (permalink / raw)
  To: Homotopy Type Theory

[-- Attachment #1: Type: text/plain, Size: 6884 bytes --]

Hi Alex,

Thanks, that is all really cool stuff! It's neat that you can do a similar
thing for equality, I hadn't thought that was possible, though it seems
obvious to me when spelled out.
I actually started off learning Coq trying to formalize an undergraduate
group theory class, and got sidetracked by various ways of making
associativity less annoying. I was exploring reflexive decision procedures,
but it's wonderful to see other approaches to this problem.

With regards to your proposed definition of A involutiveBiEquiv B, I don't
believe that it is a true definition of equivalence, since biEquiv is not a
mere proposition. The definitions with strictly involutive inversion I have
seen generally introduce a type in the middle, so A involutiveEquiv B = (C
: Type) x (C equiv A) x (C equiv B), which under univalence is equivalent
to equiv but can only strictly satisfy one of the two unit equations for
composition.

Sincerely,
- Jasper Hugunin

On Mon, Aug 17, 2020 at 6:48 AM alexr...@gmail.com <alexrice73@gmail.com>
wrote:

> Hi Jasper,
>
> I have also thought about these sort of structures a bit, and in fact this
> sort of "trick" of decomposing something of passing in an equality also
> works in a variety of situations where composition involves transitivity of
> equality. For example, you might be interested in Martin Escardo's
> version of this for equality
> <https://www.cs.bham.ac.uk/~mhe/yoneda/yoneda.html> which contains a fair
> bit of discussion on the topic. I have also done some work on this sort of
> idea related to groups which can be found here
> <https://alexarice.github.io/posts/sgtuf/Strict-Group-Theory-UF.html> and
> submitted a pull request to agda standard library with a similar idea to
> this for quasi-inverses <https://github.com/agda/agda-stdlib/pull/1156>.
>
> With respect to the questions at the end, I'm afraid I am not aware of any
> definition for which inverses are strict and I expect that (2) (at least in
> it's full generality) is not possible as this would imply that
> \infty-groupoids are equivalent to strict \infty-groupoids. For involution
> you could perhaps do a similar trick that is done in category theory
> libraries like agda-categories where you store the data for both
> directions. More precisely, if we let your definition be called biEquiv
> then you could let
>
> A involutiveBiEquiv B = A biEquiv B x B biEquiv A
>
> and then let inverting be given by swapping the order of the product. I
> believe this should maintain the nice compositional properties of biEquiv
> and adds involutive inverses for "free".
>
> Hope some of this was useful/interesting.
> Alex
>
> On Sunday, 16 August 2020 at 20:08:47 UTC+1 jas...@cs.washington.edu
> wrote:
>
>> I was thinking about various definitions of equivalence, and the various
>> equations we could ask them to satisfy up to definitional equality. (They
>> are of course all the same when looking at propositional equality.)
>>
>> Looking at composition, all the definitions of equivalence I have seen
>> before satisfy at most one of the two equations id o p = p or p o id = p
>> (for p : A equiv B and _o_ composition).
>>
>> By adapting the definition by bi-invertible maps, we can get a definition
>> of equivalence where both the above equations hold, and additionally we get
>> definitional associativity (p o q) o r = p o (q o r).
>>
>> -----
>>
>> Recall the bi-invertible map definition of equivalence is
>> A equiv B =
>>   (f : A -> B) x
>>   (gl : B -> A) x
>>   (gr : B -> A) x
>>   (linv : forall a, gl(f(a)) = a) x
>>   (rinv : forall b, f(gr(b)) = b)
>> Then the identity is (id, id, id, refl, refl).
>>
>> When composing (f1, gl1, gr1, linv1, rinv1) with (f2, gl2, gr2, linv2,
>> rinv2),
>> we can take f = f1 o f2, gl = gl2 o gl1, gr = gr2 o gr1, but linv and
>> rinv require path induction (essentially to compose instantiations of linv1
>> and linv2). Since path composition in an arbitrary type only satisfies one
>> of the two unit equations definitionally, I don't believe it is possible to
>> satisfy both id o p and p o id for this definition.
>>
>> However, we can modify the definitions of linv and rinv inspired by the
>> symmetric coinductive definition of equivalence (that A equiv B = (f : A ->
>> B) x (g : B -> A) x forall a b, (f a = b) equiv (a = g b)).
>>
>> So we take linv : forall a b, f a = b -> a = gl b, and rinv : forall a b,
>> a = gr b -> f a = b.
>>
>> (Notice that (b : B) x (f a = b) and (a : A) x (a = gr b) are
>> contractible, so this definition is equivalent to the bi-invertible map
>> definition, and thus a real definition of equivalence.)
>>
>> Then for the identity, we take linv = rinv = id.
>> Thus for composition, we can take linv = linv2 o linv1 and rinv = rinv1 o
>> rinv2, and exploit the fact that the identity function is definitionally a
>> two-sided unit for function composition.
>>
>> Q.E.D.
>>
>> -----
>>
>> Has anyone seen this definition or other definitions with this property
>> used before?
>>
>> This definition does not behave particularly nicely with respect to
>> inversion. I know a few definitions with definitional involutive inversion,
>> and most definitions seem to satisfy id^-1 = id, but I don't think I know
>> any definitions where p^-1 o p = id or p o p^-1 = id.
>>
>> There is such a wide variety of possible choices with respect to the
>> definition of equivalence, I am interested in what additional properties we
>> can ask of it to narrow down the scope of a "good" definition, and what
>> unavoidable trade offs exist.
>> Some good properties I am thinking about are:
>> 1) Decomposition into (f : A -> B) x isEquiv f
>> 2) Definitional groupoid equations.
>> Currently (1) seems to be incompatible with involutive inversion, but as
>> shown here we can have both (1) and definitional equations for everything
>> except inversion. Can we be more greedy?
>>
>> Sincerely,
>> - Jasper Hugunin
>>
> --
> 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+unsubscribe@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/HomotopyTypeTheory/02e9d6bd-3ce7-485a-a6e4-cb29ca02abecn%40googlegroups.com
> <https://groups.google.com/d/msgid/HomotopyTypeTheory/02e9d6bd-3ce7-485a-a6e4-cb29ca02abecn%40googlegroups.com?utm_medium=email&utm_source=footer>
> .
>

-- 
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+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAGTS-a8Ev95e9eop-DSPgDD6e_tCbQJyxfG-qUt15HYgpZ-hgA%40mail.gmail.com.

[-- Attachment #2: Type: text/html, Size: 8604 bytes --]

^ permalink raw reply	[flat|nested] 3+ messages in thread

end of thread, other threads:[~2020-08-17 15:59 UTC | newest]

Thread overview: 3+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2020-08-16 19:08 [HoTT] A definition of equivalence where the identity is a unit on both sides for composition Jasper Hugunin
2020-08-17 13:48 ` [HoTT] " alexr...@gmail.com
2020-08-17 15:59   ` Jasper Hugunin

Discussion of Homotopy Type Theory and Univalent Foundations

This inbox may be cloned and mirrored by anyone:

	git clone --mirror http://inbox.vuxu.org/hott

	# If you have public-inbox 1.1+ installed, you may
	# initialize and index your mirror using the following commands:
	public-inbox-init -V1 hott hott/ http://inbox.vuxu.org/hott \
		homotopytypetheory@googlegroups.com
	public-inbox-index hott

Example config snippet for mirrors.
Newsgroup available over NNTP:
	nntp://inbox.vuxu.org/vuxu.archive.hott


AGPL code for this site: git clone https://public-inbox.org/public-inbox.git