Theorems · Inductive type · category theory

CategoryTheory.ChosenPullbacksAlong

{C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {Y X : C} → (Y ⟶ X) → Type (max u₁ v₁)

A functorial choice of pullbacks along a morphism f : Y ⟶ X in C given by a functor Over X ⥤ Over Y which is a right adjoint to the functor Over.map f.

Defined in

Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Cited by

73 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CategoryTheory.Category