content: {-# language KindSignatures #-}
  {-# language PolyKinds #-}
  {-# language DataKinds #-}
  {-# language TypeFamilies #-}
  {-# language RankNTypes #-}
  {-# language NoImplicitPrelude #-}
  {-# language FlexibleContexts #-}
  {-# language MultiParamTypeClasses #-}
  {-# language GADTs #-}
  {-# language ConstraintKinds #-}
  {-# language FlexibleInstances #-}
  {-# LANGUAGE TypeAbstractions #-}
  {-# language TypeOperators #-}
  {-# language ScopedTypeVariables #-}
  {-# language DefaultSignatures #-}
  {-# language FunctionalDependencies #-}
  {-# language UndecidableSuperClasses #-}
  {-# language UndecidableInstances #-}
  
  module T11523 where
  
  import Data.Kind (Constraint, Type)
  import Data.Type.Equality (type (~))
  import qualified Prelude
  
  type Cat i = i -> i -> Type
  
  newtype Y (p :: i -> j -> Type) (a :: j) (b :: i) = Y { getY :: p b a }
  
  class Vacuous (a :: i)
  instance Vacuous a
  
  type Category :: Cat i -> Constraint
  class (Functor p, Dom p ~ Op p, Cod p ~ Nat p (->)) => Category @i p where
    type Op p :: Cat i
    type Op p = Y p
    type Ob p :: i -> Constraint
    type Ob p = Vacuous
  
  class (Category (Dom f), Category (Cod f)) => Functor (f :: i -> j) where
    type Dom f :: Cat i
    type Cod f :: Cat j
  
  class    (Functor f, Dom f ~ p, Cod f ~ q) => Fun (p :: Cat i) (q :: Cat j) (f :: i -> j) | f -> p q
  instance (Functor f, Dom f ~ p, Cod f ~ q) => Fun (p :: Cat i) (q :: Cat j) (f :: i -> j)
  
  data Nat (p :: Cat i) (q :: Cat j) (f :: i -> j) (g :: i -> j)
  
  instance (Category p, Category q) => Category (Nat p q) where
    type Ob (Nat p q) = Fun p q
  
  instance (Category p, Category q) => Functor (Nat p q) where
    type Dom (Nat p q) = Y (Nat p q)
    type Cod (Nat p q) = Nat (Nat p q) (->)
  
  instance (Category p, Category q) => Functor (Nat p q f) where
    type Dom (Nat p q f) = Nat p q
    type Cod (Nat p q f) = (->)
  
  instance Category (->)
  
  instance Functor ((->) e) where
    type Dom ((->) e) = (->)
    type Cod ((->) e) = (->)
  
  instance Functor (->) where
    type Dom (->) = Y (->)
    type Cod (->) = Nat (->) (->)
  
  instance (Category p, Op p ~ Y p) => Category (Y p) where
    type Op (Y p) = p
  
  instance (Category p, Op p ~ Y p) => Functor (Y p a) where
    type Dom (Y p a) = Y p
    type Cod (Y p a) = (->)
  
  instance (Category p, Op p ~ Y p) => Functor (Y p) where
    type Dom (Y p) = p
    type Cod (Y p) = Nat (Y p) (->)
  
  
  {-
  Given:  Category p, Op p ~ Y p
  
     -->  Category p, Op p ~ Y p
          Functor p, Dom p ~ Op p, Cod p ~ Nat p (->)
  
     -->  Category p, Op p ~ Y p
          Functor p, Dom p ~ Op p, Cod p ~ Nat p (->)
          Category (Dom p), Category (Cod p)
  -}
  