N_P3Ch15a_Spans

Markdown of literate Haskell program. Program source: /src/CTNotes/P3Ch15a_Spans.lhs

Notes about CTFP Part 3 Chapter 12. Span bicategory

Note about the category of spans described in chapter 15. It provides supporting conceptual code in Haskell. These notes use the concept of pullback which is not directly expressible in Haskell's language (and, probably, lead to undecidable problems).

 {-# LANGUAGE MultiParamTypeClasses
   , ExistentialQuantification
   , FlexibleContexts
   , ScopedTypeVariables 
   #-}

 module CTNotes.P3Ch15a_Spans where

Span bicategory

 data Cell0 a = Cell0 a
 data Cell1 x a b = Cell1 (x -> a) (x -> b)
 data Cell2 x y a b = Cell2 (x -> y)

0-cells are Haskell types.
1-cells are spans consisting of 2 morphisms (legs) from a common object x (support object/apex).
2-cells are morphisms between apex objects that result in commuting diagrams involving legs.

             z
          /  |  \
         /   |   \
        a <- x -> b 

Type Cell1 x a b represents a morphism between Cell a and Cell0 b. Type Cell2 x y a b represents a natural transformation between Cell1 x a b and Cell2 x a b where a and b are the same for both 1-cells. This note is focused on 1-cells.

Cell1-s as morphisms of Cell0-s

Identity
The identity morphism is:

 idm :: Cell1 a a a
 idm = Cell1 id id

Composition
Composition of spans needs the notion of pullback.
To approximate pullbacks in Haskell, I use this type constructor

 data Pullback x y a = forall z . Pullback z (z -> x) (z -> y)

This type represents some type z representing the pullback object and 2 morphisms p1::z -> x and p2::z -> y which complete the pullback construction of given functions f:: x -> a and g:: y -> a.

For sets, pullback of f and g is often defined as a subset of elements in (x,y):
[(xa,ya) | xa <- x, ya <- y, f xa == g ya].
The above definition is consistent with this approach:

 class Subset s a where
   inject :: s -> a

 instance Subset (Pullback x y b) (x,y) where
   inject (Pullback z f1 f2) = (f1 z, f2 z)

In this approach, Pullback of x and y on top of b is viewed as some type z together with injection of z into (x,y).

The composition of 1-cells can be defined in Haskell as:

 comp :: forall x y a b c .  Cell1 y b c -> Cell1 x a b -> Cell1 (Pullback x y b) a c
 (Cell1 g1 g2) `comp`  (Cell1 f1 f2) 
                 = Cell1 h1 h2
                   where 
                      h1 :: Pullback x y b -> a
                      h1 (Pullback z p1 _) =  f1 . p1 $ z
                      h2 :: Pullback x y b -> c
                      h2 (Pullback z _ p2)  = g2 . p2 $ z

Proofs of Category Laws

Notice that other than the type itself, pullback is not used in the above implementation of comp. However, pullbacks are needed in verifying category laws. For the category of spans these laws hold only up to isomorphism.
(In following diagrams vertical arrows are implicitly pointing down.)

Right Identity
Need to show existence of isomorphism:

idm 'comp' Cell1 x a b  ~= Cell1 x a b 

The proof follows directly from the uniqueness of universal construction.

I have the following diagram:

            x
         /id   \f
       x         b 
     /   \f   /id  \
   a        b        b 
   
Cell1 x a b |  idm 
Cell1 _ _ f

Note this diagram satisfies f . id == id . f and provides a valid pullback candidate for f and id. Let z be any other pullback candidate:

            z
         /p1  \p2
       x         b 
         \f   /id  
            b        

It suffices to show that we can factorize h :: z -> x.
Take h = p1. The following diagram commutes proving the factorization.

           z
       /   |   \   
   p1 /    |p1  \ p2
     /     |     \
    /  id  |   f  \
   x  <-   x  ->   b
    \             /
     \ f         / id
      \         /
           b
           

Left Identity follows from similar arguments due to symmetry.

Associativity
Using z = x ×a y to represent following pullback (names of morphisms are ignored in the notation and in this proof).

  z --> y 
  |     |
  |     |
  x --> a      

The proof follows from what is called associativity property of pullbacks: Consider a commutative diagram (in any category)

   a  ---->  b  -----> c
   |         |         |
   |         |         |
   |         |         |
   d  ---->  e  -----> f

Suppose the right-hand inner square is a pullback, then: the square on the left is a pullback if and only if the outer square is. (This means that I can collapse adjacent pullback square diagrams to get a pullback diagram.) (Ref: https://ncatlab.org/nlab/show/pullback Proposition 3, or Borceux categorical algebra handbook vol 1)

Consider this diagram where each square is a pullback:

   r ----> b ×e c  -----> c
   |         |            |
   |         |            |
   |         |            |
 a ×d b -->  b  --------> e
   |         |            
   |         |          
   |         |           
   a  ---->  d      

Composing horizontal arrows we get a pullback

   r ---->   c
   |         |            
   |         |  
   |         |  
 a ×d b -->  e

similarity composing vertical arrows there is a pullback:

   r ----> b ×e c 
   |         |            
   |         |          
   |         |           
   a  ---->  d      

yielding isomorphisms (a ×d b) ×e c -> r and r -> a ×d (b ×e c). Combining these shows associativity up to isomorphism.

Fun Note

Trying to come up with Haskell code for this note I got the following ghc error:

    • My brain just exploded
      I can't handle pattern bindings for existential or GADT data constructors.
      Instead, use a case-expression, or do-notation, to unpack the constructor.