# Zulip Chat Archive

## Stream: maths

### Topic: composing a list of functions

#### Kenny Lau (Aug 03 2020 at 16:59):

Can we compose a list of functions? Would this have any use?

#### Kenny Lau (Aug 03 2020 at 16:59):

Currently we can only compose two functions

#### Kenny Lau (Aug 03 2020 at 16:59):

and n times if the domain and codomain happen to be the same

#### Adam Topaz (Aug 03 2020 at 16:59):

Cant you just do a list.fold with \circ, or something like this?

#### Jalex Stark (Aug 03 2020 at 17:00):

what's the type of the list?

#### Kenny Lau (Aug 03 2020 at 17:11):

Jalex Stark said:

what's the type of the list?

exactly

#### Adam Topaz (Aug 03 2020 at 17:21):

There must be something like heterogeneous lists right?

#### Adam Topaz (Aug 03 2020 at 17:21):

And it should be `traversable`

so you should be able to fold over it.

#### Adam Topaz (Aug 03 2020 at 17:24):

Maybe traversable isn't the right term here....

#### Reid Barton (Aug 03 2020 at 17:24):

https://hackage.haskell.org/package/thrist-0.4/docs/Data-Thrist.html

https://ncatlab.org/nlab/show/free+category

#### Mario Carneiro (Aug 03 2020 at 18:01):

I tried writing a heterogeneous list type, and decided that it wouldn't actually serve the purposes people want for it very well

#### Mario Carneiro (Aug 03 2020 at 18:02):

It's better to just use iterated `prod`

if you want a strongly typed heterogeneous list

#### Mario Carneiro (Aug 03 2020 at 18:04):

For composing lists of functions, the solution is to use `comp`

several times

#### Mario Carneiro (Aug 03 2020 at 18:05):

If you want a type erased heterogeneous list you can use `list (Sigma A, A)`

but I'm not really sure what this would be good for

#### Kenny Lau (Aug 03 2020 at 19:34):

ok maybe I should talk about a potential use case to make this more clear

#### Kenny Lau (Aug 03 2020 at 19:35):

I want to be able to state (and certainly prove) the statement that a functor from `[n] = {0 -> 1 -> ... -> n}`

to any category `C`

is the same as `n`

composable morphisms in `C`

#### Kenny Lau (Aug 03 2020 at 19:35):

Mario Carneiro said:

For composing lists of functions, the solution is to use

`comp`

several times

do you mean that if we have 3 functions then we use `comp`

twice? this sounds like it can't work for an arbitrary `n`

, but I might be misunderstanding your suggestion

#### Adam Topaz (Aug 03 2020 at 19:38):

Are you defining the nerve?

#### Kenny Lau (Aug 03 2020 at 19:38):

indeed!

#### Adam Topaz (Aug 03 2020 at 19:38):

Cool!

#### Adam Topaz (Aug 03 2020 at 19:39):

Presumably you can define the simplicial set by induction on n, no?

#### Kenny Lau (Aug 03 2020 at 19:39):

you don't need induction right

#### Kenny Lau (Aug 03 2020 at 19:40):

`def nerve (C) := \la n, [n] \func C`

#### Kenny Lau (Aug 03 2020 at 19:40):

(pseudocode)

#### Adam Topaz (Aug 03 2020 at 19:40):

Yeah, sure, but I want to exploit the fact that this simplicial set has some horn filling properties :)

#### Kenny Lau (Aug 03 2020 at 19:41):

what's horn filling properties and how does defining `nerve`

inductively exploits that?

#### Reid Barton (Aug 03 2020 at 19:43):

It seems to me like you want to prove that `[n]`

is the free category on the graph `0 -> 1 -> ... -> n`

#### Kenny Lau (Aug 03 2020 at 19:45):

~~defining~~ constructing the free category sounds like a cool project

#### Reid Barton (Aug 03 2020 at 19:47):

#### Kenny Lau (Aug 03 2020 at 19:49):

aha, inductive

