## Stream: new members

### Topic: Directed/filtered categories

#### Calle Sönne (Jun 13 2019 at 19:17):

Is directed/filtered categories in mathlib? Cant seem to find it in the category theory folder

#### Johan Commelin (Jun 13 2019 at 19:18):

Nope, not yet. I think @Reid Barton has some stuff in his homotopy theory repo

#### Scott Morrison (Jun 13 2019 at 23:12):

I think this would be a great project!

#### Reid Barton (Jun 16 2019 at 01:12):

@Calle Sönne what did you want to use them for?

#### Calle Sönne (Jun 18 2019 at 15:18):

Nothing much really, I was just curious as to how/if they were defined in lean

#### Reid Barton (Jun 18 2019 at 15:36):

@Calle Sönne One definition is at https://github.com/leanprover-community/mathlib/blob/filtered-colimits-2/src/category_theory/filtered.lean. That branch also has some facts about filtered colimits of sets starting at https://github.com/leanprover-community/mathlib/blob/filtered-colimits-2/src/category_theory/limits/types.lean#L100.

#### Reid Barton (Jun 18 2019 at 15:37):

The main question is whether the notion of being filtered should be a Prop (as I made it there), a subsingleton (to maintain constructivity, while still being faithful to the fact that being filtered is a property in math, not additional structure), or really encode a choice of cocones on each relevant thing, so that the same category could have multiple distinct filtered structures.

#### Reid Barton (Jun 18 2019 at 15:37):

Or perhaps more than one of these turns out to be useful

#### Calle Sönne (Jun 18 2019 at 16:24):

Thank you!

(cocone_objs : ∀ (X Y : C), ∃ Z (f : X ⟶ Z) (g : Y ⟶ Z), true)


@Ken Lee this is a nice way to do the "filtered" criterion

#### Calle Sönne (Jun 18 2019 at 16:26):

Me and @Ken Lee tried to define it ourselves, and ended up defining it as a category with additional structure (not sure if that is what you mean by subsingleton), what would be the main difference between that and prop? To me as a math student they seem to be the "same".

#### Reid Barton (Jun 18 2019 at 16:28):

To make it a subsingleton you would use trunc of a sigma type in place of an exists. Or make a structure which contains all the choices and take a trunc of the whole thing.

#### Chris Hughes (Jun 18 2019 at 16:31):

A good example of a subsingleton that isn't a prop is fintype

class fintype (α : Type*) :=
(elems : finset α)
(complete : ∀ x : α, x ∈ elems)


The difference is that with this definition I can compute using the finset in question. For example #eval fintype.elems bool returns {ff, tt}, which I couldn't do with a mere proof that such a finset existed.

#### Reid Barton (Jun 18 2019 at 16:34):

Right, and the advantage of a Prop is that you never have to worry about having two different (as in non-definitionally equal) values of the Prop, or something else depending on the proof of that Prop.

#### Calle Sönne (Jun 18 2019 at 16:35):

To make it a subsingleton you would use trunc of a sigma type in place of an exists. Or make a structure which contains all the choices and take a trunc of the whole thing.

What do you mean by trunc?

#### Chris Hughes (Jun 18 2019 at 16:37):

trunc is quotient by the always true relation. This is a computable version of nonempty. It maintains some computability since you can turn any constant computable function X -> Y into a function trunc X -> Y computably.

#### Kevin Buzzard (Jun 18 2019 at 16:40):

@Calle Sönne as you may well know, in Lean all proofs of P are the same. So if P : Prop and then h1 : P and h2 : P then we will have h1 = h2 (and the proof will be rfl). However there are other types which have exactly one term, and then it might be a theorem that two terms of that type are equal rather than being true by definition. And furthermore the terms might somehow store data, whereas a proof in Lean is checked by the kernel and then instantly forgotten about (Lean basically just puts a tick by the proposition to say "this has been proved"). A subsingleton is a type T for which you can prove that if a : T and b : T then a = b. Examples are propositions, but there are other examples too.

#### Calle Sönne (Jun 18 2019 at 16:47):

So fintype, as @Chris Hughes defined it, is a subsingleton since any two finite sets that contains exactly all terms of alpha are equal?

Yes.

#### Ken Lee (Jun 18 2019 at 17:11):

wow, the type of cocone_objs... feels like cheating :joy:

#### Reid Barton (Jun 18 2019 at 17:16):

This exists ... ..., true is a bit silly but I find it's often easier and clearer than alternatives

#### Scott Morrison (Jun 18 2019 at 21:55):

my feeling is that it's best to have filtered_structure, which unashamedly contains the data of a cone for each pair, etc, and then have a filtered typeclass which is just trunc filtered_structure.

#### Scott Morrison (Jun 18 2019 at 21:55):

I'm not so keen on the intermediate solution where each individual field of filtered is either an existential statement or truncd data.

#### Scott Morrison (Jun 18 2019 at 21:56):

It's really a question of where you want to put the proof obligations of showing your construction didn't depend on the filtered structure.

#### Scott Morrison (Jun 18 2019 at 21:56):

You either have to do it every time you use a cone or equaliser, or once after a multi-step construction that uses several cones/equalisers.

#### Scott Morrison (Jun 18 2019 at 21:57):

(The first alternative is what you get if each field of filtereed is an existential or trunc. The second alternative is what you get if you trunc the entire structure.)

#### Scott Morrison (Jun 18 2019 at 21:58):

My limited experience using filtered was that the second alternative was more pleasant to use --- and it's the sort of argument that feels like you should be able to automate away, so it's nice if it's all quarantined in one place.

Last updated: May 10 2021 at 00:31 UTC