quivers and diagrams

Stream: maths

[Johan Commelin]

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]

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

[Kenny Lau]

why don't you use chain lol

[Kenny Lau]

aha

[Johan Commelin]

How would I best go about that

[Kenny Lau]

but lists are all finite

[Johan Commelin]

Why?

[Kenny Lau]

because they're defined inductively

[Kenny Lau]

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]

and I can inductively prove that they are finite :P

[Johan Commelin]

I see

[Johan Commelin]

Crazy...

[Kenny Lau]

you want lazy lists?

[Kenny Lau]

I see you want everything to be lazy

[Kenny Lau]

maybe that's why you think they're crazy

[Johan Commelin]

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

[Kenny Lau]

maybe your ideas are a bit hazy

[Johan Commelin]

That.

[Kenny Lau]

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

[Johan Commelin]

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

[Kenny Lau]

not many words rhyme with lazy though

[Kenny Lau]

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

[Mario Carneiro]

I guess you just did

[Johan Commelin]

And you don't wanna look like jay z

[Johan Commelin]

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]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

product is the limit of the discrete diagram

[Johan Commelin]

But that is not how we use them, I think

[Kenny Lau]

is it not?