What would happen using proof as data?

Stream: new members

[Shanghe Chen]

Hi I came accross this kind of werid question while I am learning the coherence theorem of monoidal categories. In usual textbook occasionally we use proof as data. Like the def of a category on "ℕ" that there is a unique arrow from x to y if and only if x ≤ y. I saw that the definition of Category avoids doing this by requiring that arrow can not be Prop. I did an exercise like:

import Mathlib.CategoryTheory.Category.Basic

def le := (by infer_instance: LE ℕ).le

class CategoryWithProofAsArrow (obj : Type u) extends Quiver.{0} obj : Type u where
  /-- The identity morphism on an object. -/
  id : ∀ X : obj, Hom X X
  /-- Composition of morphisms in a category, written `f ≫ g`. -/
  comp : ∀ {X Y Z : obj}, (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)

instance proofAsArrow : CategoryWithProofAsArrow ℕ where
 Hom x y := le x y
 id x := (by simp [le])
 comp f g := (by simp [le] at *; apply Nat.le_trans; repeat assumption)

example {x y : ℕ} (f g: x ⟶ y) : f = g := rfl

what would happen for definition like this? It seems to be an advantage for it: the uniqueness of arrow between two objects is directly from propext. But I don't know the disadvantage though.

[Mitchell Lee]

Allowing the hom types to be propositions would make it much harder to integrate the category theory library with the rest of mathlib. That's because Type u is the standard.

For example, AddCommGroup A requires A : Type u. So if you wanted to later state that ℕ is an additive category, you couldn't do it if the hom types were propositions.

Fortunately, there is already a mechanism for constructing categories whose hom types are subsingleton: docs#Preorder.smallCategory.

[Yaël Dillies]

Mitchell Lee said:

Allowing the hom types to be propositions would make it much harder to integrate the category theory library with the rest of mathlib. That's because Type u is the standard.

This is not quite the reason

[Mitchell Lee]

Okay, bad example because ℕ isn't an additive category, but maybe I can think of a different one

[Shanghe Chen]

Thank you for the information! Yeah I check the link and find it using Ulift. Rather than this way, the free monoidal category uses totally a different approach via quotient and proves the hom types are singletons in free monoidal category and the coherence theorem

[Shanghe Chen]

the original example for me is that I want to see what would happen if fuzzily defined the morphisms of the free monoidal category to be proof of words has same length, i.e, that there is an unique morphsim between two words x and y iff they have the same length, like ((aa)e)a to (((ea)a)a

[Shanghe Chen]

Ulift seems kind of using prop as morphisms, since it turns Prop to a Type u. Maybe it’s not a big issue here.