class LeanPool.Polylean.FreeGroupoid.Struct {S : Sort u} (Q : Quiver S) (G : Groupoid S) : Sort (max (max (u + 1) (vg + 1)) vq)

The definition of a free groupoid with basis Q.

• map {X Y : S} : (X ⟶ Y) → (X ⟶ Y)

  Map each generating quiver edge into the generated groupoid.

• inducedMap {S' : Sort u} {G' : Groupoid S'} : Q.PreFunctor G'.toQuiver → G.Functor G'

  Extend a quiver pre-functor out of the basis to a groupoid functor.

def LeanPool.Polylean.FreeGroupoid.ι {S : Sort u} (Q : Quiver S) (G : Groupoid S) [Struct Q G] : Q.PreFunctor G.toQuiver

The inclusion of a quiver into a groupoid generated freely by it.

Equations

• LeanPool.Polylean.FreeGroupoid.ι Q G = { obj := id, map := fun {X Y : S} => LeanPool.Polylean.FreeGroupoid.Struct.map }

class LeanPool.Polylean.FreeGroupoid {S : Sort u} (Q : Quiver S) (G : Groupoid S) extends LeanPool.Polylean.FreeGroupoid.Struct Q G : Sort (max (max (u + 1) (vg + 1)) vq)

The universal property characterizing a free groupoid on a quiver.

• map {X Y : S} : (X ⟶ Y) → (X ⟶ Y)
• inducedMap {S' : Sort u} {G' : Groupoid S'} : Q.PreFunctor G'.toQuiver → G.Functor G'
• induced_extends {S' : Sort u} {G' : Groupoid S'} (φ : Q.PreFunctor G'.toQuiver) : (ι Q G).comp (Struct.inducedMap φ).toPreFunctor = φ
• induced_unique {S' : Sort u} {G' : Groupoid S'} (Φ Ψ : G.Functor G') : (ι Q G).comp Φ.toPreFunctor = (ι Q G).comp Ψ.toPreFunctor → Φ = Ψ