## Stream: new members

### Topic: Lifting Prop to Type

#### Reed Mullanix (Sep 12 2020 at 03:49):

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 (Sep 12 2020 at 04:06):

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 (Sep 12 2020 at 04:09):

You can also just use Σ' for this purpose.

#### Scott Morrison (Sep 12 2020 at 04:10):

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

#### Scott Morrison (Sep 12 2020 at 04:10):

or use a structure

#### Scott Morrison (Sep 12 2020 at 04:10):

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

#### Reed Mullanix (Sep 12 2020 at 04:15):

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 (Sep 12 2020 at 05:37):

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

#### Johan Commelin (Sep 12 2020 at 05:38):

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 (Sep 12 2020 at 05:38):

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 (Sep 12 2020 at 05:39):

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 (Sep 12 2020 at 05:40):

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

#### Kenny Lau (Sep 12 2020 at 06:42):

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

#### Reed Mullanix (Sep 12 2020 at 14:12):

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

Last updated: May 09 2021 at 18:17 UTC