Such a structure is called a *-autonomous category [ Bar79].
A homotopy f® g between paths of the same length n is a function h:[0,n]x[0,1] with h(t,0) = f(t), h(t,1) = g(t), h(0,s) = x and h(n,s) = y. Modify this definition to allow f and g to have different lengths, and in particular so that f;f- and f-;f are homotopic to identities in C, where f-(t) = f(n-t). Define a bi-category of points, paths and homotopies.
Now show that the existence of a homotopy f® g is an equivalence relation, and that its quotient is a groupoid, the fundamental groupoid p1(X) of X.
|
Let V be the three-point poset {no ³ ^ £ yes}. Show that there is no pullback-preserving function por:VxV® V with por(no, no) = no and por(yes, ^) = yes = por(^,yes).