Theorems · Inductive type · category theory

CategoryTheory.PreOneHypercover.Hom

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} → CategoryTheory.PreOneHypercover S → CategoryTheory.PreOneHypercover S → Type (max (max u_2 u_3) v)

A morphism of pre-1-hypercovers of S is a family of refinement morphisms commuting with the structure morphisms of E and F.

Defined in

Mathlib.CategoryTheory.Sites.Hypercover.One

Cited by

53 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CategoryTheory.Category