## Stream: maths

### Topic: quivers and diagrams

#### Johan Commelin (May 01 2018 at 10:00):

I've got the following snippet

import data.list

universes u v w

structure quiver :=
(V : Type u)
(E : Type v)
(s : E → V)
(t : E → V)

variable {Q : quiver}

definition is_a_path : (list Q.E) → Prop
| [] := true
| [e] := true
| (e₁ :: e₂ :: es) := Q.s e₁ = Q.t e₂ ∧ is_a_path (e₂ :: es)

structure diagram :=
(D : Q.V → Type w)
(m : Π (e : Q.E), D (Q.s e) → D (Q.t e))


#### Johan Commelin (May 01 2018 at 10:00):

But now I realise that I actually only want to consider finite lists

#### Kenny Lau (May 01 2018 at 10:00):

why don't you use chain lol

aha

#### Johan Commelin (May 01 2018 at 10:00):

How would I best go about that

#### Kenny Lau (May 01 2018 at 10:00):

but lists are all finite

Why?

#### Kenny Lau (May 01 2018 at 10:01):

because they're defined inductively

#### Kenny Lau (May 01 2018 at 10:01):

inductive list : Type u → Type u
constructors:
list.nil : Π {T : Type u}, list T
list.cons : Π {T : Type u}, T → list T → list T


#### Kenny Lau (May 01 2018 at 10:01):

and I can inductively prove that they are finite :P

I see

Crazy...

#### Kenny Lau (May 01 2018 at 10:02):

you want lazy lists?

#### Kenny Lau (May 01 2018 at 10:02):

I see you want everything to be lazy

#### Kenny Lau (May 01 2018 at 10:02):

maybe that's why you think they're crazy

#### Johan Commelin (May 01 2018 at 10:02):

Hmm, maybe now I'm happy that they aren't lazy (-;

#### Kenny Lau (May 01 2018 at 10:02):

maybe your ideas are a bit hazy

That.

#### Kenny Lau (May 01 2018 at 10:03):

http://www.rhymezone.com/r/rhyme.cgi?Word=lazy&typeofrhyme=perfect

#### Johan Commelin (May 01 2018 at 10:03):

That is definitely true. It's one of my defining properties

#### Kenny Lau (May 01 2018 at 10:03):

not many words rhyme with lazy though

#### Kenny Lau (May 01 2018 at 10:03):

so I'm done coz I can't use daisy

#### Mario Carneiro (May 01 2018 at 10:03):

I guess you just did

#### Johan Commelin (May 01 2018 at 10:03):

And you don't wanna look like jay z

#### Johan Commelin (May 01 2018 at 10:05):

Anyway... I am going to try and define the set of all paths, and then try to figure out how to define commutative diagrams

#### Kenny Lau (May 01 2018 at 10:05):

hmm... I would rather use categories to define diagrams

#### Kenny Lau (May 01 2018 at 10:06):

https://github.com/kckennylau/category-theory/blob/master/src/natural_transformation.lean

#### Kenny Lau (May 01 2018 at 10:06):

@[reducible] def product {α} (C : category.{u v} α) (ι) (f : ι → α) :=
limit (discrete ι) C (functor.of_discrete C f)


#### Kenny Lau (May 01 2018 at 10:07):

product is the limit of the discrete diagram

#### Johan Commelin (May 01 2018 at 10:07):

But that is not how we use them, I think

#### Kenny Lau (May 01 2018 at 10:07):

is it not?

Last updated: May 12 2021 at 07:17 UTC