KernelFunctionExpected.lean

set_option autoBoundImplicitLocal false



section

universe u u' v w w' uv vw iu iv iw iuv uu vv iuu



class HasInstances (I : Sort v) : Sort (max (u + 1) v) where
(Inst : I → Sort u)

namespace HasInstances

  instance coeSort (I : Sort v) [h : HasInstances.{u, v} I] : CoeSort I (Sort u) := ⟨h.Inst⟩

  instance sortHasInstances : HasInstances.{u, u + 1} (Sort u) := ⟨id⟩

end HasInstances



structure Universe : Type (max u v) where
(I    : Sort v)
[inst : HasInstances.{u, v} I]

namespace Universe

  instance hasInstances : HasInstances Universe := ⟨λ S => S.I⟩

  variable (U : Universe.{u, v})

  instance instInst : HasInstances.{u, v} U.I := U.inst
  instance : HasInstances U := instInst U

end Universe

def sort : Universe.{u, u + 1} := ⟨Sort u⟩
@[reducible] def prop := sort.{0}
@[reducible] def type := sort.{u + 1}



def MetaRelation (α : Sort u) (V : Universe.{v, w}) := α → α → V

namespace MetaRelation

  section

    variable {α : Sort u} {V : Universe} (R : MetaRelation α V)

    class HasRefl where
    (refl (a : α) : R a a)

    class HasSymm where
    (symm {a b : α} : R a b → R b a)

    class HasTrans where
    (trans {a b c : α} : R a b → R b c → R a c)

    class IsPreorder extends HasRefl R, HasTrans R
    class IsEquivalence extends IsPreorder R, HasSymm R

    notation:90 g:91 " • " f:90 => MetaRelation.HasTrans.trans f g
    postfix:max "⁻¹" => MetaRelation.HasSymm.symm

    @[reducible] def lift {ω : Sort w} (l : ω → α) : MetaRelation ω V := λ a b => R (l a) (l b)

    namespace lift

      variable {ω : Sort w} (l : ω → α)

      instance hasRefl  [h : HasRefl  R] : HasRefl  (lift R l) := ⟨λ a => h.refl (l a)⟩
      instance hasSymm  [h : HasSymm  R] : HasSymm  (lift R l) := ⟨h.symm⟩
      instance hasTrans [h : HasTrans R] : HasTrans (lift R l) := ⟨h.trans⟩

      instance isPreorder    [IsPreorder    R] : IsPreorder    (lift R l) := ⟨⟩
      instance isEquivalence [IsEquivalence R] : IsEquivalence (lift R l) := ⟨⟩

    end lift

  end

  def nativeRelation {α : Sort u} (r : α → α → Prop) : MetaRelation α prop := r

  def nativeEquivalence {α : Sort u} {r : α → α → Prop} (e : Equivalence r) :
    IsEquivalence (nativeRelation r) :=
  { refl  := e.refl,
    symm  := e.symm
    trans := e.trans }

end MetaRelation



class HasEquivalenceRelation (α : Sort u) (V : outParam Universe.{v, w}) :
  Sort (max u (v + 1) w) where
(R : MetaRelation α V)
[h : MetaRelation.IsEquivalence R]

namespace HasEquivalenceRelation

  open MetaRelation

  variable {α : Sort u} {V : Universe} [h : HasEquivalenceRelation α V]

  instance isEquivalence : IsEquivalence h.R := h.h

  infix:25 " ≃ " => HasEquivalenceRelation.R

end HasEquivalenceRelation

instance HasEquivalenceRelation.coeNativeEquivalence {α : Sort u} {r : α → α → Prop} :
  Coe (Equivalence r) (HasEquivalenceRelation α prop) :=
⟨λ e => { R := r,
          h := MetaRelation.nativeEquivalence e }⟩

class HasInstanceEquivalences (U : Universe.{u}) (IU : outParam Universe.{iu}) where
(hasEq (A : U) : HasEquivalenceRelation A IU)

namespace HasInstanceEquivalences

  variable {U IU : Universe} [h : HasInstanceEquivalences U IU]

  instance hasEquivalenceRelation (A : U) : HasEquivalenceRelation A IU := h.hasEq A

end HasInstanceEquivalences

class HasIdentity (U : Universe.{u, uu}) where
{IU : Universe.{iu, iuu}}
[h  : HasInstanceEquivalences U IU]

namespace HasIdentity

  variable (U : Universe) [h : HasIdentity U]

  instance hasInstanceEquivalences : HasInstanceEquivalences U h.IU := h.h

end HasIdentity



class HasFunctors (U : Universe.{u}) [HasIdentity.{u, iu} U] where
(Fun                                          : U → U → U)
(apply {A B : U}                              : Fun A B → A → B)
(congrArg {A B : U} (F : Fun A B) {a₁ a₂ : A} : a₁ ≃ a₂ → apply F a₁ ≃ apply F a₂)

