A two-complex is defined by an underlying quiver, a groupoid whose morphisms represent path-homotopy classes of the one-complex, and a pre-functor from the quiver to that groupoid.

The lifting principle below says the groupoid has no extra edges beyond those generated by the quiver modulo the identifications represented by map.

class LeanPool.Polylean.TwoComplex (V : Sort u) [Q : Quiver V] [H : Groupoid V] extends Q.PreFunctor H.toQuiver : Sort (max (max (u + 1) (vg + 1)) vq)

A two-complex presented by a quiver and its path-homotopy groupoid.

• obj : V → V
• map {X Y : V} : (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
• lift {W : Sort u} [G : Groupoid W] (F : Q.PreFunctor G.toQuiver) : (∀ {X Y : V} {e e' : X ⟶ Y}, self.map e = self.map e' → F.map e = F.map e') → H.Functor G

  Lift a compatible quiver pre-functor to a groupoid functor.

• lift_comp {W : Sort u} [G : Groupoid W] (F : Q.PreFunctor G.toQuiver) (h : ∀ {X Y : V} {e e' : X ⟶ Y}, self.map e = self.map e' → F.map e = F.map e') : { obj := self.obj, map := fun {X Y : V} => self.map }.comp (lift F ⋯).toPreFunctor = F

  The lifted functor extends the original quiver pre-functor.