Theorems · Definition · category theory

CategoryTheory.Cat.freeReflMap

{V : Type u_1} →
  [inst : CategoryTheory.ReflQuiver V] →
    {W : Type u_2} →
      [inst_1 : CategoryTheory.ReflQuiver W] →
        V ⥤rq W → CategoryTheory.Functor (CategoryTheory.Cat.FreeRefl V) (CategoryTheory.Cat.FreeRefl W)

A refl prefunctor V ⥤rq W induces a functor FreeRefl V ⥤ FreeRefl W defined using freeMap and the quotient functor.

Defined in

Mathlib.CategoryTheory.Category.ReflQuiv

Cited by

5 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.ReflQuiverCategoryTheory.ReflQuiver