namespace HasFunctors

  open MetaRelation

  infixr:20 " ⟶ " => HasFunctors.Fun

  variable {U : Universe} [HasIdentity U] [HasFunctors U]

  instance coeFun (A B : U) : CoeFun (A ⟶ B) (λ _ => A → B) := ⟨apply⟩

  structure DefFun (A B : U) (f : A → B) where
  (F           : A ⟶ B)
  (eff (a : A) : F a ≃ f a)

  notation:20 A:21 " ⟶{" f:0 "} " B:21 => HasFunctors.DefFun A B f

  variable {A B : U}

  def fromDefFun {f : A → B} (F : A ⟶{f} B) : A ⟶ B := F.F

  def byDef {f : A → B} {F : A ⟶{f} B} {a : A} : (fromDefFun F) a ≃ f a := F.eff a

  def applyCongrArg {A B : U} (F : A ⟶ B) {a₁ a₂ : A} (h : a₁ ≃ a₂)
                    {b₁ b₂ : B} (h₁ : F a₁ ≃ b₁) (h₂ : F a₂ ≃ b₂) :
    b₁ ≃ b₂ :=
  h₂ • congrArg F h • h₁⁻¹

  def defCongrArg {A B : U} {f : A → B} (F : A ⟶{f} B) {a₁ a₂ : A} : a₁ ≃ a₂ → f a₁ ≃ f a₂ :=
  λ h => applyCongrArg (fromDefFun F) h byDef byDef

end HasFunctors



class HasCongrFun (U : Universe.{u}) [HasIdentity U] [HasFunctors U] where
(congrFun {A B : U} {F₁ F₂ : A ⟶ B} (h : F₁ ≃ F₂) (a : A) : F₁ a ≃ F₂ a)

namespace HasCongrFun

  open HasFunctors

  variable {U : Universe} [HasIdentity U] [HasFunctors U] [HasCongrFun U]

  def applyCongrFun {A B : U} {F₁ F₂ : A ⟶ B} (h : F₁ ≃ F₂) (a : A)
                    {b₁ b₂ : B} (h₁ : F₁ a ≃ b₁) (h₂ : F₂ a ≃ b₂) :
    b₁ ≃ b₂ :=
  h₂ • congrFun h a • h₁⁻¹

  def defCongrFun {A B : U} {f₁ f₂ : A → B} {F₁ : A ⟶{f₁} B} {F₂ : A ⟶{f₂} B}
                  (h : fromDefFun F₁ ≃ fromDefFun F₂) (a : A) :
    f₁ a ≃ f₂ a :=
  applyCongrFun h a byDef byDef

end HasCongrFun



class HasRevAppFun (U : Universe) [HasIdentity U] [HasFunctors U] where
(defRevAppFun {A : U} (a : A) (B : U) : (A ⟶ B) ⟶{λ F => F a} B)

namespace HasRevAppFun

  variable {U : Universe} [HasIdentity U] [HasFunctors U] [HasRevAppFun U]

  instance hasCongrFun : HasCongrFun U :=
  ⟨λ {A B F₁ F₂} h a => HasFunctors.defCongrArg (defRevAppFun a B) h⟩

end HasRevAppFun



namespace MetaRelation

  open HasFunctors HasCongrFun

  variable {α : Sort u} {V : Universe.{v}} {VV : Universe.{vv}} [HasIdentity.{v, iv} V]
           [HasFunctors V] (R : MetaRelation α V)

  class HasTransFun [HasIdentity V] [HasFunctors V] [HasTrans R] where
  (defTransFun    {a b   : α} (f : R a b) (c : α) : R b c ⟶{λ g => g • f} R a c)
  (defTransFunFun (a b c : α)                     : R a b ⟶{λ f => fromDefFun (defTransFun f c)} (R b c ⟶ R a c))

  namespace HasTransFun

    variable [HasTrans R] [h : HasTransFun R] [HasCongrFun V]

    def congrArgTransLeft {a b c : α} (f : R a b) {g₁ g₂ : R b c} (hg : g₁ ≃ g₂) :
      g₁ • f ≃ g₂ • f :=
    defCongrArg (defTransFun f c) hg

    def congrArgTransRight {a b c : α} {f₁ f₂ : R a b} (hf : f₁ ≃ f₂) (g : R b c) :
      g • f₁ ≃ g • f₂ :=
    defCongrFun (defCongrArg (defTransFunFun a b c) hf) g

    def congrArgTrans {a b c : α} {f₁ f₂ : R a b} (hf : f₁ ≃ f₂) {g₁ g₂ : R b c} (hg : g₁ ≃ g₂) :
      g₁ • f₁ ≃ g₂ • f₂ :=
    congrArgTransRight R hf g₂ • congrArgTransLeft R f₁ hg

  end HasTransFun

end MetaRelation



