# Zulip Chat Archive

## Stream: new members

### Topic: Typeclasses on categories, syntax issues

#### Saul Glasman (Oct 24 2020 at 14:06):

Hi,

I'm trying to build up the definition of a model category via some weaker structures, but trying to compose typeclasses here I'm hitting a syntax error I don't understand, and I suspect I've made an elementary mistake. My file is:

```
import category_theory.fully_faithful
universes u v
open category_theory
namespace category_theory.model
variables (C: Type u) [category.{v} C]
class subcategory (D: Type u) [category.{v} D] :=
(inc: D ⥤ C)
(inc_faithful: faithful inc)
class relative_category (D: Type u) [category.{v} D] extends (subcategory D) :=
(inc_wide: function.surjective inc.obj)
end category_theory.model
```

But lean doesn't seem to like `extends (subcategory D)`

- I get the error

```
type expected at
subcategory D
term has type
Π (D : Type u) [_inst_2 : category D], Type (max u v)
```

What do I have wrong here? I should probably ask this too: what's the "Π" that I often see appearing in type expressions?

#### Kevin Buzzard (Oct 24 2020 at 14:12):

If you hover over `subcategory`

you'll see it has type `Π (C : Type u) [_inst_1 : category C] (D : Type u) [_inst_2 : category D], Type (max u v)`

. Pi is just "for all", if you like. `subcategory`

is expecting four inputs here, namely C, the structure of a category on C, and then D and the structure of a category on D. Two are in square brackets, meaning that those inputs will be supplied by Lean's type class system. But the other two are in round brackets which means that the user is expected to supply them. In particular `subcategory D`

is still a function -- it's expecting another input. You probably want `subcategory C D`

, although looking at other subthings like `subring`

it seems that you might want to take a different approach and make D a field of the class rather than an input (I am not very good with classes, all I know is that there are lots of pitfalls).

#### Kevin Buzzard (Oct 24 2020 at 14:16):

What's going on with the Pi is that Lean has something called "dependent functions", which are functions from a type X to...well, the type of the output depends on the term being input! Here's an example very familiar to mathematicians. If we have infinitely many true-false statements $P(0)$, $P(1)$, $P(2)\ldots$ and we want to construct proofs of them all, then we need a function which takes as input a natural $n$ and spits out a proof of $P(n)$. If you think about it, this is slightly weirder than a function, because in Lean $P(n)$ is a type, and a proof of $P(n)$ is a term of that type, so the proof function takes as input $n$ and spits out a term whose type depends on $n$, so it's difficult to imagine it as a traditional function from the naturals to some fixed type -- there is no "type of all proofs of all propositions" for the same sort of reason that there's no set of all sets. The function $P$ itself (the statements of the theorems) is just a regular function from $\mathbb{N}$ to `Prop`

, but the proof function is not a function in a traditional sense, it's a term of the Pi type ` Π (n : nat), P n`

, or, as a mathematician would usually write, a proof of $\forall n\in\mathbb{N}, P(n)$.

#### Kevin Buzzard (Oct 24 2020 at 14:19):

Theorem Proving In Lean provides a more computer-science-focussed explanation of Pi types in section 2.8.

#### Adam Topaz (Oct 24 2020 at 14:25):

Everything Kevin said is of course important, but another way to look at this in this particular case is that, a priori, `D`

has nothing to do with `C`

, so you need to tell lean explicitly that `D`

is a subcategory of `C`

, i.e. you would have to write `subcategory C D`

. The actual reason, coming from lean syntax, is that you wrote `variables (C: Type u) [category.{v} C]`

, and `C`

appears in the definition of `subcategory`

, so lean automatically makes `C`

an explicit variable in the declaration of `subcategory`

.

#### Kevin Buzzard (Oct 24 2020 at 14:26):

I also realise that I probably can make a type of all proofs of all propositions -- it's `Π (P : Prop), P`

:-)

#### Adam Topaz (Oct 24 2020 at 14:27):

That's a good empty type :)

#### Kevin Buzzard (Oct 24 2020 at 14:28):

oh yeah, it seems to say that every proposition is true :-)

#### Adam Topaz (Oct 24 2020 at 14:29):

BTW, I think this is one instance where it makes sense to define a subcategory as a category with a faithful functor, as opposed to, say, something analogous to bundled subrings (which are defined as a subset of the ring with some conditions), essentially due to the equivalence principle in category theory ( https://ncatlab.org/nlab/show/principle+of+equivalence )

#### Kevin Buzzard (Oct 24 2020 at 14:29):

and Lean doesn't buy `Σ (P : Prop), P`

#### Adam Topaz (Oct 24 2020 at 14:31):

Oh, and one more comment, since `faithful`

is a class, it makes sense to define subcategory using the following syntax:

```
class subcategory (D: Type u) [category.{v} D] :=
(inc: D ⥤ C)
[faithful inc]
```

This way lean would go and try to find a `faithful`

instance for `inc`

using typeclass search, instead of requiring the user to manually tell lean what the instance is.

#### Adam Topaz (Oct 24 2020 at 14:32):

This works:

```
def foo := Σ (P : Prop), (plift P)
```

#### Kevin Buzzard (Oct 24 2020 at 14:34):

This doesn't: `example : Σ (P : Prop), plift P := ⟨true, trivial⟩`

#### Kevin Buzzard (Oct 24 2020 at 14:35):

got it -- `example : Σ (P : Prop), plift P := ⟨true, plift.up trivial⟩`

#### Adam Topaz (Oct 24 2020 at 14:35):

Yeah. it's the plift thing

#### Adam Topaz (Oct 24 2020 at 14:45):

Saul is a homotopy theorist, so you can just tell him that a dependent function is a section of a fibration :)

