# Zulip Chat Archive

## 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?

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

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 `trunc`

d 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