namespace MetaRelation

  variable {α : Sort u} {V : Universe.{v}} [HasIdentity.{v, iv} V]
           (R : MetaRelation α V)

  class IsAssociative [HasTrans R] where
  (assoc {a b c d : α} (f : R a b) (g : R b c) (h : R c d) : (h • g) • f ≃ h • (g • f))

  class IsCategoricalPreorder [IsPreorder R] extends IsAssociative R where
  (rightId {a b : α} (f : R a b) : f • HasRefl.refl a ≃ f)
  (leftId  {a b : α} (f : R a b) : HasRefl.refl b • f ≃ f)

  namespace IsCategoricalPreorder

    open HasTransFun

    variable [IsPreorder R] [IsCategoricalPreorder R] [HasFunctors V] [HasTransFun R]

    def cancelLeftId {a b : α} (f : R a b) {e : R b b}
                     (he : e ≃ HasRefl.refl (R := R) b) :
      e • f ≃ f :=
    leftId f • congrArgTransLeft R f he

    def cancelRightId [HasCongrFun V] {a b : α} {e : R a a}
                      (he : e ≃ HasRefl.refl (R := R) a) (f : R a b) :
      f • e ≃ f :=
    rightId f • congrArgTransRight R he f

  end IsCategoricalPreorder

  namespace lift

    variable {ω : Sort w} (l : ω → α)

    instance isAssociative [HasTrans R] [h : IsAssociative R] : IsAssociative (lift R l) :=
    { assoc := h.assoc }

    instance isCategoricalPreorder [IsPreorder R] [h : IsCategoricalPreorder R] :
      IsCategoricalPreorder (lift R l) :=
    { rightId := h.rightId,
      leftId  := h.leftId }

  end lift

end MetaRelation



end



