# -

Assuming that (obj, mor, ==, id, refl, @, then, =@=) is a 2-category
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.
• #### (no subject)

Guy from Seattle team we've been working with showed up today at work; no matter how much I'm generally comfortable working with remote teams (and I…

• #### (no subject)

Sean's back in town --- good fun working with nonremote teammates.

• #### (no subject)

Sean's in town at work, good times.

• Post a new comment

#### Error

Anonymous comments are disabled in this journal

default userpic