#### Kenny Lau (Aug 03 2020 at 19:49):

can one even state "a list of composable morphisms"? it might have to be a type with `nat.rec`

again, like I made before

#### Kenny Lau (Aug 03 2020 at 19:50):

#### Reid Barton (Aug 03 2020 at 19:50):

Isn't that what `morphism_path`

in the link above is?

#### Kenny Lau (Aug 03 2020 at 19:50):

I guess it is

#### Reid Barton (Aug 03 2020 at 19:51):

Another option is trees of (formal) compositions modulo associativity

#### Reid Barton (Aug 03 2020 at 19:51):

& unitality

#### Kenny Lau (Aug 03 2020 at 19:52):

this is syntax vs semantics again: I don't know how to put it into words, but it's sort of the difference between saying that the inductive implementation is `list`

vs a function from `fin n`

is a list

#### Kenny Lau (Aug 03 2020 at 19:52):

if it quacks like a list, then it's a list

#### Reid Barton (Aug 03 2020 at 19:52):

right, so there's a second presentation of categories which doesn't use dependent types but rather a type of objects and a type of (all) morphisms

#### Reid Barton (Aug 03 2020 at 19:53):

then you could consider a list of morphisms together with a bunch of equations that say the intermediate objects line up

#### Reid Barton (Aug 03 2020 at 19:53):

I suspect if you consider the nerve for long enough, you'll be sort of forced into this perspective anyways

#### Kenny Lau (Aug 03 2020 at 19:54):

I keep having the illusion that objects have some "internal representation", that the `inductive`

and the function from `fin n`

have some sort of difference

#### Adam Topaz (Aug 03 2020 at 20:12):

Mathlib should really have categories internal to other categories :)

#### Bhavik Mehta (Aug 03 2020 at 20:13):

https://github.com/b-mehta/topos/blob/master/src/internal_category%20copy.lean Feel free to tidy this and PR it if you want :)

#### Bhavik Mehta (Aug 03 2020 at 20:13):

i'm pretty sure it compiles on the latest mathlib

#### Kenny Lau (Aug 03 2020 at 20:15):

@Bhavik Mehta what's an example of an internal category?

#### Adam Topaz (Aug 03 2020 at 20:16):

A category is an internal category in types :)

#### Adam Topaz (Aug 03 2020 at 20:16):

(At least in the way Reid mentioned above)

#### Kenny Lau (Aug 03 2020 at 20:16):

apart from that, I guess

#### Reid Barton (Aug 03 2020 at 20:17):

a two-term chain complex is a category internal to abelian groups

#### Reid Barton (Aug 03 2020 at 20:25):

normally though you'd look at categories internal to say topological spaces

#### Adam Topaz (Aug 03 2020 at 22:08):

@Kenny Lau In case you find this helpful:

```
import category_theory.category
import category_theory.arrow
open category_theory
variables {C : Type*} [category C]
def composable_things {n : ℕ} : (fin (n+1) → C) → (fin n → arrow C) → Prop :=
nat.rec_on n
(λ _ _, true)
(λ n h f g, (h (f ∘ fin.succ) (g ∘ fin.succ)) ∧ (g 0).left = f 0) -- wrong
```

#### Adam Topaz (Aug 03 2020 at 22:09):

Wait, I may have gotten the fin.succ's wrong.

#### Adam Topaz (Aug 03 2020 at 22:10):

This is probably better:

```
def composable_things {n : ℕ} : (fin (n+1) → C) → (fin n → arrow C) → Prop :=
nat.rec_on n
(λ _ _, true)
(λ n h f g, (h (f ∘ fin.succ) (g ∘ fin.succ)) ∧ (g 0).right = f (fin.succ 0))
```

#### Kenny Lau (Aug 04 2020 at 05:21):

we will certainly run into `eq.rec`

hell if we do this

#### Kenny Lau (Aug 04 2020 at 05:21):

but there seems no other way

#### Scott Morrison (Aug 04 2020 at 05:28):