namespace CategoryTheory

  universe u u' u'' v vv w ww iv ivv iw

  open MetaRelation HasTransFun
       IsAssociative IsCategoricalPreorder
       HasFunctors HasCongrFun

  class IsHomUniverse (V : Universe.{v, vv}) extends
    HasIdentity.{v, iv, vv, ivv} V, HasFunctors V, HasRevAppFun V

  class HasMorphisms (V : outParam Universe.{v, vv}) [outParam (IsHomUniverse.{v, vv, iv} V)]
                     (α : Sort u) : Sort (max 1 u vv) where
  (Hom : MetaRelation α V)

  infix:20 " ⇾ " => CategoryTheory.HasMorphisms.Hom

  class IsCategory (V : outParam Universe.{v, vv}) [outParam (IsHomUniverse.{v, vv, iv} V)]
                   (α : Sort u) extends
    HasMorphisms V α : Sort (max 1 u v vv iv) where
  [homIsPreorder            : IsPreorder            Hom]
  [homHasTransFun           : HasTransFun           Hom]
  [homIsCategoricalPreorder : IsCategoricalPreorder Hom]

  namespace IsCategory

    variable {V : Universe.{v, vv}} [IsHomUniverse.{v, vv, iv} V] {α : Sort u} [h : IsCategory V α]

    instance : HasRefl               h.Hom := h.homIsPreorder.toHasRefl
    instance : HasTrans              h.Hom := h.homIsPreorder.toHasTrans
    instance : IsPreorder            h.Hom := h.homIsPreorder
    instance : HasTransFun           h.Hom := h.homHasTransFun
    instance : IsCategoricalPreorder h.Hom := h.homIsCategoricalPreorder

    @[reducible] def idHom (a : α) : a ⇾ a := HasRefl.refl a

  end IsCategory

  open IsCategory



  structure MorphismFunctor {W : Universe.{w, ww}} [IsHomUniverse.{w, ww, iw} W]
                            (α : Sort u) (β : Sort v)
                            [hα : HasMorphisms W α] [hβ : HasMorphisms W β] where
  {φ : α → β}
  (F {a b : α} : (a ⇾ b) ⟶ (φ a ⇾ φ b))

  class IsCategoryFunctor {W : Universe.{w, ww}} [IsHomUniverse.{w, ww, iw} W]
                          {α : Sort u} {β : Sort v} [hα : IsCategory W α] [hβ : IsCategory W β]
                          (F : MorphismFunctor α β) where
  (reflEq  (a     : α)                         : F.F (idHom a) ≃ idHom (F.φ a))
  (transEq {a b c : α} (f : a ⇾ b) (g : b ⇾ c) : F.F (g • f) ≃ F.F g • F.F f)



  def Quantification {W : Universe.{w, ww}} [IsHomUniverse.{w, ww, iw} W] {α : Sort u} {β : Sort v}
                     [hα : HasMorphisms W α] [hβ : IsCategory W β] (F G : MorphismFunctor α β) :=
  ∀ a, hβ.Hom (F.φ a) (G.φ a)

  namespace Quantification

    variable {W : Universe.{w, ww}} [IsHomUniverse.{w, ww, iw} W] {α : Sort u} {β : Sort v}

    @[reducible] def refl [hα : HasMorphisms W α] [hβ : IsCategory W β] (F : MorphismFunctor α β) :
      Quantification F F :=
    λ a => HasRefl.refl (F.φ a)

    @[reducible] def trans [hα : HasMorphisms W α] [hβ : IsCategory W β]
                           {F G H : MorphismFunctor α β}
                           (η : Quantification F G) (ε : Quantification G H) :
      Quantification F H :=
    λ a => ε a • η a

  end Quantification

  class IsNaturalTransformation {W : Universe.{w, ww}} [IsHomUniverse.{w, ww, iw} W]
                                {α : Sort u} {β : Sort v}
                                [hα : HasMorphisms W α] [hβ : IsCategory W β]
                                {F G : MorphismFunctor α β} (η : Quantification F G) where
  (nat {a b : α} (f : a ⇾ b) : hβ.homIsPreorder.trans (F.F f) (η b) ≃ hβ.homIsPreorder.trans (η a) (G.F f))

  namespace IsNaturalTransformation

    variable {W : Universe.{w, ww}} [IsHomUniverse.{w, ww, iw} W] {α : Sort u} {β : Sort v}

    instance refl [hα : HasMorphisms W α] [hβ : IsCategory W β] (F : MorphismFunctor α β) :
      IsNaturalTransformation (Quantification.refl F) :=
      ⟨λ f => (rightId (F.F f))⁻¹ • leftId (F.F f)⟩

    instance trans [hα : HasMorphisms W α] [hβ : IsCategory W β] {F G H : MorphismFunctor α β}
                   (η : Quantification F G) (ε : Quantification G H)
                   [hη : IsNaturalTransformation η] [hε : IsNaturalTransformation ε] :
      IsNaturalTransformation (Quantification.trans η ε) :=
    ⟨λ {a b} f => assoc (η a) (ε a) (H.F f) •
                  congrArgTransLeft hβ.Hom (η a) (hε.nat f) •
                  (assoc (η a) (G.F f) (ε b))⁻¹ •
                  congrArgTransRight hβ.Hom (hη.nat f) (ε b) •
                  assoc (R := hβ.Hom) (F.F f) (η b) (ε b)⟩

  end IsNaturalTransformation



  structure FunDesc {W : Universe.{w, ww}} [IsHomUniverse.{w, ww, iw} W]
                    {α : Sort u} {β : Sort v} [hα : IsCategory W α] [hβ : IsCategory W β]
                    (φ : α → β) where
  (F {a b : α} : (a ⇾ b) ⟶ (φ a ⇾ φ b))
  [hF : IsCategoryFunctor ⟨F⟩]

  namespace FunDesc

    variable {W : Universe.{w, ww}} [IsHomUniverse.{w, ww, iw} W]
             {α : Sort u} {β : Sort v} [hα : IsCategory W α] [hβ : IsCategory W β] {φ : α → β}

    @[reducible] def morFun (F : FunDesc φ) : MorphismFunctor α β := ⟨F.F⟩

    instance (F : FunDesc φ) : IsCategoryFunctor (morFun F) := F.hF

  end FunDesc

  class HasFunProp {W : Universe.{w, ww}} [IsHomUniverse.{w, ww, iw} W]
                   (α : Sort u) (β : Sort v) [hα : IsCategory W α] [hβ : IsCategory W β] where
  (Fun : (α → β) → W)
  (desc {φ : α → β} : Fun φ → FunDesc φ)

  namespace HasFunProp

    variable {W : Universe.{w, ww}} [IsHomUniverse.{w, ww, iw} W]

    structure Functor (α : Sort u) (β : Sort v) [hα : IsCategory W α] [hβ : IsCategory W β]
                      [h : HasFunProp α β] : Sort (max 1 u v w) where
    {φ : α → β}
    (F : h.Fun φ)

    namespace Functor

      infixr:20 " ⮕ " => CategoryTheory.HasFunProp.Functor

      variable {α : Sort u} {β : Sort v} [hα : IsCategory W α] [hβ : IsCategory W β]
               [h : HasFunProp α β] (F : α ⮕ β)

      def desc : FunDesc F.φ := h.desc F.F
      @[reducible] def preFun {a b : α} : (a ⇾ b) ⟶ (F.φ a ⇾ F.φ b) := (desc F).F
      @[reducible] def morFun : MorphismFunctor α β := ⟨preFun F⟩

      @[reducible] def mapHom {a b : α} (f : a ⇾ b) : F.φ a ⇾ F.φ b :=
      (preFun F) f

      def reflEq (a : α) : mapHom F (idHom a) ≃ idHom (F.φ a) :=
      IsCategoryFunctor.reflEq (F := morFun F) a

      def transEq {a b c : α} (f : a ⇾ b) (g : b ⇾ c) :
        mapHom F (g • f) ≃ mapHom F g • mapHom F f :=
      IsCategoryFunctor.transEq (F := morFun F) f g

    end Functor

  end HasFunProp



  structure NatDesc {W : Universe.{w, ww}} [IsHomUniverse.{w, ww, iw} W]
                    {α : Sort u} {β : Sort v} [hα : IsCategory W α] [hβ : IsCategory W β]
                    [hFunProp : HasFunProp α β] (F G : α ⮕ β) :
    Sort (max 1 u w iw) where
  (η     : Quantification (HasFunProp.Functor.morFun F) (HasFunProp.Functor.morFun G))
  [isNat : IsNaturalTransformation η]

  namespace NatDesc

    variable {W : Universe.{w, ww}} [IsHomUniverse.{w, ww, iw} W]
             {α : Sort u} {β : Sort v} [hα : IsCategory W α] [hβ : IsCategory W β]
             [hFunProp : HasFunProp α β]
             {F G : α ⮕ β} (η : NatDesc F G)

    instance : IsNaturalTransformation η.η := η.isNat

  end NatDesc

  class HasNatRel {W : Universe.{w, ww}} [IsHomUniverse.{w, ww, iw} W]
                  (α : Sort u) (β : Sort v) [hα : IsCategory W α] [hβ : IsCategory W β]
                  [hFunProp : HasFunProp α β] where
  (Nat : MetaRelation (α ⮕ β) W)
  (desc {F G : α ⮕ β} (η : Nat F G) : NatDesc F G)
  (defNatFun (F G : α ⮕ β) (a : α) :
     Nat F G ⟶{λ η => (desc η).η a} (F.φ a ⇾ G.φ a))

  namespace HasNatRel

    open HasFunctors HasFunProp HasFunProp.Functor

    section

      variable {W : Universe.{w, ww}} [IsHomUniverse.{w, ww, iw} W]
               {α : Sort u} {β : Sort v} [hα : IsCategory W α] [hβ : IsCategory W β]
               [hFunProp : HasFunProp α β] [h : HasNatRel α β]

      @[reducible] def nat {F G : α ⮕ β} (η : h.Nat F G) (a : α) : F.φ a ⇾ G.φ a :=
      (h.desc η).η a

      @[reducible] def natFun (F G : α ⮕ β) (a : α) : h.Nat F G ⟶ (F.φ a ⇾ G.φ a) :=
      fromDefFun (h.defNatFun F G a)

      def natCongrArg {F G : α ⮕ β} {η₁ η₂ : h.Nat F G} (e : η₁ ≃ η₂) (a : α) :
        nat η₁ a ≃ nat η₂ a :=
      defCongrArg (defNatFun F G a) e

      def naturality {F G : α ⮕ β} (η : h.Nat F G) {a b : α} (f : a ⇾ b) :
        nat η b • mapHom F f ≃ mapHom G f • nat η a :=
      (h.desc η).isNat.nat f

      structure DefNat {F G : α ⮕ β} (desc : NatDesc F G) where
      (η             : h.Nat F G)
      (natEq (a : α) : nat η a ≃ desc.η a)

      def byNatDef {F G : α ⮕ β} {desc : NatDesc F G} {η : DefNat desc} (a : α) :
        nat η.η a ≃ desc.η a :=
      η.natEq a

      def NatEquiv {F G : α ⮕ β} (η₁ η₂ : h.Nat F G)
                   (hNat : ∀ a, nat η₁ a ≃ nat η₂ a) :=
      η₁ ≃ η₂

      def DefNatEquiv {F G : α ⮕ β} {desc₁ desc₂ : NatDesc F G} (η₁ : DefNat desc₁)
                      (η₂ : DefNat desc₂) (hNat : ∀ a, desc₁.η a ≃ desc₂.η a) :=
      NatEquiv η₁.η η₂.η (λ a => (byNatDef a)⁻¹ • hNat a • byNatDef a)

    end

    class HasTrivialNaturalityCondition {W : Universe.{w, ww}} [IsHomUniverse.{w, ww, iw} W]
                                        (α : Sort u) (β : Sort v)
                                        [hα : IsCategory W α] [hβ : IsCategory W β]
                                        [hFunProp : HasFunProp α β] [h : HasNatRel α β] where
    (nat {F G : α ⮕ β} (desc : NatDesc F G) : DefNat desc)

    namespace HasTrivialNaturalityCondition

      variable {W : Universe.{w, ww}} [IsHomUniverse.{w, ww, iw} W]
               {α : Sort u} {β : Sort v} [hα : IsCategory W α] [hβ : IsCategory W β]
               [HasFunProp α β] [HasNatRel α β] [h : HasTrivialNaturalityCondition α β]

      def defNat {F G : α ⮕ β} {desc : NatDesc F G} : DefNat desc := h.nat desc

    end HasTrivialNaturalityCondition

    class HasTrivialNatEquiv {W : Universe.{w, ww}} [IsHomUniverse.{w, ww, iw} W]
                             (α : Sort u) (β : Sort v) [hα : IsCategory W α] [hβ : IsCategory W β]
                             [hFunProp : HasFunProp α β] [h : HasNatRel α β] where
    (equiv {F G : α ⮕ β} (η₁ η₂ : h.Nat F G) (hNat : ∀ a, nat η₁ a ≃ nat η₂ a) :
       NatEquiv η₁ η₂ hNat)

    namespace HasTrivialNatEquiv

      variable {W : Universe.{w, ww}} [IsHomUniverse.{w, ww, iw} W]
               {α : Sort u} {β : Sort v} [hα : IsCategory W α] [hβ : IsCategory W β]
               [HasFunProp α β] [hNatRel : HasNatRel α β] [h : HasTrivialNatEquiv α β]

      def natEquiv {F G : α ⮕ β} {η₁ η₂ : hNatRel.Nat F G} {hNat : ∀ a, nat η₁ a ≃ nat η₂ a} :
        NatEquiv η₁ η₂ hNat :=
      h.equiv η₁ η₂ hNat

    end HasTrivialNatEquiv

  end HasNatRel

  class HasNatOp {W : Universe.{w, ww}} [IsHomUniverse.{w, ww, iw} W]
                 (α : Sort u) (β : Sort v) [hα : IsCategory W α] [hβ : IsCategory W β]
                 [hFunProp : HasFunProp α β] extends
    HasNatRel α β where
  (defRefl (F : α ⮕ β) : HasNatRel.DefNat { η     := Quantification.refl (HasFunProp.Functor.morFun F),
                                            isNat := IsNaturalTransformation.refl (HasFunProp.Functor.morFun F)})
  (defTrans {F G H : α ⮕ β} (η : Nat F G) (ε : Nat G H) :
     HasNatRel.DefNat ⟨Quantification.trans (desc η).η (desc ε).η⟩)

  namespace HasNatOp

    open HasFunProp HasFunProp.Functor HasNatRel

    variable {W : Universe.{w, ww}} [IsHomUniverse.{w, ww, iw} W]

    section

      variable (α : Sort u) (β : Sort v) [hα : IsCategory W α] [hβ : IsCategory W β]
               [HasFunProp α β]

      instance trivial [HasNatRel α β] [HasTrivialNaturalityCondition α β] : HasNatOp α β :=
      { defRefl  := λ _   => HasTrivialNaturalityCondition.defNat,
        defTrans := λ _ _ => HasTrivialNaturalityCondition.defNat }

      variable [h : HasNatOp α β]

      instance natIsPreorder : IsPreorder h.Nat :=
      { refl  := λ F   => (h.defRefl F).η,
        trans := λ η ε => (h.defTrans η ε).η }

    end

    section

      variable {α : Sort u} {β : Sort v} [hα : IsCategory W α] [hβ : IsCategory W β]
               [hFunProp : HasFunProp α β] [h : HasNatOp α β]

      def natReflEq (F : α ⮕ β) (a : α) :
        nat (HasRefl.refl F) a ≃ idHom (F.φ a) :=
      byNatDef a

      def natTransEq {F G H : α ⮕ β} (η : h.Nat F G) (ε : h.Nat G H) (a : α) :
        nat (ε • η) a ≃ nat ε a • nat η a :=
      byNatDef a

      def natAssoc {F G H I : α ⮕ β} (η : h.Nat F G) (ε : h.Nat G H) (θ : h.Nat H I) (a : α) :
        nat ((θ • ε) • η) a ≃ nat (θ • (ε • η)) a :=
      (congrArgTransRight hβ.Hom (natTransEq η ε a) (nat θ a) •
       natTransEq (ε • η) θ a)⁻¹ •
      assoc (nat η a) (nat ε a) (nat θ a) •
      (congrArgTransLeft hβ.Hom (nat η a) (natTransEq ε θ a) •
       natTransEq η (θ • ε) a)

      def natRightId {F G : α ⮕ β} (η : h.Nat F G) (a : α) :
        nat (η • HasRefl.refl F) a ≃ nat η a :=
      cancelRightId hβ.Hom (natReflEq F a) (nat η a) •
      natTransEq (HasRefl.refl F) η a

      def natLeftId {F G : α ⮕ β} (η : h.Nat F G) (a : α) :
        nat (HasRefl.refl G • η) a ≃ nat η a :=
      cancelLeftId hβ.Hom (nat η a) (natReflEq G a) •
      natTransEq η (HasRefl.refl G) a

    end

  end HasNatOp

  class HasNatOpEquiv {W : Universe.{w, ww}} [IsHomUniverse.{w, ww, iw} W]
                      (α : Sort u) (β : Sort v) [hα : IsCategory W α] [hβ : IsCategory W β]
                      [hFunProp : HasFunProp α β] extends
    HasNatOp α β where
  (assoc {F G H I : α ⮕ β} (η : Nat F G) (ε : Nat G H) (θ : Nat H I) :
     HasNatRel.NatEquiv ((θ • ε) • η) (θ • (ε • η)) (HasNatOp.natAssoc η ε θ))
  (rightId {F G : α ⮕ β} (η : Nat F G) :
     HasNatRel.NatEquiv (η • HasRefl.refl F) η (HasNatOp.natRightId η))
  (leftId {F G : α ⮕ β} (η : Nat F G) :
     HasNatRel.NatEquiv (HasRefl.refl G • η) η (HasNatOp.natLeftId η))

  namespace HasNatOpEquiv

    open HasNatRel

    variable {W : Universe.{w, ww}} [IsHomUniverse.{w, ww, iw} W]
             (α : Sort u) (β : Sort v) [hα : IsCategory W α] [hβ : IsCategory W β] [HasFunProp α β]

    instance trivial [HasNatOp α β] [HasTrivialNatEquiv α β] : HasNatOpEquiv α β :=
    { assoc     := λ _ _ _   => HasTrivialNatEquiv.natEquiv,
      rightId   := λ _       => HasTrivialNatEquiv.natEquiv,
      leftId    := λ _       => HasTrivialNatEquiv.natEquiv }

    variable [h : HasNatOpEquiv α β]

    instance natIsCategoricalPreorder : IsCategoricalPreorder h.Nat :=
    { assoc   := h.assoc,
      leftId  := h.leftId,
      rightId := h.rightId }

  end HasNatOpEquiv

  class HasNaturality {W : Universe.{w, ww}} [IsHomUniverse.{w, ww, iw} W]
                      (α : Sort u) (β : Sort v) [hα : IsCategory W α] [hβ : IsCategory W β]
                      [hFunProp : HasFunProp α β] extends
    HasNatOpEquiv α β where
  [natHasTransFun : HasTransFun Nat]

  namespace HasNaturality

    open HasFunProp HasFunProp.Functor HasNatRel HasNatOp

    variable {W : Universe.{w, ww}} [IsHomUniverse.{w, ww, iw} W]

    section

      variable (α : Sort u) (β : Sort v) [hα : IsCategory W α] [hβ : IsCategory W β]
               [HasFunProp α β] [h : HasNaturality α β]

      instance : HasTransFun h.Nat := h.natHasTransFun

      instance funHasMorphisms : HasMorphisms W (α ⮕ β) := ⟨h.Nat⟩

      instance funIsCategory : IsCategory.{max 1 u v w} W (α ⮕ β) :=
      { homIsPreorder            := HasNatOp.natIsPreorder α β,
        homHasTransFun           := h.natHasTransFun,
        homIsCategoricalPreorder := HasNatOpEquiv.natIsCategoricalPreorder α β }

    end

    section

      variable {α : Sort u} (a : α) (β : Sort v) [hα : IsCategory W α] [hβ : IsCategory W β]
               [HasFunProp α β] [h : HasNaturality α β]

      def revApp (F : α ⮕ β) : β := F.φ a

      -- The error disappears if the definition of `revAppFunDesc` is replaced with:
      --
      --   instance revAppCategoryFunctor : IsCategoryFunctor { φ := revApp a β,
      --                                                        F := λ {F₁ F₂} => natFun F₁ F₂ a } :=
      --   { reflEq  := λ F   => natReflEq F a • byDef,
      --     transEq := λ η ε => (congrArgTrans hβ.Hom byDef byDef)⁻¹ •
      --                         natTransEq η ε a •
      --                         byDef }
      --
      --   def revAppFunDesc : FunDesc (revApp a β) :=
      --   ⟨λ {F₁ F₂} => natFun F₁ F₂ a⟩

      def revAppFunDesc : FunDesc (revApp a β) :=
      { F  := λ {F₁ F₂} => natFun F₁ F₂ a,
        hF := { reflEq  := λ F   => natReflEq F a • byDef,
                transEq := λ η ε => (congrArgTrans hβ.Hom byDef byDef)⁻¹ •
                                    natTransEq η ε a •
                                    byDef } }

    end

    class HasRevAppFun (α : Sort u) (β : Sort v) [hα : IsCategory W α] [hβ : IsCategory W β]
                       [hFunαβ : HasFunProp α β] [hNatαβ : HasNaturality α β]
                       [hFunαββ : HasFunProp (α ⮕ β) β] where
    (revAppFun (a : α) : hFunαββ.Fun (revApp a β))

  end HasNaturality

