Zulip Chat Archive

Stream: maths

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 What do you think about this? (Also in light of #926.)

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

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

Hmm... that's a pity

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

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

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

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

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

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)

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

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

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

...

Last updated: Dec 20 2023 at 11:08 UTC