I've used something like

```
inductive composable_morphisms'
(V : Type u) [category.{v} V] : V → Type (max u v)
| zero [] : Π X, composable_morphisms' X
| cons : Π {X Y : V} (f : X ⟶ Y) (C : composable_morphisms' Y), composable_morphisms' X
def composable_morphisms := Σ (X : V), (composable_morphisms' V X)
```

#### Kenny Lau (Aug 04 2020 at 05:31):

yeah that sounds like a good idea

#### Scott Morrison (Aug 04 2020 at 06:18):

might be better to parameterise by both endpoints, for the sake of composition

#### Kenny Lau (Aug 04 2020 at 06:25):

@Scott Morrison this is what I have now, in my livestream:

```
universe u
/-- A list of composable functions -/
inductive list_fun (α : Type u) : Type u → Type (u+1)
| nil : list_fun α
| cons : Π {β γ}, (β → γ) → list_fun β → list_fun γ
namespace list_fun
#check nil
#check cons (coe : ℕ → ℤ) $ cons (int.nat_abs) nil
/-- The composition of a list of composable functions.
Set up so that `comp (f :: g :: nil) = f ∘ g`. -/
def comp {α} : Π {β}, list_fun α β → α → β
| _ nil := id
| _ (cons f L) := f ∘ L.comp
@[simp] lemma comp_nil (α) : (nil : list_fun α α).comp = id := rfl
@[simp] lemma comp_cons {α β γ} (f : β → γ) (L : list_fun α β) : (cons f L).comp = f ∘ L.comp := rfl
/-- Concatenation of two lists of composable functions. -/
def append {α β} : Π {γ}, list_fun β γ → list_fun α β → list_fun α γ
| _ nil L₂ := L₂
| _ (cons f L₁) L₂ := cons f (append L₁ L₂)
@[simp] lemma comp_append {α β} : ∀ {γ} (L₁ : list_fun β γ) (L₂ : list_fun α β),
(L₁.append L₂).comp = L₁.comp ∘ L₂.comp
| _ nil L₂ := rfl
| _ (cons f L₁) L₂ := congr_arg ((∘) f) $ comp_append L₁ L₂
end list_fun
```

#### Scott Morrison (Aug 04 2020 at 06:27):

Looks great, except that you could make it category polymorphic trivially, and get the current behaviour substituting `Type`

for `C`

. :-)

#### Kenny Lau (Aug 04 2020 at 06:27):

right

#### Kenny Lau (Aug 04 2020 at 06:27):

where in the category library should this go?

#### Scott Morrison (Aug 04 2020 at 06:28):

I guess `comp_append`

would be harder.

#### Scott Morrison (Aug 04 2020 at 06:28):

(deleted)

#### Kenny Lau (Aug 04 2020 at 06:28):

but I just proved `comp_append`

#### Kenny Lau (Aug 04 2020 at 06:28):

oh, you mean for categories

#### Scott Morrison (Aug 04 2020 at 06:29):

Yes. Harder, but still easy. :-)

#### Scott Morrison (Aug 04 2020 at 06:29):

Just make a new file in `category_theory/`

?

#### Scott Morrison (Aug 04 2020 at 06:29):

with the same name as `lift_fun`

, or whatever you call it?

#### Kenny Lau (Aug 04 2020 at 06:30):

I'll add `TODO: port every lemma about list ever (except the permutation part!)`

#### Kenny Lau (Aug 04 2020 at 06:30):

`comp list.repeat = nat.iterate`

!

#### Kenny Lau (Aug 04 2020 at 06:31):

oh right, and prove that this is the same as a functor from fin n+1 to C

#### Scott Morrison (Aug 04 2020 at 06:41):

and the equivalence with the subtype of `list (arrow C)`

satisfying some `pairwise`

condition

#### Kenny Lau (Aug 04 2020 at 06:46):

if I define `cons f L`

then I lose analogy with category; if I define `cons L f`

