import Mathlib.CategoryTheory.Category.Basic
import Mathlib.CategoryTheory.IsomorphismClasses
import Mathlib.CategoryTheory.NatIso

#check
Quiver.{v, u} (V : Type u) : Type (max u (v + 1)) 
Quiver: Type u → Type (max u (v + 1))
Quiver

universe u

variable {
U: Type u
U: 
Type u: Type (u + 1)
Type u} [
Quiver: Type u → Type (max u (?u.4 + 1))
Quiver 
U: Type u
U] (
a: U
a 
b: U
b : 
U: Type u
U) in
#check
a ⟶ b : Type u_1 
a: U
a ⟶ 
b: U
b

#check
CategoryTheory.isomorphismClasses.{v, u} : CategoryTheory.Functor CategoryTheory.Cat (Type u) 
CategoryTheory.isomorphismClasses: CategoryTheory.Functor CategoryTheory.Cat (Type u)
CategoryTheory.isomorphismClasses

#check
CategoryTheory.NatIso.pi.{w₀, v₁, v₂, u₁, u₂} {I : Type w₀} {C : I → Type u₁}
  [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : I → Type u₂}
  [(i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] {F G : (i : I) → CategoryTheory.Functor (C i) (D i)}
  (e : (i : I) → F i ≅ G i) : CategoryTheory.Functor.pi F ≅ CategoryTheory.Functor.pi G 
CategoryTheory.NatIso.pi: {I : Type w₀} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {D : I → Type u₂} →
        [inst_1 : (i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] →
          {F G : (i : I) → CategoryTheory.Functor (C i) (D i)} →
            ((i : I) → F i ≅ G i) → (CategoryTheory.Functor.pi F ≅ CategoryTheory.Functor.pi G)
CategoryTheory.NatIso.pi

-- ≌
#check
CategoryTheory.Equivalence.{v₁, v₂, u₁, u₂} (C : Type u₁) (D : Type u₂) [CategoryTheory.Category.{v₁, u₁} C]
  [CategoryTheory.Category.{v₂, u₂} D] : Type (max (max (max u₁ u₂) v₁) v₂) 
CategoryTheory.Equivalence: (C : Type u₁) →
  (D : Type u₂) →
    [CategoryTheory.Category.{v₁, u₁} C] → [CategoryTheory.Category.{v₂, u₂} D] → Type (max (max (max u₁ u₂) v₁) v₂)
CategoryTheory.Equivalence

--This file should be redone following https://github.com/lftcm2023/lftcm2023/blob/master/LftCM/C10_Category_Theory/CategoryTheory.lean