#### Reid Barton (Oct 24 2020 at 15:38):

Since weak equivalences form a *wide* subcategory, and the basic operation is asking whether a morphism of the ambient category is a weak equivalence, I think it's better not to use this equivalence-invariant approach and just use some variation on `\Pi {X Y : C} (f : X --> Y), Prop`

.

#### Reid Barton (Oct 24 2020 at 15:39):

@Saul Glasman You should take a look at https://github.com/rwbarton/lean-homotopy-theory and https://github.com/rwbarton/lean-model-categories/tree/top-dev (note: this one is a non-master branch).

#### Adam Topaz (Oct 24 2020 at 15:42):

Oh right, this is for defining a model structure. There is also docs#category_theory.arrow which you can use instead of the Pi type that Reid mentioned

#### Adam Topaz (Oct 24 2020 at 15:44):

I.e. you can use `set (arrow C)`

#### Reid Barton (Oct 24 2020 at 15:44):

I think I also started with a similar approach using `extends`

but a problem is that as soon as you add a second class of morphisms (like cofibrations) you need a way to distinguish whether you're talking about the weak equivalences subcategory or the cofibrations subcategory.

#### Reid Barton (Oct 24 2020 at 15:47):

I think using `arrow`

will get awkward pretty quickly because Lean is bad at unification problems like "what's `a : arrow C`

with `a.hom = f`

".

#### Reid Barton (Oct 24 2020 at 15:48):

It's more practical to just make all the objects involved into implicit arguments--I edited my original message to reflect this.

#### Adam Topaz (Oct 24 2020 at 15:57):

Sometimes (like in this case) I wish categories were defined as categories internal to types, where the type of all arrows is a first class citizen like the type of objects.

#### Reid Barton (Oct 24 2020 at 15:58):

The downside is that it's not as convenient to take the intersection of two wide subcategories, but (a) that's not something that happens very often, (b) even if you get to reuse the intersection of `set`

s, you still need to prove it is closed under composition, say, so there's more work that needs to happen anyways

#### Saul Glasman (Oct 24 2020 at 16:48):

Thanks everyone!

#### Saul Glasman (Oct 24 2020 at 16:48):

Reid, I didn't know that you had worked on model categories - I'll take a look at your approach

#### Saul Glasman (Oct 24 2020 at 16:53):

I think I still don't know how to read `Π (D : Type u) [_inst_2 : category D], Type (max u v)`

, which is supposed to be the type of `subcategory D`

. Does it mean "for each type `D`

and (implicit) category structure on `D`

, a type"? Shouldn't `D`

be fixed here?

#### Reid Barton (Oct 24 2020 at 17:13):

I can translate your Lean code back into math:

Let $C$ be a category.

Definition. A *$C$-subcategory structure* on a category $D$ consists of a faithful functor $i : D \to C$.

Definition. A *relative category* is a category $D$ equipped with a $D$-subcategory structure such that $i$ is surjective on objects.

#### Reid Barton (Oct 24 2020 at 17:14):

You'll note that something is missing in the second definition: a $D$-subcategory structure on what?

#### Reid Barton (Oct 24 2020 at 17:14):

The error is saying that `subcategory D`

expected more arguments, this missing other category (which, as a result of the chosen variable names, Lean is also calling `D`

).

#### Saul Glasman (Oct 24 2020 at 18:01):

So there are actually two different `D`

s?

#### Kevin Buzzard (Oct 24 2020 at 18:03):

Reid is just saying that in the definition of relative category which you posted, no C is mentioned, so there must be something wrong.

#### Adam Topaz (Oct 24 2020 at 18:11):

If you want to go with the faithful functor route without having to specify both `C`

and `D`

you could do something like this:

```
structure subcategory :=
(D : Type*)
[I : category D]
(inc: D ⥤ C)
[J : faithful inc]
```

#### Reid Barton (Oct 24 2020 at 18:12):

I realize now my English translation is ambiguous in the phrase "a category $D$ equipped with a $D$-subcategory structure" which could be interpreted as "a category $D$ equipped with a $D$-subcategory structure *on $D$*".

#### Reid Barton (Oct 24 2020 at 18:17):

But, that's not the right notion anyways. There needs to be a second category at some point, which is going to play the role of the subcategory of weak equivalences.

#### Saul Glasman (Nov 08 2020 at 16:09):

@Reid Barton , I did one of the "todo"s in your model categories repo as an exercise (retracts of weak equivalences in a model category are weak equivalences) - wonder if you would be willing to accept a PR/give feedback?

#### Reid Barton (Nov 09 2020 at 12:19):

Hi @Saul Glasman, very cool! As you probably noticed, the model categories repository has been dormant for a long time, but please do submit a PR!

#### Reid Barton (Nov 09 2020 at 12:23):

At this point the model category repository is so old that, moving forward, it would probably be better to start from scratch.

#### Saul Glasman (Nov 11 2020 at 01:04):

Done! https://github.com/rwbarton/lean-model-categories/pull/1/files

#### Saul Glasman (Nov 11 2020 at 01:06):

Reid Barton said:

At this point the model category repository is so old that, moving forward, it would probably be better to start from scratch.

Yeah, I noticed that if I updated the mathlib dependency to current in the model categories repo, things failed fairly dramatically...

Last updated: Dec 20 2023 at 11:08 UTC