then I lose analogy with functions...

#### Kenny Lau (Aug 04 2020 at 06:46):

the category theory composition is the opposite of functions iirc

#### Scott Morrison (Aug 04 2020 at 06:47):

Shall we switch the order in `category_theory/`

? :-)

#### Scott Morrison (Aug 04 2020 at 06:48):

I'm not sure it matters particularly; just pick whichever order feels most ergonomic locally.

#### Kenny Lau (Aug 04 2020 at 06:50):

I guess we want `(cons f L).comp = f >> L`

?

#### Kenny Lau (Aug 04 2020 at 07:00):

you know what, I'll just make it so that `(cons f L).comp = L.comp >> f`

, who cares

#### Kenny Lau (Aug 04 2020 at 07:00):

just to make the inductive require one argument less

#### Kenny Lau (Aug 04 2020 at 07:01):

@Scott Morrison is this ok?

#### Kenny Lau (Aug 04 2020 at 07:01):

```
import category_theory.category
universes v u
namespace category_theory
variables {C : Type u} [category.{v} C]
/-- A list of composable functions -/
inductive list_fun (X : C) : C → Type (max u v)
| nil : list_fun X
| cons : Π {Y Z}, (Y ⟶ Z) → list_fun Y → list_fun Z
namespace list_fun
/-- The composition of a list of composable functions.
Set up so that `comp (f :: g :: nil) = (𝟙 ≫ g) ≫ f`. -/
def comp {X : C} : Π {Y}, list_fun X Y → (X ⟶ Y)
| _ nil := 𝟙 X
| _ (cons f L) := L.comp ≫ f
end list_fun
```

#### Kenny Lau (Aug 04 2020 at 07:08):

turns out `comp_append`

wasn't hard:

```
/-
Copyright (c) 2020 Kenny Lau. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kenny Lau
-/
import category_theory.category
/-!
# Lists of Composable Morphisms
In this file we define lists of composable morphisms, and their composition.
We also show that a list of composable morphism is the same as a functor from `[n]`
(the category `0 ⟶ 1 ⟶ ... ⟶ n`) to the category.
## Main Definitions
- `list_fun X Y` where `X, Y : C` for some category `C` is a list of composable morphisms starting
from `X` and ending at `Y`.
- `list_fun.comp L` where `L : list_fun X Y` returns the composition as a morphism `X ⟶ Y`.
-/
-- TODO: port every lemma about list ever
universes v u
namespace category_theory
variables {C : Type u} [category.{v} C]
/-- A list of composable functions -/
inductive list_fun (X : C) : C → Type (max u v)
| nil : list_fun X
| cons : Π {Y Z}, (Y ⟶ Z) → list_fun Y → list_fun Z
notation a :: b := list_fun.cons a b
namespace list_fun
/-- The composition of a list of composable functions.
Set up so that `comp (f :: g :: nil) = (𝟙 ≫ g) ≫ f`. -/
def comp {X : C} : Π {Y}, list_fun X Y → (X ⟶ Y)
| _ nil := 𝟙 X
| _ (f :: L) := L.comp ≫ f
@[simp] lemma comp_nil (X : C) : (nil : list_fun X X).comp = 𝟙 X := rfl
@[simp] lemma comp_cons {X Y Z : C} (f : Y ⟶ Z) (L : list_fun X Y) :
(cons f L).comp = L.comp ≫ f := rfl
/-- Concatenation of two lists of composable functions. -/
def append {X Y : C} : Π {Z}, list_fun Y Z → list_fun X Y → list_fun X Z
| _ nil L₂ := L₂
| _ (cons f L₁) L₂ := cons f (append L₁ L₂)
@[simp] lemma nil_append {X Y : C} (L : list_fun X Y) : nil.append L = L := rfl
@[simp] lemma cons_append {X Y Z W : C} (f : Z ⟶ W) (L₁ : list_fun Y Z) (L₂ : list_fun X Y) :
(cons f L₁).append L₂ = cons f (L₁.append L₂) := rfl
@[simp] lemma comp_append {X Y : C} : ∀ {Z} (L₁ : list_fun Y Z) (L₂ : list_fun X Y),
(L₁.append L₂).comp = L₂.comp ≫ L₁.comp
| _ nil L₂ := by rw [comp_nil, nil_append, category.comp_id]
| _ (cons f L₁) L₂ := by rw [cons_append, comp_cons, comp_cons, comp_append, category.assoc]
end list_fun
end category_theory
```

