Theorems · Inductive type · category theory

CategoryTheory.IsoCat

(C : Type u_1) →
  (D : Type u_2) →
    [CategoryTheory.Category.{v_1, u_1} C] →
      [CategoryTheory.Category.{v_2, u_2} D] → Type (max (max (max u_1 u_2) v_1) v_2)

An isomorphism of categories: a pair of functors whose composites are equal to the identity functors.

Defined in

Mathlib.CategoryTheory.IsoCat

Cited by

9 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Category