Theorems · Theorem · category theory

CategoryTheory.Limits.Types.pullbackIsoPullback_inv_snd

∀ {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.pullbackIsoPullback f g).inv
      (CategoryTheory.Limits.pullback.snd f g) =
    TypeCat.ofHom fun p => (↑p).2

Defined in

Mathlib.CategoryTheory.Limits.Types.Pullbacks

Cited by

3 results in Mathlib

Foundations

Depth 36 from the axioms · uses propext, Classical.choice, Quot.sound