Theorems · Inductive type · category theory

Prefunctor

(V : Type u₁) → [Quiver V] → (W : Type u₂) → [Quiver W] → Type (max (max (max u₁ u₂) v₁) v₂)

A morphism of quivers. As we will later have categorical functors extend this structure, we call it a Prefunctor.

Defined in

Mathlib.Combinatorics.Quiver.Prefunctor

Cited by

116 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

QuiverQuiver