Theorems · Inductive type · category theory

CategoryTheory.CommSq.LiftStruct

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {A B X Y : C} → {f : A ⟶ X} → {i : A ⟶ B} → {p : X ⟶ Y} → {g : B ⟶ Y} → CategoryTheory.CommSq f i p g → Type v_1

Now we consider a square: `` A f > X | | i p | | v v B g > Y `` The datum of a lift in a commutative square, i.e. an up-right-diagonal morphism which makes both triangles commute.

Defined in

Mathlib.CategoryTheory.CommSq

Cited by

33 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

CategoryTheory.Category