{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Internal where

import Prelude (($))

import Data.Fin (fin0, fin1, fin2)
import Data.Type.Nat (Nat2, Nat3)
import Data.Vec.Lazy (Vec (..))
import Proarrow.Category.Instance.Bool (BOOL)
import Proarrow.Category.Instance.FinSet (FINSET (..), FinSet (..))
import Proarrow.Core (CategoryOf (..))
import Proarrow.Profunctor.Instance.Cone (Cone (..), Cosink (..))

-- | An internal category in a category @k@.
class ik `InternalIn` k where
  type C0 ik :: k
  type C1 ik :: k
  source :: C1 ik ~> (C0 ik :: k)
  target :: C1 ik ~> (C0 ik :: k)
  identity :: C0 ik ~> (C1 ik :: k)
  compose :: Cosink [C1 ik, C1 ik, C1 ik :: k] -- first arrow projection, second arrow projection, composite

-- >>> import Data.Fin
-- >>> import Data.Type.Nat
-- >>> import Data.Vec.Lazy
-- >>> import Proarrow.Limit.Pullback
-- >>> (case pullback (source @BOOL @FINSET) (target @BOOL @FINSET) of Cone (Leg (FinSet l) (Leg (FinSet r) Apex)) -> P.show (l, r)) :: P.String
-- "(0 ::: 1 ::: 2 ::: 2 ::: VNil,0 ::: 0 ::: 1 ::: 2 ::: VNil)"
instance BOOL `InternalIn` FINSET where
  type C0 BOOL = FS Nat2 -- Fin0 = FLS, Fin1 = TRU
  type C1 BOOL = FS Nat3 -- Fin0 = Fls, Fin1 = F2T, Fin2 = Tru
  source :: C1 BOOL ~> C0 BOOL
source = Vec ('S ('S ('S 'Z))) (Fin ('S ('S 'Z)))
-> FinSet (FS ('S ('S ('S 'Z)))) (FS ('S ('S 'Z)))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet (Vec ('S ('S ('S 'Z))) (Fin ('S ('S 'Z)))
 -> FinSet (FS ('S ('S ('S 'Z)))) (FS ('S ('S 'Z))))
-> Vec ('S ('S ('S 'Z))) (Fin ('S ('S 'Z)))
-> FinSet (FS ('S ('S ('S 'Z)))) (FS ('S ('S 'Z)))
forall a b. (a -> b) -> a -> b
$ Fin ('S ('S 'Z))
Fin (Plus 'Z ('S ('S 'Z)))
forall (n :: Nat). Fin (Plus 'Z ('S n))
fin0 Fin ('S ('S 'Z))
-> Vec ('S ('S 'Z)) (Fin ('S ('S 'Z)))
-> Vec ('S ('S ('S 'Z))) (Fin ('S ('S 'Z)))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S ('S 'Z))
Fin (Plus 'Z ('S ('S 'Z)))
forall (n :: Nat). Fin (Plus 'Z ('S n))
fin0 Fin ('S ('S 'Z))
-> Vec ('S 'Z) (Fin ('S ('S 'Z)))
-> Vec ('S ('S 'Z)) (Fin ('S ('S 'Z)))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S ('S 'Z))
Fin (Plus ('S 'Z) ('S 'Z))
forall (n :: Nat). Fin (Plus ('S 'Z) ('S n))
fin1 Fin ('S ('S 'Z))
-> Vec 'Z (Fin ('S ('S 'Z))) -> Vec ('S 'Z) (Fin ('S ('S 'Z)))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Vec 'Z (Fin ('S ('S 'Z)))
forall a. Vec 'Z a
VNil
  target :: C1 BOOL ~> C0 BOOL
target = Vec ('S ('S ('S 'Z))) (Fin ('S ('S 'Z)))
-> FinSet (FS ('S ('S ('S 'Z)))) (FS ('S ('S 'Z)))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet (Vec ('S ('S ('S 'Z))) (Fin ('S ('S 'Z)))
 -> FinSet (FS ('S ('S ('S 'Z)))) (FS ('S ('S 'Z))))
-> Vec ('S ('S ('S 'Z))) (Fin ('S ('S 'Z)))
-> FinSet (FS ('S ('S ('S 'Z)))) (FS ('S ('S 'Z)))
forall a b. (a -> b) -> a -> b
$ Fin ('S ('S 'Z))
Fin (Plus 'Z ('S ('S 'Z)))
forall (n :: Nat). Fin (Plus 'Z ('S n))
fin0 Fin ('S ('S 'Z))
-> Vec ('S ('S 'Z)) (Fin ('S ('S 'Z)))
-> Vec ('S ('S ('S 'Z))) (Fin ('S ('S 'Z)))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S ('S 'Z))
Fin (Plus ('S 'Z) ('S 'Z))
forall (n :: Nat). Fin (Plus ('S 'Z) ('S n))
fin1 Fin ('S ('S 'Z))
-> Vec ('S 'Z) (Fin ('S ('S 'Z)))
-> Vec ('S ('S 'Z)) (Fin ('S ('S 'Z)))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S ('S 'Z))
Fin (Plus ('S 'Z) ('S 'Z))
forall (n :: Nat). Fin (Plus ('S 'Z) ('S n))
fin1 Fin ('S ('S 'Z))
-> Vec 'Z (Fin ('S ('S 'Z))) -> Vec ('S 'Z) (Fin ('S ('S 'Z)))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Vec 'Z (Fin ('S ('S 'Z)))
forall a. Vec 'Z a
VNil
  identity :: C0 BOOL ~> C1 BOOL
identity = Vec ('S ('S 'Z)) (Fin ('S ('S ('S 'Z))))
-> FinSet (FS ('S ('S 'Z))) (FS ('S ('S ('S 'Z))))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet (Vec ('S ('S 'Z)) (Fin ('S ('S ('S 'Z))))
 -> FinSet (FS ('S ('S 'Z))) (FS ('S ('S ('S 'Z)))))
-> Vec ('S ('S 'Z)) (Fin ('S ('S ('S 'Z))))
-> FinSet (FS ('S ('S 'Z))) (FS ('S ('S ('S 'Z))))
forall a b. (a -> b) -> a -> b
$ Fin ('S ('S ('S 'Z)))
Fin (Plus 'Z ('S ('S ('S 'Z))))
forall (n :: Nat). Fin (Plus 'Z ('S n))
fin0 Fin ('S ('S ('S 'Z)))
-> Vec ('S 'Z) (Fin ('S ('S ('S 'Z))))
-> Vec ('S ('S 'Z)) (Fin ('S ('S ('S 'Z))))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S ('S ('S 'Z)))
Fin (Plus ('S ('S 'Z)) ('S 'Z))
forall (n :: Nat). Fin (Plus ('S ('S 'Z)) ('S n))
fin2 Fin ('S ('S ('S 'Z)))
-> Vec 'Z (Fin ('S ('S ('S 'Z))))
-> Vec ('S 'Z) (Fin ('S ('S ('S 'Z))))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Vec 'Z (Fin ('S ('S ('S 'Z))))
forall a. Vec 'Z a
VNil

  -- 4 different ways to compose, read vertically.
  compose :: Cosink '[C1 BOOL, C1 BOOL, C1 BOOL]
compose =
    Cone
  ('PR (FS ('S ('S ('S ('S 'Z)))))) (L '[C1 BOOL, C1 BOOL, C1 BOOL])
-> Cosink '[C1 BOOL, C1 BOOL, C1 BOOL]
forall {k} (a :: k) (as :: [k]). Cone ('PR a) (L as) -> Cosink as
Cone (Cone
   ('PR (FS ('S ('S ('S ('S 'Z)))))) (L '[C1 BOOL, C1 BOOL, C1 BOOL])
 -> Cosink '[C1 BOOL, C1 BOOL, C1 BOOL])
-> Cone
     ('PR (FS ('S ('S ('S ('S 'Z)))))) (L '[C1 BOOL, C1 BOOL, C1 BOOL])
-> Cosink '[C1 BOOL, C1 BOOL, C1 BOOL]
forall a b. (a -> b) -> a -> b
$
      (FS ('S ('S ('S ('S 'Z)))) ~> C1 BOOL)
-> Cone ('PR (FS ('S ('S ('S ('S 'Z)))))) (L '[C1 BOOL, C1 BOOL])
-> Cone
     ('PR (FS ('S ('S ('S ('S 'Z)))))) (L '[C1 BOOL, C1 BOOL, C1 BOOL])
forall {k} (a1 :: k) (b :: k) (bs1 :: [k]).
(a1 ~> b) -> Cone ('PR a1) (L bs1) -> Cone ('PR a1) (L (b : bs1))
Leg (Vec ('S ('S ('S ('S 'Z)))) (Fin ('S ('S ('S 'Z))))
-> FinSet (FS ('S ('S ('S ('S 'Z))))) (FS ('S ('S ('S 'Z))))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet (Vec ('S ('S ('S ('S 'Z)))) (Fin ('S ('S ('S 'Z))))
 -> FinSet (FS ('S ('S ('S ('S 'Z))))) (FS ('S ('S ('S 'Z)))))
-> Vec ('S ('S ('S ('S 'Z)))) (Fin ('S ('S ('S 'Z))))
-> FinSet (FS ('S ('S ('S ('S 'Z))))) (FS ('S ('S ('S 'Z))))
forall a b. (a -> b) -> a -> b
$ Fin ('S ('S ('S 'Z)))
Fin (Plus 'Z ('S ('S ('S 'Z))))
forall (n :: Nat). Fin (Plus 'Z ('S n))
fin0 Fin ('S ('S ('S 'Z)))
-> Vec ('S ('S ('S 'Z))) (Fin ('S ('S ('S 'Z))))
-> Vec ('S ('S ('S ('S 'Z)))) (Fin ('S ('S ('S 'Z))))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S ('S ('S 'Z)))
Fin (Plus ('S 'Z) ('S ('S 'Z)))
forall (n :: Nat). Fin (Plus ('S 'Z) ('S n))
fin1 Fin ('S ('S ('S 'Z)))
-> Vec ('S ('S 'Z)) (Fin ('S ('S ('S 'Z))))
-> Vec ('S ('S ('S 'Z))) (Fin ('S ('S ('S 'Z))))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S ('S ('S 'Z)))
Fin (Plus ('S ('S 'Z)) ('S 'Z))
forall (n :: Nat). Fin (Plus ('S ('S 'Z)) ('S n))
fin2 Fin ('S ('S ('S 'Z)))
-> Vec ('S 'Z) (Fin ('S ('S ('S 'Z))))
-> Vec ('S ('S 'Z)) (Fin ('S ('S ('S 'Z))))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S ('S ('S 'Z)))
Fin (Plus ('S ('S 'Z)) ('S 'Z))
forall (n :: Nat). Fin (Plus ('S ('S 'Z)) ('S n))
fin2 Fin ('S ('S ('S 'Z)))
-> Vec 'Z (Fin ('S ('S ('S 'Z))))
-> Vec ('S 'Z) (Fin ('S ('S ('S 'Z))))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Vec 'Z (Fin ('S ('S ('S 'Z))))
forall a. Vec 'Z a
VNil) (Cone ('PR (FS ('S ('S ('S ('S 'Z)))))) (L '[C1 BOOL, C1 BOOL])
 -> Cone
      ('PR (FS ('S ('S ('S ('S 'Z)))))) (L '[C1 BOOL, C1 BOOL, C1 BOOL]))
-> Cone ('PR (FS ('S ('S ('S ('S 'Z)))))) (L '[C1 BOOL, C1 BOOL])
-> Cone
     ('PR (FS ('S ('S ('S ('S 'Z)))))) (L '[C1 BOOL, C1 BOOL, C1 BOOL])
forall a b. (a -> b) -> a -> b
$
        (FS ('S ('S ('S ('S 'Z)))) ~> C1 BOOL)
-> Cone ('PR (FS ('S ('S ('S ('S 'Z)))))) (L '[C1 BOOL])
-> Cone ('PR (FS ('S ('S ('S ('S 'Z)))))) (L '[C1 BOOL, C1 BOOL])
forall {k} (a1 :: k) (b :: k) (bs1 :: [k]).
(a1 ~> b) -> Cone ('PR a1) (L bs1) -> Cone ('PR a1) (L (b : bs1))
Leg (Vec ('S ('S ('S ('S 'Z)))) (Fin ('S ('S ('S 'Z))))
-> FinSet (FS ('S ('S ('S ('S 'Z))))) (FS ('S ('S ('S 'Z))))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet (Vec ('S ('S ('S ('S 'Z)))) (Fin ('S ('S ('S 'Z))))
 -> FinSet (FS ('S ('S ('S ('S 'Z))))) (FS ('S ('S ('S 'Z)))))
-> Vec ('S ('S ('S ('S 'Z)))) (Fin ('S ('S ('S 'Z))))
-> FinSet (FS ('S ('S ('S ('S 'Z))))) (FS ('S ('S ('S 'Z))))
forall a b. (a -> b) -> a -> b
$ Fin ('S ('S ('S 'Z)))
Fin (Plus 'Z ('S ('S ('S 'Z))))
forall (n :: Nat). Fin (Plus 'Z ('S n))
fin0 Fin ('S ('S ('S 'Z)))
-> Vec ('S ('S ('S 'Z))) (Fin ('S ('S ('S 'Z))))
-> Vec ('S ('S ('S ('S 'Z)))) (Fin ('S ('S ('S 'Z))))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S ('S ('S 'Z)))
Fin (Plus 'Z ('S ('S ('S 'Z))))
forall (n :: Nat). Fin (Plus 'Z ('S n))
fin0 Fin ('S ('S ('S 'Z)))
-> Vec ('S ('S 'Z)) (Fin ('S ('S ('S 'Z))))
-> Vec ('S ('S ('S 'Z))) (Fin ('S ('S ('S 'Z))))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S ('S ('S 'Z)))
Fin (Plus ('S 'Z) ('S ('S 'Z)))
forall (n :: Nat). Fin (Plus ('S 'Z) ('S n))
fin1 Fin ('S ('S ('S 'Z)))
-> Vec ('S 'Z) (Fin ('S ('S ('S 'Z))))
-> Vec ('S ('S 'Z)) (Fin ('S ('S ('S 'Z))))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S ('S ('S 'Z)))
Fin (Plus ('S ('S 'Z)) ('S 'Z))
forall (n :: Nat). Fin (Plus ('S ('S 'Z)) ('S n))
fin2 Fin ('S ('S ('S 'Z)))
-> Vec 'Z (Fin ('S ('S ('S 'Z))))
-> Vec ('S 'Z) (Fin ('S ('S ('S 'Z))))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Vec 'Z (Fin ('S ('S ('S 'Z))))
forall a. Vec 'Z a
VNil) (Cone ('PR (FS ('S ('S ('S ('S 'Z)))))) (L '[C1 BOOL])
 -> Cone ('PR (FS ('S ('S ('S ('S 'Z)))))) (L '[C1 BOOL, C1 BOOL]))
-> Cone ('PR (FS ('S ('S ('S ('S 'Z)))))) (L '[C1 BOOL])
-> Cone ('PR (FS ('S ('S ('S ('S 'Z)))))) (L '[C1 BOOL, C1 BOOL])
forall a b. (a -> b) -> a -> b
$
          (FS ('S ('S ('S ('S 'Z)))) ~> C1 BOOL)
-> Cone ('PR (FS ('S ('S ('S ('S 'Z)))))) (L '[])
-> Cone ('PR (FS ('S ('S ('S ('S 'Z)))))) (L '[C1 BOOL])
forall {k} (a1 :: k) (b :: k) (bs1 :: [k]).
(a1 ~> b) -> Cone ('PR a1) (L bs1) -> Cone ('PR a1) (L (b : bs1))
Leg
            (Vec ('S ('S ('S ('S 'Z)))) (Fin ('S ('S ('S 'Z))))
-> FinSet (FS ('S ('S ('S ('S 'Z))))) (FS ('S ('S ('S 'Z))))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet (Vec ('S ('S ('S ('S 'Z)))) (Fin ('S ('S ('S 'Z))))
 -> FinSet (FS ('S ('S ('S ('S 'Z))))) (FS ('S ('S ('S 'Z)))))
-> Vec ('S ('S ('S ('S 'Z)))) (Fin ('S ('S ('S 'Z))))
-> FinSet (FS ('S ('S ('S ('S 'Z))))) (FS ('S ('S ('S 'Z))))
forall a b. (a -> b) -> a -> b
$ Fin ('S ('S ('S 'Z)))
Fin (Plus 'Z ('S ('S ('S 'Z))))
forall (n :: Nat). Fin (Plus 'Z ('S n))
fin0 Fin ('S ('S ('S 'Z)))
-> Vec ('S ('S ('S 'Z))) (Fin ('S ('S ('S 'Z))))
-> Vec ('S ('S ('S ('S 'Z)))) (Fin ('S ('S ('S 'Z))))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S ('S ('S 'Z)))
Fin (Plus ('S 'Z) ('S ('S 'Z)))
forall (n :: Nat). Fin (Plus ('S 'Z) ('S n))
fin1 Fin ('S ('S ('S 'Z)))
-> Vec ('S ('S 'Z)) (Fin ('S ('S ('S 'Z))))
-> Vec ('S ('S ('S 'Z))) (Fin ('S ('S ('S 'Z))))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S ('S ('S 'Z)))
Fin (Plus ('S 'Z) ('S ('S 'Z)))
forall (n :: Nat). Fin (Plus ('S 'Z) ('S n))
fin1 Fin ('S ('S ('S 'Z)))
-> Vec ('S 'Z) (Fin ('S ('S ('S 'Z))))
-> Vec ('S ('S 'Z)) (Fin ('S ('S ('S 'Z))))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S ('S ('S 'Z)))
Fin (Plus ('S ('S 'Z)) ('S 'Z))
forall (n :: Nat). Fin (Plus ('S ('S 'Z)) ('S n))
fin2 Fin ('S ('S ('S 'Z)))
-> Vec 'Z (Fin ('S ('S ('S 'Z))))
-> Vec ('S 'Z) (Fin ('S ('S ('S 'Z))))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Vec 'Z (Fin ('S ('S ('S 'Z))))
forall a. Vec 'Z a
VNil)
            Cone ('PR (FS ('S ('S ('S ('S 'Z)))))) (L '[])
forall {k} (a1 :: k). Ob a1 => Cone ('PR a1) (L '[])
Apex

-- | A finite category is an internal category in @FINSET@.
type Finite k = k `InternalIn` FINSET