Lifting Prop to Type

Stream: new members

[Reed Mullanix]

I'm trying to define the simplex category, but I'm running into an issue with the type of my morphisms:

hom := λ n m, Σ f : fin n → fin m, monotone f

Lean doesn't seem to like the fact that monotone f has type Prop (which is fair). Is there a way to lift this into Type, or should I define a struct or something instead of using a sigma type.

[Scott Morrison]

You'll need plift to lift from Prop to Type, and then possibly ulift as well, if you want to lift to an arbitrary universe.

[Scott Morrison]

See src#category_theory.discrete_category and preorder.small_category.

[Scott Morrison]

You can also just use Σ' for this purpose.

[Scott Morrison]

which allows the second part to be a Prop, but leaves you in Type.

[Scott Morrison]

or use a structure

[Scott Morrison]

Or check in with Johan who has a branch about the simplex category somewhere.

[Reed Mullanix]

Awesome, thanks! I think I'll try to fight my way through this for the practice. I'm moving over from Agda, so still very much getting use to things :)

[Johan Commelin]

@Reed Mullanix Note that the branch sset contains a bunch of stuff on simplicial sets.

[Johan Commelin]

I hope to return to it soonish

[Johan Commelin]

It is my second or third attempt at the matter, and this time I've decided not to use fin n, but arbitrary nonempty finite linear orders.

[Johan Commelin]

I think that's better, because with that approach, you can restrict to a subtype of fin n and it will still live in the category, and things like that.

[Johan Commelin]

The branch contains definitions up to simplicial homology. But it doesn't show that the standard face and degeneracy maps generate the simplex category... that's still something I wanted to do.

[Johan Commelin]

It also has geometric realization of a simplicial set, but not the adjunction.

[Kenny Lau]

{ f : fin n → fin m // monotone f }

[Reed Mullanix]

The Linear Order idea is a good one! That branch looks like its got some great stuff in it, Ill poke around