# -

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)

A paper on describing circuits in an agda DSL: http://www.staff.science.uu.nl/~swier004/publications/2015-types-draft.pdf

• #### (no subject)

Going more carefully now through this little tutorial on fpga programming with the iCEstick. It's in spanish, which makes it slightly more…

• #### (no subject)

Some further progress cleaning up the https://xkcd.com/1360/ -esque augean stables that is my hard drive. Tomato chicken I made a couple days ago…

• Post a new comment

#### Error

Anonymous comments are disabled in this journal

default userpic

Your reply will be screened

Your IP address will be recorded

• 0 comments