Zulip Chat Archive

Stream: new members

Topic: Lifting Prop to Type


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Sep 12 2020 at 04:07):

See src#category_theory.discrete_category and preorder.small_category.

view this post on Zulip Scott Morrison (Sep 12 2020 at 04:09):

You can also just use Σ' for this purpose.

view this post on Zulip Scott Morrison (Sep 12 2020 at 04:10):

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

view this post on Zulip Scott Morrison (Sep 12 2020 at 04:10):

or use a structure

view this post on Zulip Scott Morrison (Sep 12 2020 at 04:10):

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

view this post on Zulip 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 :)

view this post on Zulip Johan Commelin (Sep 12 2020 at 05:37):

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

view this post on Zulip Johan Commelin (Sep 12 2020 at 05:37):

I hope to return to it soonish

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 12 2020 at 05:40):

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

view this post on Zulip Kenny Lau (Sep 12 2020 at 06:42):

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

view this post on Zulip 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