#### Scott Morrison (Aug 04 2020 at 07:10):

presumably rename `list_fun`

to `list_hom`

?

#### Kenny Lau (Aug 04 2020 at 07:16):

done

#### Kenny Lau (Aug 04 2020 at 07:17):

@Scott Morrison what sort of structure does `list_hom`

form, given `append`

and `map`

?

#### Kenny Lau (Aug 04 2020 at 07:17):

```
def map {X : C} : Π {Y : C}, list_hom X Y → list_hom (F.obj X) (F.obj Y)
```

#### Scott Morrison (Aug 04 2020 at 07:18):

I think `list_hom`

is just the free category on a `category_struct`

.

#### Scott Morrison (Aug 04 2020 at 07:19):

so maybe you could set it up as a functor from `Graph`

to `Cat`

, adjoint to the forgetful functor?

#### Kenny Lau (Aug 04 2020 at 07:35):

is graph in mathlib?

#### Kenny Lau (Aug 04 2020 at 07:35):

@Scott Morrison

#### Kevin Buzzard (Aug 04 2020 at 07:37):

Even if someone had "put graphs in mathlib" the chances that they would be the kind of graph you wanted is i guess low

#### Kenny Lau (Aug 04 2020 at 07:39):

```
structure functor (C : Type u₁) [category.{v₁} C] (D : Type u₂) [category.{v₂} D] :
Type (max v₁ v₂ u₁ u₂) :=
(obj [] : C → D)
(map : Π {X Y : C}, (X ⟶ Y) → ((obj X) ⟶ (obj Y)))
(map_id' : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X) . obviously)
(map_comp' : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = (map f) ≫ (map g) . obviously)
```

#### Kenny Lau (Aug 04 2020 at 07:40):

you don't need C and D to be a category! ;)

#### Kenny Lau (Aug 04 2020 at 07:42):

oh what am I doing, generalizing category theory itself

#### Kenny Lau (Aug 04 2020 at 07:45):

