Theorems · Definition · category theory

CategoryTheory.Bicategory.InducedBicategory

{B : Type u_1} → (C : Type u_2) → (B → C) → Type u_1

InducedBicategory B C, where F : B → C, is a typeclass synonym for B. This is given a bicategory structure where the 1-morphisms X ⟶ Y are the 1-morphisms in C from F X to F Y, and the 2-morphisms f ⟶ g are also the 2-morphisms in C from f to g.

Defined in

Mathlib.CategoryTheory.Bicategory.InducedBicategory

Cited by

39 results in Mathlib

Foundations

Depth 0 from the axioms · uses no axioms