Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: Jasper Hugunin <jasperh@cs.washington.edu>
To: HomotopyTypeTheory@googlegroups.com
Subject: [HoTT] A definition of equivalence where the identity is a unit on both sides for composition
Date: Sun, 16 Aug 2020 12:08:32 -0700	[thread overview]
Message-ID: <CAGTS-a9Qo5jTP7bMsHkQGgBp9y46icJ1m1bB0qiSiHUS+JxQGw@mail.gmail.com> (raw)

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

             reply	other threads:[~2020-08-16 19:08 UTC|newest]

Thread overview: 3+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2020-08-16 19:08 Jasper Hugunin [this message]
2020-08-17 13:48 ` [HoTT] " alexr...@gmail.com
2020-08-17 15:59   ` Jasper Hugunin

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=CAGTS-a9Qo5jTP7bMsHkQGgBp9y46icJ1m1bB0qiSiHUS+JxQGw@mail.gmail.com \
    --to=jasperh@cs.washington.edu \
    --cc=HomotopyTypeTheory@googlegroups.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).