```
/-
Copyright (c) 2020 Kenny Lau. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kenny Lau
-/
import category_theory.functor_category
/-!
# Lists of Composable Morphisms
In this file we define lists of composable morphisms, and their composition.
We also show that a list of composable morphism is the same as a functor from `[n]`
(the category `0 ⟶ 1 ⟶ ... ⟶ n`) to the category.
## Main Definitions
- `list_hom X Y` where `X, Y : C` for some category `C` is a list of composable morphisms starting
from `X` and ending at `Y`.
- `list_hom.comp L` where `L : list_hom X Y` returns the composition as a morphism `X ⟶ Y`.
-/
-- TODO: port every lemma about list ever
universes v₁ v₂ u₁ u₂
namespace category_theory
variables {C : Type u₁} {D : Type u₂}
/-- A list of composable functions -/
inductive list_hom [has_hom.{v₁} C] (X : C) : C → Type (max u₁ v₁)
| nil : list_hom X
| cons : Π {Y Z}, (Y ⟶ Z) → list_hom Y → list_hom Z
namespace list_hom
notation a :: b := cons a b
section has_hom
variables [has_hom.{v₁} C] [has_hom.{v₂} D]
/-- Concatenation of two lists of composable functions. -/
def append {X Y : C} : Π {Z}, list_hom Y Z → list_hom X Y → list_hom X Z
| _ nil L₂ := L₂
| _ (f :: L₁) L₂ := f :: (append L₁ L₂)
notation a ++ b := append a b
@[simp] lemma nil_append {X Y : C} (L : list_hom X Y) : nil ++ L = L := rfl
@[simp] lemma cons_append {X Y Z W : C} (f : Z ⟶ W) (L₁ : list_hom Y Z) (L₂ : list_hom X Y) :
(f :: L₁) ++ L₂ = f :: (L₁ ++ L₂) := rfl
end has_hom
section category_struct
variables [category_struct.{v₁} C] [category_struct.{v₂} D]
/-- The composition of a list of composable functions.
Set up so that `comp (f :: g :: nil) = (𝟙 ≫ g) ≫ f`. -/
def comp {X : C} : Π {Y}, list_hom X Y → (X ⟶ Y)
| _ nil := 𝟙 X
| _ (f :: L) := L.comp ≫ f
@[simp] lemma comp_nil (X : C) : (nil : list_hom X X).comp = 𝟙 X := rfl
@[simp] lemma comp_cons {X Y Z : C} (f : Y ⟶ Z) (L : list_hom X Y) :
(f :: L).comp = L.comp ≫ f := rfl
end category_struct
section category
variables [category.{v₁} C] [category.{v₂} D]
@[simp] lemma comp_append {X Y : C} : ∀ {Z} (L₁ : list_hom Y Z) (L₂ : list_hom X Y),
(L₁.append L₂).comp = L₂.comp ≫ L₁.comp
| _ nil L₂ := by rw [comp_nil, nil_append, category.comp_id]
| _ (f :: L₁) L₂ := by rw [cons_append, comp_cons, comp_cons, comp_append, category.assoc]
variables (F : C ⥤ D)
def map {X : C} : Π {Y : C}, list_hom X Y → list_hom (F.obj X) (F.obj Y)
| _ nil := nil
| _ (f :: L) := F.map f :: L.map
@[simp] lemma map_nil {X : C} : (nil : list_hom X X).map F = nil := rfl
@[simp] lemma map_cons {X Y Z : C} (f : Y ⟶ Z) (L : list_hom X Y) :
(f :: L).map F = F.map f :: L.map F := rfl
@[simp] lemma map_append {X Y : C} : ∀ {Z} (L₁ : list_hom Y Z) (L₂ : list_hom X Y),
(L₁ ++ L₂).map F = L₁.map F ++ L₂.map F
| _ nil L₂ := rfl
| _ (f :: L₁) L₂ := congr_arg (cons (F.map f)) $ map_append L₁ L₂
end category
end list_hom
end category_theory
```

#### Kenny Lau (Aug 04 2020 at 07:45):

"maximal generality"

#### Kenny Lau (Aug 04 2020 at 07:47):

so `Func([n], -)`

is a functor $\mathsf{Cat} \to \mathsf{Type}$?

#### Kenny Lau (Aug 04 2020 at 07:47):

aha

#### Kenny Lau (Aug 04 2020 at 07:47):

then list_hom would also have to be one...?

#### Jalex Stark (Aug 04 2020 at 14:44):

Kevin Buzzard said:

Even if someone had "put graphs in mathlib" the chances that they would be the kind of graph you wanted is i guess low

indeed, the most recent PR attempting to put graphs in mathlib implements loopless graphs, but for the category Graph you really ought to allow loops.

#### Jalex Stark (Aug 04 2020 at 14:50):

this makes it, uh, "cartesian closed" might be the right word? The graph 1 with one vertex and one edge is a terminal object, and this terminal object gives rise to a sensible notion of point. e.g. there is a good bijection between Hom(1, G^H) and Hom(H, G)

#### Adam Topaz (Aug 04 2020 at 14:55):

Mathlib already has something like a (pre-)graph (whatever that means):

```
import category_theory.category
open category_theory
variables (G : Type*) [has_hom G]
```

#### Adam Topaz (Aug 04 2020 at 14:57):

It's certainly possible to take such a $G$ and construct the free category associated to it.

Last updated: May 14 2021 at 18:28 UTC