implies the following equalities of proofs:
(P1 then P2) then P3 === P1 then (P2 then P3)
[vert. comp. is assoc.]
refl then P1 === P1 === P1 then refl
[vert. id.s are neutral for vert. comp.]
=@= (P1 then P2) (P3 then P4) === (=@= P1 P3) then (=@= P2 P4)
[horiz. comp. preserves vert. comp.]
=@= refl refl === refl
[horiz. comp. preserves vert. id.s]
Assuming further that sym is a ``horizontally covariant,
vertically contravariant'' 2-endofunctor leaving
1-cells fixed we get
sym (P1 then P2) === (sym P2) then (sym P1)
[vert. contravar.]
sym refl === refl
[preserves id.s]
sym (=@= P1 P2) === =@= (sym P1) (sym P2)
[horiz. covar.]
and it makes a lot of sense to impose
sym (sym P1) === P1
but I don't know what to call that property
in terms of 2-functors.
Is this notion of equality at all interesting?
Is it (efficiently) decidable?
Might something like this idea capture the
symmetry between prod_l and prod_r proofs?
Ah -- G. M. Kelley in Basic Concepts of Category Theory
(512.86 K29b) calls what sym does a
`duality involution'. It seems that
f o f = id is called the `involutivity' of f.
