## Stream: maths

### Topic: preorder categories

#### Johan Commelin (Apr 09 2019 at 09:04):

Now that categories live in Prop, should we turn preorder categories into category instead of small_category to get rid of the ulift-plift dance? https://github.com/leanprover-community/mathlib/blob/2f088fc1cb98c6e789f3c61e594e9c85a121d139/src/category_theory/category.lean#L117

#### Scott Morrison (Apr 13 2019 at 13:29):

No, it turns out to be a bad idea. I spent a while using it

#### Scott Morrison (Apr 13 2019 at 13:29):

in fact, the whole generalisation to Sort was a bit dubious

#### Johan Commelin (Apr 13 2019 at 13:30):

Hmm... that's a pity

#### Scott Morrison (Apr 13 2019 at 13:30):

it's _possible_ that there is a good fix, actually

#### Scott Morrison (Apr 13 2019 at 13:31):

the problem was that when morphisms are in Prop, because of proof irrelevance the simplifier won't touch them

#### Scott Morrison (Apr 13 2019 at 13:31):

so sometimes I'd have something I knew was the identity, but couldn't get there by simp

#### Scott Morrison (Apr 13 2019 at 13:31):

and then if I had a functor into a "honest" category, I couldn't show that F.map f was the identity.

#### Johan Commelin (Apr 13 2019 at 13:32):

Hmm... I see. So you would need simp-lemmas specialised to "homs-in-Prop" categories...

#### Scott Morrison (Apr 13 2019 at 13:32):

a possible way to fix it is just to state the lemma that if f : X \hom X is Prop level, then F.map f = eq_to_hom (congr_arg F.obj X)

#### Johan Commelin (Apr 13 2019 at 13:33):

That simplify F.map f for any f : X \hom X to the identity on F.obj X

#### Scott Morrison (Apr 13 2019 at 13:33):

no -- it's important to use eq_to_hom if you don't want eq.rec hell :-)

#### Scott Morrison (Apr 13 2019 at 13:33):

I may have actually tried this. It's too late for me to remember.

#### Scott Morrison (Apr 13 2019 at 13:33):

...

Last updated: May 09 2021 at 09:11 UTC