Theorems · Inductive type · category theory

CategoryTheory.Adjunction.CoreHomEquiv

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C D → CategoryTheory.Functor D C → Type (max (max (max u₁ u₂) v₁) v₂)

This is an auxiliary data structure useful for constructing adjunctions. See Adjunction.mkOfHomEquiv. This structure won't typically be used anywhere else.

Defined in

Mathlib.CategoryTheory.Adjunction.Basic

Cited by

11 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Category