categorical diamond

Stream: general

[Johan Commelin]

example (i : fin 3) : @quiver.hom (prod (fin 3) (fin 2))
    (@category_theory.category_struct.to_quiver (prod (fin 3) (fin 2))
       (@category_theory.category.to_category_struct (prod (fin 3) (fin 2))
          (@preorder.small_category (prod (fin 3) (fin 2))
             (@prod.preorder (fin 3) (fin 2)
                (@directed_order.to_preorder (fin 3) (@linear_order.to_directed_order (fin 3) (@fin.linear_order 3)))
                (@directed_order.to_preorder (fin 2)
                   (@linear_order.to_directed_order (fin 2) (@fin.linear_order 2)))))))
    (@prod.mk (fin 3) (fin 2) i 0)
    (@prod.mk (fin 3) (fin 2) i 1) =
  @quiver.hom (prod (fin 3) (fin 2))
    (@category_theory.category_struct.to_quiver (prod (fin 3) (fin 2))
       (@category_theory.category.to_category_struct (prod (fin 3) (fin 2))
          (@category_theory.uniform_prod (fin 3)
             (@preorder.small_category (fin 3)
                (@directed_order.to_preorder (fin 3) (@linear_order.to_directed_order (fin 3) (@fin.linear_order 3))))
             (fin 2)
             (@preorder.small_category (fin 2)
                (@directed_order.to_preorder (fin 2)
                   (@linear_order.to_directed_order (fin 2) (@fin.linear_order 2)))))))
    (@prod.mk (fin 3) (fin 2) i 0)
    (@prod.mk (fin 3) (fin 2) i 1) := rfl -- fails

[Johan Commelin]

If we have two preorders P and Q, and we consider P × Q as a category, we can do this in two ways:
(i) first view them as categories, then take the product
(ii) take the product of preorders, then view it as a category.

[Johan Commelin]

These aren't defeq :crying_cat:

[Scott Morrison]

Presumably it comes down to ulift (plift (X \and Y)) is not the same as ulift (plift X) \times ulift (plift Y).