end CategoryTheory



class HasTrivialFunctoriality (U : Universe) [HasIdentity U] [HasFunctors U] where
(mkDefFun {A B : U} (f : A → B) : A ⟶{f} B)

namespace HasTrivialFunctoriality

  universe u v

  open MetaRelation

  def defFun {U : Universe} [HasIdentity U] [HasFunctors U]
             [h : HasTrivialFunctoriality U] {A B : U} {f : A → B} :
    A ⟶{f} B :=
  h.mkDefFun f

  instance hasRevAppFun (U : Universe) [HasIdentity U] [HasFunctors U]
                        [HasTrivialFunctoriality U] :
    HasRevAppFun U :=
  ⟨λ _ _ => defFun⟩

  section MetaRelation

    variable {α : Sort u} {V : Universe.{v}} [HasIdentity V] [HasFunctors V]
             [HasTrivialFunctoriality V] (R : MetaRelation α V)

    instance hasTransFun [HasTrans R] : HasTransFun R :=
    { defTransFun    := λ _ _   => defFun,
      defTransFunFun := λ _ _ _ => defFun }

  end MetaRelation

end HasTrivialFunctoriality



namespace sort

  universe u

  theorem Eq.isEquivalence  (α : Sort u) : Equivalence (@Eq α) := ⟨Eq.refl,  Eq.symm,  Eq.trans⟩

  instance hasInstanceEquivalences : HasInstanceEquivalences sort.{u} prop :=
  ⟨λ α => @Eq.isEquivalence (HasInstances.Inst α)⟩

  instance hasIdentity : HasIdentity sort.{u} := ⟨⟩

  instance hasFunctors : HasFunctors sort.{u} :=
  { Fun      := λ α B => α → B,
    apply    := id,
    congrArg := λ f => congrArg f }

  instance hasTrivialFunctoriality : HasTrivialFunctoriality sort.{u} :=
  ⟨λ f => ⟨f, λ _ => rfl⟩⟩

