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