Theorems · Inductive type · category theory

CategoryTheory.HomIsOver

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

Given OverClass X S and OverClass Y S and f : X ⟶ Y, HomIsOver f S is the typeclass asserting f commutes with the structure morphisms.

Defined in

Mathlib.CategoryTheory.Comma.Over.OverClass

Cited by

11 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.OverClassCategoryTheory.OverClass