end sort



namespace type

  universe u

  open MetaRelation CategoryTheory IsCategory

  instance isHomUniverse : IsHomUniverse type.{u} := ⟨⟩

  instance hasFunProp (α β : Type u) [hα : IsCategory type.{u} α] [hβ : IsCategory type.{u} β] :
    HasFunProp α β :=
  { Fun  := FunDesc,
    desc := id }

  theorem IsNaturalTransformation.ext {α β : Type u} [hα : HasMorphisms type.{u} α]
                                                     [hβ : IsCategory type.{u} β]
                                      {F G : MorphismFunctor α β} (η : Quantification F G)
                                      (h₁ h₂ : IsNaturalTransformation η) :
    h₁ = h₂ :=
  match h₁, h₂ with
  | ⟨_⟩, ⟨_⟩ => rfl

  theorem NatDesc.ext {α β : Type u} [hα : IsCategory type.{u} α] [hβ : IsCategory type.{u} β]
                      {F G : α ⮕ β} (η₁ η₂ : NatDesc F G) :
    (∀ a, η₁.η a = η₂.η a) → η₁ = η₂ :=
  match η₁, η₂ with
  | { η := nat₁, isNat := isNat₁ }, { η := nat₂, isNat := isNat₂ } =>
    λ h => by have hNat : nat₁ = nat₂ := funext h;
              subst hNat;
              have hIsNat : isNat₁ = isNat₂ :=
                   IsNaturalTransformation.ext (hα := hα.toHasMorphisms)
                                               nat₁ isNat₁ isNat₂;
              subst hIsNat; rfl

  def natRel (α β : Type u) [hα : IsCategory type.{u} α] [hβ : IsCategory type.{u} β] :
    MetaRelation (α ⮕ β) type.{u} :=
  NatDesc

  instance hasNaturalityRelation (α β : Type u) [hα : IsCategory type.{u} α]
                                                [hβ : IsCategory type.{u} β] :
    HasNatRel.{u + 1} α β :=
  { Nat       := natRel α β,
    desc      := id,
    defNatFun := λ _ _ _ => HasTrivialFunctoriality.defFun }

  instance hasTrivialNaturalityCondition (α β : Type u) [hα : IsCategory type.{u} α]
                                                        [hβ : IsCategory type.{u} β] :
    HasNatRel.HasTrivialNaturalityCondition.{u + 1} α β :=
  ⟨λ η => { η     := η,
            natEq := λ _ => rfl }⟩

  instance hasTrivialNatEquiv (α β : Type u) [hα : IsCategory type.{u} α]
                                             [hβ : IsCategory type.{u} β] :
    HasNatRel.HasTrivialNatEquiv.{u + 1} α β :=
  ⟨NatDesc.ext⟩

  instance natIsPreorder (α β : Type u) [hα : IsCategory type.{u} α] [hβ : IsCategory type.{u} β] :
    IsPreorder (natRel α β) :=
  HasNatOp.natIsPreorder α β

  instance hasNaturality (α β : Type u) [hα : IsCategory type.{u} α] [hβ : IsCategory type.{u} β] :
    HasNaturality.{u + 1} α β :=
  { natHasTransFun := HasTrivialFunctoriality.hasTransFun (natRel α β) }

  instance hasRevAppFun (α β : Type u) [hα : IsCategory type.{u} α] [hβ : IsCategory type.{u} β] :
    HasNaturality.HasRevAppFun.{u + 1} α β :=
  { revAppFun := λ a => HasNaturality.revAppFunDesc a β }

end type