-- | The finite ordinal @n@ as a thin category: the kind @'ORDINAL' n@ has objects @'OZ', 'OS' 'OZ',
-- ...@ (@n@ of them), with an arrow @a '~>' b@ when and only when @a <= b@ ('LTE'). This is the
-- linear order on @n@ elements. Small enough that (co)equalizers can be computed by explicit case
-- analysis.
module Proarrow.Category.Instance.Ordinal where

import Data.Kind (Constraint, Type)
import Data.Type.Nat (Nat (..), SNat (..), SNatI, snat)
import Prelude (Maybe (..), type (~))

import Proarrow.Category.Enriched.Thin
  ( AtOb (..)
  , DecidableProfunctor (..)
  , Decision (..)
  , Enumerable (..)
  , Finite (..)
  , FmapWrap
  , Indexed (..)
  , IndexedList (..)
  , Lookup
  , MapWrap
  , ThinProfunctor (..)
  , mapDecision
  , mapWrap
  , withLookupMapWrap
  )
import Proarrow.Category.Instance.Bool (BOOL (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard)
import Proarrow.Category.Monoidal.Distributive (Distributive (..))
import Proarrow.Category.Topos (HasEpiMonoFactorization (..))
import Proarrow.Colimit.BinaryCoproduct (HasBinaryCoproducts (..))
import Proarrow.Colimit.Coequalizer (HasCoequalizers (..), thinCoequalize)
import Proarrow.Colimit.Initial (HasInitialObject (..))
import Proarrow.Colimit.Pushout (HasPushouts (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), dimapDefault, obj)
import Proarrow.Limit.BinaryProduct
  ( HasBinaryProducts (..)
  , HasProducts
  , associatorProd
  , associatorProdInv
  , diag
  , leftUnitorProd
  , leftUnitorProdInv
  , rightUnitorProd
  , rightUnitorProdInv
  , swapProd
  )
import Proarrow.Limit.Equalizer (HasEqualizers (..), thinEqualize)
import Proarrow.Limit.Pullback (HasPullbacks (..))
import Proarrow.Limit.Terminal (HasTerminalObject (..))
import Proarrow.Monoid (CocommutativeComonoid, Comonoid (..))
import Prelude qualified as P

type data ORDINAL n where
  OZ :: ORDINAL (S n)
  OS :: ORDINAL (S n) -> ORDINAL (S (S n))

type ORDINAL0 = ORDINAL Z
type ORDINAL1 = ORDINAL (S Z)
type ORDINAL2 = ORDINAL (S (S Z))
type ORDINAL3 = ORDINAL (S (S (S Z)))

type LTE :: forall {n :: Nat}. CAT (ORDINAL n)
data LTE a b where
  ZEQ :: LTE OZ OZ
  ZLT :: LTE OZ b -> LTE OZ (OS b)
  SLT :: LTE a b -> LTE (OS a) (OS b)

-- | @'ORDINAL' 'Z'@ is the empty ordinal, so an object of it is a contradiction: @'LTE' a a@ has
-- no constructor that can match at this kind, and the empty case discharges any goal.
absurdL :: forall (a :: ORDINAL Z) b. (Ob a) => a ~> b
absurdL :: forall (a :: ORDINAL 'Z) (b :: ORDINAL 'Z). Ob a => a ~> b
absurdL = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: ORDINAL 'Z). (CategoryOf (ORDINAL 'Z), Ob a) => Obj a
obj @a of {}

absurdR :: forall a (b :: ORDINAL Z). (Ob b) => a ~> b
absurdR :: forall (a :: ORDINAL 'Z) (b :: ORDINAL 'Z). Ob b => a ~> b
absurdR = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: ORDINAL 'Z). (CategoryOf (ORDINAL 'Z), Ob a) => Obj a
obj @b of {}

type SOrdinal :: forall {n :: Nat}. ORDINAL n -> Type
data SOrdinal a where
  SOZ :: SOrdinal OZ
  SOS :: (IsOrdinal a) => SOrdinal (OS a)

type IsOrdinal :: forall {n :: Nat}. ORDINAL n -> Constraint
class IsOrdinal (a :: ORDINAL n) where
  singOrdinal :: SOrdinal a
instance IsOrdinal OZ where
  singOrdinal :: SOrdinal OZ
singOrdinal = SOrdinal OZ
forall (n :: Nat). SOrdinal OZ
SOZ
instance (IsOrdinal b) => IsOrdinal (OS b) where
  singOrdinal :: SOrdinal (OS b)
singOrdinal = SOrdinal (OS b)
forall (n :: Nat) (b :: ORDINAL ('S n)).
IsOrdinal b =>
SOrdinal (OS b)
SOS

-- | Each ordinal is numbered by itself: @'OZ'@ is zero and @'OS'@ the successor.
type OrdIndex :: forall {n :: Nat}. ORDINAL n -> Nat
type family OrdIndex a where
  OrdIndex OZ = Z
  OrdIndex (OS a) = S (OrdIndex a)

type OrdAt :: forall (n :: Nat) -> Nat -> Maybe (ORDINAL n)
type family OrdAt n i where
  OrdAt Z i = 'Nothing
  OrdAt (S n) Z = 'Just OZ
  OrdAt (S Z) (S i) = 'Nothing
  OrdAt (S (S n)) (S i) = FmapWrap OS (OrdAt (S n) i)

-- | The ordinals of @'ORDINAL' n@, in order.
type OrdObjects :: forall (n :: Nat) -> [ORDINAL n]
type family OrdObjects n where
  OrdObjects Z = '[]
  OrdObjects (S Z) = '[OZ]
  OrdObjects (S (S n)) = OZ ': MapWrap OS (OrdObjects (S n))

instance Indexed (ORDINAL n) where
  type Index (a :: ORDINAL n) = OrdIndex a
  type At (ORDINAL n) i = OrdAt n i

instance (SNatI n) => Finite (ORDINAL n) where
  type Objects (ORDINAL n) = OrdObjects n
  finite :: IndexedList (Objects (ORDINAL n))
finite = forall (n :: Nat) (i :: Nat) r.
SNatI n =>
SNat i
-> ((Lookup (OrdObjects n) i ~ OrdAt n i) =>
    IndexedList (OrdObjects n) -> r)
-> r
withOrdObjects @n SNat 'Z
SZ (Lookup (OrdObjects n) 'Z ~ OrdAt n 'Z) =>
IndexedList (OrdObjects n) -> IndexedList (OrdObjects n)
IndexedList (OrdObjects n) -> IndexedList (OrdObjects n)
forall a. a -> a
P.id
  withAtLookup :: forall (i :: Nat) r.
SNat i
-> ((Lookup (Objects (ORDINAL n)) i ~ At (ORDINAL n) i) => r) -> r
withAtLookup SNat i
i (Lookup (Objects (ORDINAL n)) i ~ At (ORDINAL n) i) => r
r = forall (n :: Nat) (i :: Nat) r.
SNatI n =>
SNat i
-> ((Lookup (OrdObjects n) i ~ OrdAt n i) =>
    IndexedList (OrdObjects n) -> r)
-> r
withOrdObjects @n SNat i
i (r -> IndexedList (OrdObjects n) -> r
forall a b. a -> b -> a
P.const r
(Lookup (Objects (ORDINAL n)) i ~ At (ORDINAL n) i) => r
r)

-- | An ordinal count is none, one, or more. It needs three cases, and not the two of 'Nat', because
-- @'OS'@ lands in @'ORDINAL' ('S' ('S' n))@, so @'ORDINAL' ('S' 'Z')@ holds only @'OZ'@.
ordSize
  :: forall n r
   . (SNatI n)
  => ((n ~ Z) => r) -> ((n ~ S Z) => r) -> (forall m. (n ~ S (S m), SNatI m) => r) -> r
ordSize :: forall (n :: Nat) r.
SNatI n =>
((n ~ 'Z) => r)
-> ((n ~ 'S 'Z) => r)
-> (forall (m :: Nat). (n ~ 'S ('S m), SNatI m) => r)
-> r
ordSize (n ~ 'Z) => r
none (n ~ 'S 'Z) => r
single forall (m :: Nat). (n ~ 'S ('S m), SNatI m) => r
more = case forall (n :: Nat). SNatI n => SNat n
snat @n of
  SNat n
SZ -> r
(n ~ 'Z) => r
none
  SS @m -> case forall (n :: Nat). SNatI n => SNat n
snat @m of
    SNat n1
SZ -> r
(n ~ 'S 'Z) => r
single
    SNat n1
SS -> r
forall (m :: Nat). (n ~ 'S ('S m), SNatI m) => r
more

-- | The ordinals of @'ORDINAL' n@ together with the proof that the list tabulates 'OrdAt' at one index.
-- The two are produced by the same recursion, so each level builds the shorter list once and both
-- the proof and the longer list use it.
withOrdObjects
  :: forall n i r
   . (SNatI n)
  => SNat i -> ((Lookup (OrdObjects n) i ~ OrdAt n i) => IndexedList (OrdObjects n) -> r) -> r
withOrdObjects :: forall (n :: Nat) (i :: Nat) r.
SNatI n =>
SNat i
-> ((Lookup (OrdObjects n) i ~ OrdAt n i) =>
    IndexedList (OrdObjects n) -> r)
-> r
withOrdObjects SNat i
i (Lookup (OrdObjects n) i ~ OrdAt n i) =>
IndexedList (OrdObjects n) -> r
k =
  forall (n :: Nat) r.
SNatI n =>
((n ~ 'Z) => r)
-> ((n ~ 'S 'Z) => r)
-> (forall (m :: Nat). (n ~ 'S ('S m), SNatI m) => r)
-> r
ordSize @n
    ((Lookup (OrdObjects n) i ~ OrdAt n i) =>
IndexedList (OrdObjects n) -> r
IndexedList (OrdObjects n) -> r
k IndexedList '[]
IndexedList (OrdObjects n)
forall {k}. IndexedList '[]
FNil)
    (case SNat i
i of SNat i
SZ -> (Lookup (OrdObjects n) i ~ OrdAt n i) =>
IndexedList (OrdObjects n) -> r
IndexedList (OrdObjects n) -> r
k (IndexedList '[] -> IndexedList '[OZ]
forall {k} (a :: k) (as1 :: [k]).
KnownIndex a =>
IndexedList as1 -> IndexedList (a : as1)
FCons IndexedList '[]
forall {k}. IndexedList '[]
FNil); SNat i
SS -> (Lookup (OrdObjects n) i ~ OrdAt n i) =>
IndexedList (OrdObjects n) -> r
IndexedList (OrdObjects n) -> r
k (IndexedList '[] -> IndexedList '[OZ]
forall {k} (a :: k) (as1 :: [k]).
KnownIndex a =>
IndexedList as1 -> IndexedList (a : as1)
FCons IndexedList '[]
forall {k}. IndexedList '[]
FNil))
    ( \ @m -> case SNat i
i of
        SNat i
SZ -> forall (n :: Nat) (i :: Nat) r.
SNatI n =>
SNat i
-> ((Lookup (OrdObjects n) i ~ OrdAt n i) =>
    IndexedList (OrdObjects n) -> r)
-> r
withOrdObjects @(S m) SNat 'Z
SZ \IndexedList (OrdObjects ('S m))
xs -> (Lookup (OrdObjects n) i ~ OrdAt n i) =>
IndexedList (OrdObjects n) -> r
IndexedList (OrdObjects n) -> r
k (IndexedList (MapWrap OS (OrdObjects ('S m)))
-> IndexedList (OZ : MapWrap OS (OrdObjects ('S m)))
forall {k} (a :: k) (as1 :: [k]).
KnownIndex a =>
IndexedList as1 -> IndexedList (a : as1)
FCons (forall {j} {k} (w :: j -> k) (xs :: [j]).
(forall (a :: j). KnownIndex a => KnownIndex (w a)) =>
IndexedList xs -> IndexedList (MapWrap w xs)
forall (w :: ORDINAL ('S m) -> ORDINAL ('S ('S m)))
       (xs :: [ORDINAL ('S m)]).
(forall (a :: ORDINAL ('S m)). KnownIndex a => KnownIndex (w a)) =>
IndexedList xs -> IndexedList (MapWrap w xs)
mapWrap @OS IndexedList (OrdObjects ('S m))
xs))
        SS @i' -> forall (n :: Nat) (i :: Nat) r.
SNatI n =>
SNat i
-> ((Lookup (OrdObjects n) i ~ OrdAt n i) =>
    IndexedList (OrdObjects n) -> r)
-> r
withOrdObjects @(S m) (forall (n :: Nat). SNatI n => SNat n
snat @i') \IndexedList (OrdObjects ('S m))
xs ->
          forall {j} {k} (w :: j -> k) (xs :: [j]) (i :: Nat) r.
SNat i
-> IndexedList xs
-> ((Lookup (MapWrap w xs) i ~ FmapWrap w (Lookup xs i)) => r)
-> r
forall (w :: ORDINAL ('S m) -> ORDINAL ('S ('S m)))
       (xs :: [ORDINAL ('S m)]) (i :: Nat) r.
SNat i
-> IndexedList xs
-> ((Lookup (MapWrap w xs) i ~ FmapWrap w (Lookup xs i)) => r)
-> r
withLookupMapWrap @OS (forall (n :: Nat). SNatI n => SNat n
snat @i') IndexedList (OrdObjects ('S m))
xs ((Lookup (OrdObjects n) i ~ OrdAt n i) =>
IndexedList (OrdObjects n) -> r
IndexedList (OrdObjects n) -> r
k (IndexedList (MapWrap OS (OrdObjects ('S m)))
-> IndexedList (OZ : MapWrap OS (OrdObjects ('S m)))
forall {k} (a :: k) (as1 :: [k]).
KnownIndex a =>
IndexedList as1 -> IndexedList (a : as1)
FCons (forall {j} {k} (w :: j -> k) (xs :: [j]).
(forall (a :: j). KnownIndex a => KnownIndex (w a)) =>
IndexedList xs -> IndexedList (MapWrap w xs)
forall (w :: ORDINAL ('S m) -> ORDINAL ('S ('S m)))
       (xs :: [ORDINAL ('S m)]).
(forall (a :: ORDINAL ('S m)). KnownIndex a => KnownIndex (w a)) =>
IndexedList xs -> IndexedList (MapWrap w xs)
mapWrap @OS IndexedList (OrdObjects ('S m))
xs)))
    )

-- | The ordinal at an index, if there is one. 'Enumerable' cannot go through the generic 'atOb',
-- which is defined in terms of the 'withOb' being given here, so the walk is done by recursion
-- on the index instead of on the object list.
ordAtOb :: forall n i. (SNatI n) => SNat i -> AtOb (ORDINAL n) (OrdAt n i)
ordAtOb :: forall (n :: Nat) (i :: Nat).
SNatI n =>
SNat i -> AtOb (ORDINAL n) (OrdAt n i)
ordAtOb SNat i
i =
  forall (n :: Nat) r.
SNatI n =>
((n ~ 'Z) => r)
-> ((n ~ 'S 'Z) => r)
-> (forall (m :: Nat). (n ~ 'S ('S m), SNatI m) => r)
-> r
ordSize @n
    AtOb (ORDINAL n) 'Nothing
AtOb (ORDINAL n) (OrdAt n i)
(n ~ 'Z) => AtOb (ORDINAL n) (OrdAt n i)
forall k. AtOb k 'Nothing
AtNothing
    (case SNat i
i of SNat i
SZ -> AtOb (ORDINAL n) ('Just OZ)
AtOb (ORDINAL n) (OrdAt n i)
forall k (a :: k). (Ob a, KnownIndex a) => AtOb k ('Just a)
AtJust; SNat i
SS -> AtOb (ORDINAL n) 'Nothing
AtOb (ORDINAL n) (OrdAt n i)
forall k. AtOb k 'Nothing
AtNothing)
    ( \ @m -> case SNat i
i of
        SNat i
SZ -> AtOb (ORDINAL n) ('Just OZ)
AtOb (ORDINAL n) (OrdAt n i)
forall k (a :: k). (Ob a, KnownIndex a) => AtOb k ('Just a)
AtJust
        SS @i' -> case forall (n :: Nat) (i :: Nat).
SNatI n =>
SNat i -> AtOb (ORDINAL n) (OrdAt n i)
ordAtOb @(S m) (forall (n :: Nat). SNatI n => SNat n
snat @i') of
          AtOb (ORDINAL ('S m)) (OrdAt ('S m) n1)
AtNothing -> AtOb (ORDINAL n) 'Nothing
AtOb (ORDINAL n) (OrdAt n i)
forall k. AtOb k 'Nothing
AtNothing
          AtOb (ORDINAL ('S m)) (OrdAt ('S m) n1)
AtJust -> AtOb (ORDINAL n) ('Just (OS a))
AtOb (ORDINAL n) (OrdAt n i)
forall k (a :: k). (Ob a, KnownIndex a) => AtOb k ('Just a)
AtJust
    )

instance (SNatI n) => Enumerable (ORDINAL n) where
  withIndex :: forall (a :: ORDINAL n) r. Ob a => (KnownIndex a => r) -> r
withIndex @a KnownIndex a => r
r = case forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL n). IsOrdinal a => SOrdinal a
singOrdinal @a of
    SOrdinal a
SOZ -> r
KnownIndex a => r
r
    SOS @a' -> case forall (n :: Nat). SNatI n => SNat n
snat @n of SNat n
SS -> forall k (a :: k) r.
(Enumerable k, Ob a) =>
(KnownIndex a => r) -> r
withIndex @_ @a' r
KnownIndex a => r
KnownIndex a => r
r
  atOb :: forall (i :: Nat). SNat i -> AtOb (ORDINAL n) (At (ORDINAL n) i)
atOb = SNat i -> AtOb (ORDINAL n) (At (ORDINAL n) i)
SNat i -> AtOb (ORDINAL n) (OrdAt n i)
forall (n :: Nat) (i :: Nat).
SNatI n =>
SNat i -> AtOb (ORDINAL n) (OrdAt n i)
ordAtOb

instance Profunctor LTE where
  dimap :: forall (c :: ORDINAL n) (a :: ORDINAL n) (b :: ORDINAL n)
       (d :: ORDINAL n).
(c ~> a) -> (b ~> d) -> LTE a b -> LTE c d
dimap = (c ~> a) -> (b ~> d) -> LTE a b -> LTE c d
LTE c a -> LTE b d -> LTE a b -> LTE c d
forall {k} (p :: CAT k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: ORDINAL n) (b :: ORDINAL n) r.
((Ob a, Ob b) => r) -> LTE a b -> r
\\ LTE a b
ZEQ = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ ZLT LTE OZ b
b = r
(Ob a, Ob b) => r
(Ob OZ, Ob b) => r
r ((Ob OZ, Ob b) => r) -> LTE OZ b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: ORDINAL ('S n)) (b :: ORDINAL ('S n)) r.
((Ob a, Ob b) => r) -> LTE a b -> r
\\ LTE OZ b
b
  (Ob a, Ob b) => r
r \\ SLT LTE a b
ab = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> LTE a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: ORDINAL ('S n)) (b :: ORDINAL ('S n)) r.
((Ob a, Ob b) => r) -> LTE a b -> r
\\ LTE a b
ab
instance Promonad LTE where
  id :: forall (a :: ORDINAL n). Ob a => LTE a a
id @a = case forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL n). IsOrdinal a => SOrdinal a
singOrdinal @a of
    SOrdinal a
SOZ -> LTE a a
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ
    SOrdinal a
SOS -> LTE a a -> LTE (OS a) (OS a)
forall {n :: Nat} (b :: ORDINAL ('S n)) (b :: ORDINAL ('S n)).
LTE b b -> LTE (OS b) (OS b)
SLT LTE a a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: ORDINAL ('S n)). Ob a => LTE a a
id
  LTE b c
ZEQ . :: forall (b :: ORDINAL n) (c :: ORDINAL n) (a :: ORDINAL n).
LTE b c -> LTE a b -> LTE a c
. LTE a b
ZEQ = LTE a c
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ
  ZLT LTE OZ b
b . LTE a b
ZEQ = LTE OZ b -> LTE OZ (OS b)
forall {n :: Nat} (b :: ORDINAL ('S n)). LTE OZ b -> LTE OZ (OS b)
ZLT LTE OZ b
b
  SLT LTE a b
ab . ZLT LTE OZ b
za = LTE OZ b -> LTE OZ (OS b)
forall {n :: Nat} (b :: ORDINAL ('S n)). LTE OZ b -> LTE OZ (OS b)
ZLT (LTE a b
ab LTE a b -> LTE OZ a -> LTE OZ b
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: ORDINAL ('S n)) (c :: ORDINAL ('S n))
       (a :: ORDINAL ('S n)).
LTE b c -> LTE a b -> LTE a c
. LTE OZ a
LTE OZ b
za)
  SLT LTE a b
ab . SLT LTE a b
bc = LTE a b -> LTE (OS a) (OS b)
forall {n :: Nat} (b :: ORDINAL ('S n)) (b :: ORDINAL ('S n)).
LTE b b -> LTE (OS b) (OS b)
SLT (LTE a b
ab LTE a b -> LTE a a -> LTE a b
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: ORDINAL ('S n)) (c :: ORDINAL ('S n))
       (a :: ORDINAL ('S n)).
LTE b c -> LTE a b -> LTE a c
. LTE a a
LTE a b
bc)

-- | The (thin) category of finite ordinals. An arrow from a to b means that a is less than or equal to b.
instance CategoryOf (ORDINAL n) where
  type (~>) = LTE
  type Ob a = IsOrdinal a

-- | @a <= b@ on the ordinal, as a 'BOOL'.
type OrdLeq :: forall {n :: Nat}. ORDINAL n -> ORDINAL n -> BOOL
type family OrdLeq a b where
  OrdLeq OZ b = TRU
  OrdLeq (OS a) OZ = FLS
  OrdLeq (OS a) (OS b) = OrdLeq a b

instance ThinProfunctor LTE

instance DecidableProfunctor LTE where
  type Holds LTE a b = OrdLeq a b
  decide :: forall (a :: ORDINAL n) (b :: ORDINAL n).
(Ob a, Ob b) =>
Decision LTE a b (Holds LTE a b)
decide @a @b = case (forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL n). IsOrdinal a => SOrdinal a
singOrdinal @a, forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL n). IsOrdinal a => SOrdinal a
singOrdinal @b) of
    (SOrdinal a
SOZ, SOrdinal b
SOZ) -> LTE a b -> Decision LTE a b 'TRU
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Decision p a b 'TRU
Yes LTE a b
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ
    (SOrdinal a
SOZ, SOS @b') -> (LTE OZ a -> LTE a b)
-> Decision LTE OZ a 'TRU -> Decision LTE a b 'TRU
forall {k1} {j1} {k2} {j2} (p :: k1 -> j1 -> Type) (a :: k1)
       (b :: j1) (q :: k2 -> j2 -> Type) (c :: k2) (d :: j2) (h :: BOOL).
(p a b -> q c d) -> Decision p a b h -> Decision q c d h
mapDecision LTE OZ a -> LTE a b
LTE OZ a -> LTE OZ (OS a)
forall {n :: Nat} (b :: ORDINAL ('S n)). LTE OZ b -> LTE OZ (OS b)
ZLT (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
forall (p :: ORDINAL ('S n) +-> ORDINAL ('S n))
       (a :: ORDINAL ('S n)) (b :: ORDINAL ('S n)).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
decide @LTE @OZ @b')
    (SOrdinal a
SOS, SOrdinal b
SOZ) -> Decision LTE a b 'FLS
Decision LTE a b (Holds LTE a b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Decision p a b 'FLS
No
    (SOS @a', SOS @b') -> (LTE a a -> LTE a b)
-> Decision LTE a a (OrdLeq a a) -> Decision LTE a b (OrdLeq a a)
forall {k1} {j1} {k2} {j2} (p :: k1 -> j1 -> Type) (a :: k1)
       (b :: j1) (q :: k2 -> j2 -> Type) (c :: k2) (d :: j2) (h :: BOOL).
(p a b -> q c d) -> Decision p a b h -> Decision q c d h
mapDecision LTE a a -> LTE a b
LTE a a -> LTE (OS a) (OS a)
forall {n :: Nat} (b :: ORDINAL ('S n)) (b :: ORDINAL ('S n)).
LTE b b -> LTE (OS b) (OS b)
SLT (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
forall (p :: ORDINAL ('S n) +-> ORDINAL ('S n))
       (a :: ORDINAL ('S n)) (b :: ORDINAL ('S n)).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
decide @LTE @a' @b')
  toHolds :: forall (a :: ORDINAL n) (b :: ORDINAL n) r.
LTE a b -> ((Holds LTE a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds LTE a b
ZEQ (Holds LTE a b ~ 'TRU, Ob a, Ob b) => r
r = r
(Holds LTE a b ~ 'TRU, Ob a, Ob b) => r
r
  toHolds (ZLT LTE OZ b
b) (Holds LTE a b ~ 'TRU, Ob a, Ob b) => r
r = LTE OZ b -> ((Holds LTE OZ b ~ 'TRU, Ob OZ, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
DecidableProfunctor p =>
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
forall (a :: ORDINAL ('S n)) (b :: ORDINAL ('S n)) r.
LTE a b -> ((Holds LTE a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds LTE OZ b
b r
(Holds LTE a b ~ 'TRU, Ob a, Ob b) => r
(Holds LTE OZ b ~ 'TRU, Ob OZ, Ob b) => r
r
  toHolds (SLT LTE a b
ab) (Holds LTE a b ~ 'TRU, Ob a, Ob b) => r
r = LTE a b -> ((Holds LTE a b ~ 'TRU, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
DecidableProfunctor p =>
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
forall (a :: ORDINAL ('S n)) (b :: ORDINAL ('S n)) r.
LTE a b -> ((Holds LTE a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds LTE a b
ab r
(Holds LTE a b ~ 'TRU, Ob a, Ob b) => r
(Holds LTE a b ~ 'TRU, Ob a, Ob b) => r
r

instance HasInitialObject (ORDINAL (S n)) where
  type InitialObject = OZ
  initiate :: forall (a :: ORDINAL ('S n)). Ob a => InitialObject ~> a
initiate @a = case forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S n)). IsOrdinal a => SOrdinal a
singOrdinal @a of
    SOrdinal a
SOZ -> InitialObject ~> a
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ
    SOS @a' -> LTE OZ a -> LTE OZ (OS a)
forall {n :: Nat} (b :: ORDINAL ('S n)). LTE OZ b -> LTE OZ (OS b)
ZLT (forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @_ @a')

instance HasTerminalObject (ORDINAL (S Z)) where
  type TerminalObject = OZ
  terminate :: forall (a :: ORDINAL ('S 'Z)). Ob a => a ~> TerminalObject
terminate @a = case forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S 'Z)). IsOrdinal a => SOrdinal a
singOrdinal @a of SOrdinal a
SOZ -> a ~> TerminalObject
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ

instance (HasTerminalObject (ORDINAL (S n))) => HasTerminalObject (ORDINAL (S (S n))) where
  type TerminalObject = OS TerminalObject
  terminate :: forall (a :: ORDINAL ('S ('S n))). Ob a => a ~> TerminalObject
terminate @a = case forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S ('S n))). IsOrdinal a => SOrdinal a
singOrdinal @a of
    SOrdinal a
SOZ -> LTE OZ TerminalObject -> LTE OZ (OS TerminalObject)
forall {n :: Nat} (b :: ORDINAL ('S n)). LTE OZ b -> LTE OZ (OS b)
ZLT OZ ~> TerminalObject
LTE OZ TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
forall (a :: ORDINAL ('S n)). Ob a => a ~> TerminalObject
terminate
    SOS @a' -> LTE a TerminalObject -> LTE (OS a) (OS TerminalObject)
forall {n :: Nat} (b :: ORDINAL ('S n)) (b :: ORDINAL ('S n)).
LTE b b -> LTE (OS b) (OS b)
SLT (forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate @_ @a')

instance HasBinaryCoproducts (ORDINAL Z) where
  type a || b = a
  withObCoprod :: forall (a :: ORDINAL 'Z) (b :: ORDINAL 'Z) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod Ob (a || b) => r
r = r
Ob (a || b) => r
r
  lft :: forall (a :: ORDINAL 'Z) (b :: ORDINAL 'Z).
(Ob a, Ob b) =>
a ~> (a || b)
lft = a ~> a
a ~> (a || b)
forall (a :: ORDINAL 'Z) (b :: ORDINAL 'Z). Ob b => a ~> b
absurdR
  rgt :: forall (a :: ORDINAL 'Z) (b :: ORDINAL 'Z).
(Ob a, Ob b) =>
b ~> (a || b)
rgt = b ~> a
b ~> (a || b)
forall (a :: ORDINAL 'Z) (b :: ORDINAL 'Z). Ob b => a ~> b
absurdR
  ||| :: forall (x :: ORDINAL 'Z) (a :: ORDINAL 'Z) (y :: ORDINAL 'Z).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
(|||) = \case {}

instance HasBinaryCoproducts (ORDINAL (S Z)) where
  type OZ || OZ = OZ
  withObCoprod :: forall (a :: ORDINAL ('S 'Z)) (b :: ORDINAL ('S 'Z)) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @a @b Ob (a || b) => r
r = case (forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S 'Z)). IsOrdinal a => SOrdinal a
singOrdinal @a, forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S 'Z)). IsOrdinal a => SOrdinal a
singOrdinal @b) of (SOrdinal a
SOZ, SOrdinal b
SOZ) -> r
Ob (a || b) => r
r
  lft :: forall (a :: ORDINAL ('S 'Z)) (b :: ORDINAL ('S 'Z)).
(Ob a, Ob b) =>
a ~> (a || b)
lft @a @b = case (forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S 'Z)). IsOrdinal a => SOrdinal a
singOrdinal @a, forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S 'Z)). IsOrdinal a => SOrdinal a
singOrdinal @b) of (SOrdinal a
SOZ, SOrdinal b
SOZ) -> a ~> (a || b)
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ
  rgt :: forall (a :: ORDINAL ('S 'Z)) (b :: ORDINAL ('S 'Z)).
(Ob a, Ob b) =>
b ~> (a || b)
rgt @a @b = case (forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S 'Z)). IsOrdinal a => SOrdinal a
singOrdinal @a, forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S 'Z)). IsOrdinal a => SOrdinal a
singOrdinal @b) of (SOrdinal a
SOZ, SOrdinal b
SOZ) -> b ~> (a || b)
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ
  x ~> a
LTE x a
ZEQ ||| :: forall (x :: ORDINAL ('S 'Z)) (a :: ORDINAL ('S 'Z))
       (y :: ORDINAL ('S 'Z)).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| y ~> a
LTE y OZ
ZEQ = (x || y) ~> a
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ

-- | Maximum
instance (HasBinaryCoproducts (ORDINAL (S n))) => HasBinaryCoproducts (ORDINAL (S (S n))) where
  type OZ || b = b
  type a || OZ = a
  type OS a || OS b = OS (a || b)
  withObCoprod :: forall (a :: ORDINAL ('S ('S n))) (b :: ORDINAL ('S ('S n))) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @a @b Ob (a || b) => r
r = case forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S ('S n))). IsOrdinal a => SOrdinal a
singOrdinal @a of
    SOrdinal a
SOZ -> r
Ob (a || b) => r
r
    SOS @a' -> case forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S ('S n))). IsOrdinal a => SOrdinal a
singOrdinal @b of
      SOrdinal b
SOZ -> r
Ob (a || b) => r
r
      SOS @b' -> forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @(ORDINAL (S n)) @a' @b' r
Ob (a || a) => r
Ob (a || b) => r
r

  lft :: forall (a :: ORDINAL ('S ('S n))) (b :: ORDINAL ('S ('S n))).
(Ob a, Ob b) =>
a ~> (a || b)
lft @a @b = case forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S ('S n))). IsOrdinal a => SOrdinal a
singOrdinal @b of
    SOrdinal b
SOZ -> forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: ORDINAL ('S ('S n))).
(CategoryOf (ORDINAL ('S ('S n))), Ob a) =>
Obj a
obj @a
    SOS @b' -> case forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S ('S n))). IsOrdinal a => SOrdinal a
singOrdinal @a of
      SOrdinal a
SOZ -> LTE OZ a -> LTE OZ (OS a)
forall {n :: Nat} (b :: ORDINAL ('S n)). LTE OZ b -> LTE OZ (OS b)
ZLT (forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @_ @b')
      SOS @a' -> LTE a (a || a) -> LTE (OS a) (OS (a || a))
forall {n :: Nat} (b :: ORDINAL ('S n)) (b :: ORDINAL ('S n)).
LTE b b -> LTE (OS b) (OS b)
SLT (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @_ @a' @b')

  rgt :: forall (a :: ORDINAL ('S ('S n))) (b :: ORDINAL ('S ('S n))).
(Ob a, Ob b) =>
b ~> (a || b)
rgt @a @b = case forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S ('S n))). IsOrdinal a => SOrdinal a
singOrdinal @a of
    SOrdinal a
SOZ -> forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: ORDINAL ('S ('S n))).
(CategoryOf (ORDINAL ('S ('S n))), Ob a) =>
Obj a
obj @b
    SOS @a' -> case forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S ('S n))). IsOrdinal a => SOrdinal a
singOrdinal @b of
      SOrdinal b
SOZ -> LTE OZ a -> LTE OZ (OS a)
forall {n :: Nat} (b :: ORDINAL ('S n)). LTE OZ b -> LTE OZ (OS b)
ZLT (forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @_ @a')
      SOS @b' -> LTE a (a || a) -> LTE (OS a) (OS (a || a))
forall {n :: Nat} (b :: ORDINAL ('S n)) (b :: ORDINAL ('S n)).
LTE b b -> LTE (OS b) (OS b)
SLT (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @_ @a' @b')

  x ~> a
LTE x a
ZEQ ||| :: forall (x :: ORDINAL ('S ('S n))) (a :: ORDINAL ('S ('S n)))
       (y :: ORDINAL ('S ('S n))).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| y ~> a
LTE y OZ
ZEQ = (x || y) ~> a
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ
  ZLT LTE OZ b
ZEQ ||| y ~> a
a = y ~> a
(x || y) ~> a
a
  x ~> a
a ||| ZLT LTE OZ b
ZEQ = x ~> a
(x || y) ~> a
a
  ZLT a :: LTE OZ b
a@ZLT{} ||| ZLT b :: LTE OZ b
b@ZLT{} = LTE OZ (OS b) -> LTE OZ (OS (OS b))
forall {n :: Nat} (b :: ORDINAL ('S n)). LTE OZ b -> LTE OZ (OS b)
ZLT (OZ ~> OS b
LTE OZ b
a (OZ ~> OS b) -> (OZ ~> OS b) -> (OZ || OZ) ~> OS b
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall (x :: ORDINAL ('S ('S n))) (a :: ORDINAL ('S ('S n)))
       (y :: ORDINAL ('S ('S n))).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| OZ ~> OS b
LTE OZ b
b)
  ZLT a :: LTE OZ b
a@ZLT{} ||| SLT LTE a b
bc = LTE (OZ || a) (OS b) -> LTE (OS (OZ || a)) (OS (OS b))
forall {n :: Nat} (b :: ORDINAL ('S n)) (b :: ORDINAL ('S n)).
LTE b b -> LTE (OS b) (OS b)
SLT (OZ ~> OS b
LTE OZ b
a (OZ ~> OS b) -> (a ~> OS b) -> (OZ || a) ~> OS b
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall (x :: ORDINAL ('S ('S n))) (a :: ORDINAL ('S ('S n)))
       (y :: ORDINAL ('S ('S n))).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| a ~> OS b
LTE a b
bc)
  SLT LTE a b
ab ||| ZLT c :: LTE OZ b
c@ZLT{} = LTE (a || OZ) (OS b) -> LTE (OS (a || OZ)) (OS (OS b))
forall {n :: Nat} (b :: ORDINAL ('S n)) (b :: ORDINAL ('S n)).
LTE b b -> LTE (OS b) (OS b)
SLT (a ~> OS b
LTE a b
ab (a ~> OS b) -> (OZ ~> OS b) -> (a || OZ) ~> OS b
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall (x :: ORDINAL ('S ('S n))) (a :: ORDINAL ('S ('S n)))
       (y :: ORDINAL ('S ('S n))).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| OZ ~> OS b
LTE OZ b
c)
  SLT LTE a b
a ||| SLT LTE a b
b = LTE (a || a) b -> LTE (OS (a || a)) (OS b)
forall {n :: Nat} (b :: ORDINAL ('S n)) (b :: ORDINAL ('S n)).
LTE b b -> LTE (OS b) (OS b)
SLT (a ~> b
LTE a b
a (a ~> b) -> (a ~> b) -> (a || a) ~> b
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall (x :: ORDINAL ('S n)) (a :: ORDINAL ('S n))
       (y :: ORDINAL ('S n)).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| a ~> b
LTE a b
b)

instance HasBinaryProducts (ORDINAL Z) where
  type a && b = a
  withObProd :: forall (a :: ORDINAL 'Z) (b :: ORDINAL 'Z) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd Ob (a && b) => r
r = r
Ob (a && b) => r
r
  fst :: forall (a :: ORDINAL 'Z) (b :: ORDINAL 'Z).
(Ob a, Ob b) =>
(a && b) ~> a
fst = a ~> a
(a && b) ~> a
forall (a :: ORDINAL 'Z) (b :: ORDINAL 'Z). Ob b => a ~> b
absurdR
  snd :: forall (a :: ORDINAL 'Z) (b :: ORDINAL 'Z).
(Ob a, Ob b) =>
(a && b) ~> b
snd = a ~> b
(a && b) ~> b
forall (a :: ORDINAL 'Z) (b :: ORDINAL 'Z). Ob b => a ~> b
absurdR
  &&& :: forall (a :: ORDINAL 'Z) (x :: ORDINAL 'Z) (y :: ORDINAL 'Z).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
(&&&) = \case {}

instance HasBinaryProducts (ORDINAL (S Z)) where
  type OZ && OZ = OZ
  withObProd :: forall (a :: ORDINAL ('S 'Z)) (b :: ORDINAL ('S 'Z)) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @a @b Ob (a && b) => r
r = case (forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S 'Z)). IsOrdinal a => SOrdinal a
singOrdinal @a, forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S 'Z)). IsOrdinal a => SOrdinal a
singOrdinal @b) of (SOrdinal a
SOZ, SOrdinal b
SOZ) -> r
Ob (a && b) => r
r
  fst :: forall (a :: ORDINAL ('S 'Z)) (b :: ORDINAL ('S 'Z)).
(Ob a, Ob b) =>
(a && b) ~> a
fst @a @b = case (forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S 'Z)). IsOrdinal a => SOrdinal a
singOrdinal @a, forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S 'Z)). IsOrdinal a => SOrdinal a
singOrdinal @b) of (SOrdinal a
SOZ, SOrdinal b
SOZ) -> (a && b) ~> a
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ
  snd :: forall (a :: ORDINAL ('S 'Z)) (b :: ORDINAL ('S 'Z)).
(Ob a, Ob b) =>
(a && b) ~> b
snd @a @b = case (forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S 'Z)). IsOrdinal a => SOrdinal a
singOrdinal @a, forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S 'Z)). IsOrdinal a => SOrdinal a
singOrdinal @b) of (SOrdinal a
SOZ, SOrdinal b
SOZ) -> (a && b) ~> b
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ
  a ~> x
LTE a x
ZEQ &&& :: forall (a :: ORDINAL ('S 'Z)) (x :: ORDINAL ('S 'Z))
       (y :: ORDINAL ('S 'Z)).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& a ~> y
LTE OZ y
ZEQ = a ~> (x && y)
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ

-- | Minimum
instance (HasBinaryProducts (ORDINAL (S n))) => HasBinaryProducts (ORDINAL (S (S n))) where
  type OZ && b = OZ
  type a && OZ = OZ
  type OS a && OS b = OS (a && b)
  withObProd :: forall (a :: ORDINAL ('S ('S n))) (b :: ORDINAL ('S ('S n))) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @a @b Ob (a && b) => r
r = case forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S ('S n))). IsOrdinal a => SOrdinal a
singOrdinal @a of
    SOrdinal a
SOZ -> r
Ob (a && b) => r
r
    SOS @a' -> case forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S ('S n))). IsOrdinal a => SOrdinal a
singOrdinal @b of
      SOrdinal b
SOZ -> r
Ob (a && b) => r
r
      SOS @b' -> forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @_ @a' @b' r
Ob (a && a) => r
Ob (a && b) => r
r

  fst :: forall (a :: ORDINAL ('S ('S n))) (b :: ORDINAL ('S ('S n))).
(Ob a, Ob b) =>
(a && b) ~> a
fst @a @b = case forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S ('S n))). IsOrdinal a => SOrdinal a
singOrdinal @b of
    SOrdinal b
SOZ -> forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @_ @a
    SOS @b' -> case forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S ('S n))). IsOrdinal a => SOrdinal a
singOrdinal @a of
      SOrdinal a
SOZ -> (a && b) ~> a
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ
      SOS @a' -> LTE (a && a) a -> LTE (OS (a && a)) (OS a)
forall {n :: Nat} (b :: ORDINAL ('S n)) (b :: ORDINAL ('S n)).
LTE b b -> LTE (OS b) (OS b)
SLT (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @_ @a' @b')

  snd :: forall (a :: ORDINAL ('S ('S n))) (b :: ORDINAL ('S ('S n))).
(Ob a, Ob b) =>
(a && b) ~> b
snd @a @b = case forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S ('S n))). IsOrdinal a => SOrdinal a
singOrdinal @a of
    SOrdinal a
SOZ -> forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @_ @b
    SOS @a' -> case forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S ('S n))). IsOrdinal a => SOrdinal a
singOrdinal @b of
      SOrdinal b
SOZ -> (a && b) ~> b
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ
      SOS @b' -> LTE (a && a) a -> LTE (OS (a && a)) (OS a)
forall {n :: Nat} (b :: ORDINAL ('S n)) (b :: ORDINAL ('S n)).
LTE b b -> LTE (OS b) (OS b)
SLT (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @_ @a' @b')

  a ~> x
LTE a x
ZEQ &&& :: forall (a :: ORDINAL ('S ('S n))) (x :: ORDINAL ('S ('S n)))
       (y :: ORDINAL ('S ('S n))).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& a ~> y
LTE OZ y
ZEQ = a ~> (x && y)
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ
  ZLT LTE OZ b
_ &&& a ~> y
LTE OZ y
ZEQ = a ~> (x && y)
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ
  a ~> x
LTE a x
ZEQ &&& ZLT LTE OZ b
_ = a ~> (x && y)
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ
  ZLT LTE OZ b
a &&& ZLT LTE OZ b
b = LTE OZ (b && b) -> LTE OZ (OS (b && b))
forall {n :: Nat} (b :: ORDINAL ('S n)). LTE OZ b -> LTE OZ (OS b)
ZLT (OZ ~> b
LTE OZ b
a (OZ ~> b) -> (OZ ~> b) -> OZ ~> (b && b)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall (a :: ORDINAL ('S n)) (x :: ORDINAL ('S n))
       (y :: ORDINAL ('S n)).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& OZ ~> b
LTE OZ b
b)
  SLT LTE a b
a &&& SLT LTE a b
b = LTE a (b && b) -> LTE (OS a) (OS (b && b))
forall {n :: Nat} (b :: ORDINAL ('S n)) (b :: ORDINAL ('S n)).
LTE b b -> LTE (OS b) (OS b)
SLT (a ~> b
LTE a b
a (a ~> b) -> (a ~> b) -> a ~> (b && b)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall (a :: ORDINAL ('S n)) (x :: ORDINAL ('S n))
       (y :: ORDINAL ('S n)).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& a ~> b
LTE a b
b)

-- | The meet as tensor and the top as unit: the cartesian monoidal structure. Like the products it
-- is made of, only for a syntactically concrete @n@. 'MonoidalOrdinal' names the context.
type MonoidalOrdinal :: Nat -> Constraint
type MonoidalOrdinal n = (HasProducts (ORDINAL n), Ob (TerminalObject :: ORDINAL n))

-- The second conjunct looks redundant, since 'Ob' 'TerminalObject' is a superclass of
-- 'HasTerminalObject'. It is not: 'Monoidal' needs @'Ob' 'Unit'@ as a superclass of the instance
-- /declaration/, and GHC does not discharge an instance's own superclasses from the superclasses
-- of its context (see "Undecidable instances and loopy superclasses" in the GHC user's guide).
-- Without it the instance fails with @Could not deduce IsOrdinal TerminalObject@.

instance (MonoidalOrdinal n) => MonoidalProfunctor (LTE :: CAT (ORDINAL n)) where
  one :: LTE Unit Unit
one = LTE Unit Unit
LTE TerminalObject TerminalObject
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: ORDINAL n). Ob a => LTE a a
id
  LTE x1 x2
f ** :: forall (x1 :: ORDINAL n) (x2 :: ORDINAL n) (y1 :: ORDINAL n)
       (y2 :: ORDINAL n).
LTE x1 x2 -> LTE y1 y2 -> LTE (x1 ** y1) (x2 ** y2)
** LTE y1 y2
g = x1 ~> x2
LTE x1 x2
f (x1 ~> x2) -> (y1 ~> y2) -> (x1 && y1) ~> (x2 && y2)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
forall (a :: ORDINAL n) (b :: ORDINAL n) (x :: ORDINAL n)
       (y :: ORDINAL n).
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
*** y1 ~> y2
LTE y1 y2
g

instance (MonoidalOrdinal n) => Monoidal (ORDINAL n) where
  type Unit = TerminalObject
  type a ** b = a && b
  withOb2 :: forall (a :: ORDINAL n) (b :: ORDINAL n) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @a @b = forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @(ORDINAL n) @a @b
  leftUnitor :: forall (a :: ORDINAL n). Ob a => (Unit ** a) ~> a
leftUnitor = (Unit ** a) ~> a
(TerminalObject && a) ~> a
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(TerminalObject && a) ~> a
leftUnitorProd
  leftUnitorInv :: forall (a :: ORDINAL n). Ob a => a ~> (Unit ** a)
leftUnitorInv = a ~> (Unit ** a)
a ~> (TerminalObject && a)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (TerminalObject && a)
leftUnitorProdInv
  rightUnitor :: forall (a :: ORDINAL n). Ob a => (a ** Unit) ~> a
rightUnitor = (a ** Unit) ~> a
(a && TerminalObject) ~> a
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(a && TerminalObject) ~> a
rightUnitorProd
  rightUnitorInv :: forall (a :: ORDINAL n). Ob a => a ~> (a ** Unit)
rightUnitorInv = a ~> (a ** Unit)
a ~> (a && TerminalObject)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (a && TerminalObject)
rightUnitorProdInv
  associator :: forall (a :: ORDINAL n) (b :: ORDINAL n) (c :: ORDINAL n).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @a @b @c = forall {k} (a :: k) (b :: k) (c :: k).
(HasBinaryProducts k, Ob a, Ob b, Ob c) =>
((a && b) && c) ~> (a && (b && c))
forall (a :: ORDINAL n) (b :: ORDINAL n) (c :: ORDINAL n).
(HasBinaryProducts (ORDINAL n), Ob a, Ob b, Ob c) =>
((a && b) && c) ~> (a && (b && c))
associatorProd @a @b @c
  associatorInv :: forall (a :: ORDINAL n) (b :: ORDINAL n) (c :: ORDINAL n).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @a @b @c = forall {k} (a :: k) (b :: k) (c :: k).
(HasBinaryProducts k, Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
forall (a :: ORDINAL n) (b :: ORDINAL n) (c :: ORDINAL n).
(HasBinaryProducts (ORDINAL n), Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
associatorProdInv @a @b @c

instance (MonoidalOrdinal n) => SymMonoidal (ORDINAL n) where
  swap :: forall (a :: ORDINAL n) (b :: ORDINAL n).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @a @b = forall {k} (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> (b && a)
forall (a :: ORDINAL n) (b :: ORDINAL n).
(HasBinaryProducts (ORDINAL n), Ob a, Ob b) =>
(a && b) ~> (b && a)
swapProd @a @b

-- | Every object is a comonoid by the diagonal and the map to the top. So the chain is
-- 'CopyDiscard', and hence 'Proarrow.Category.Monoidal.Cartesian.Cartesian'.
instance (MonoidalOrdinal n, Ob a) => Comonoid (a :: ORDINAL n) where
  counit :: a ~> Unit
counit = a ~> Unit
a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
forall (a :: ORDINAL n). Ob a => a ~> TerminalObject
terminate
  comult :: a ~> (a ** a)
comult = a ~> (a ** a)
a ~> (a && a)
forall {k} (a :: k). (HasBinaryProducts k, Ob a) => a ~> (a && a)
diag

instance (MonoidalOrdinal n, Ob a) => CocommutativeComonoid (a :: ORDINAL n)

instance (MonoidalOrdinal n) => CopyDiscard (ORDINAL n)

instance Distributive (ORDINAL (S Z)) where
  distL :: forall (a :: ORDINAL ('S 'Z)) (b :: ORDINAL ('S 'Z))
       (c :: ORDINAL ('S 'Z)).
(Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL @a @b @c = case (forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S 'Z)). IsOrdinal a => SOrdinal a
singOrdinal @a, forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S 'Z)). IsOrdinal a => SOrdinal a
singOrdinal @b, forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S 'Z)). IsOrdinal a => SOrdinal a
singOrdinal @c) of (SOrdinal a
SOZ, SOrdinal b
SOZ, SOrdinal c
SOZ) -> (a ** (b || c)) ~> ((a ** b) || (a ** c))
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ
  distR :: forall (a :: ORDINAL ('S 'Z)) (b :: ORDINAL ('S 'Z))
       (c :: ORDINAL ('S 'Z)).
(Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR @a @b @c = case (forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S 'Z)). IsOrdinal a => SOrdinal a
singOrdinal @a, forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S 'Z)). IsOrdinal a => SOrdinal a
singOrdinal @b, forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S 'Z)). IsOrdinal a => SOrdinal a
singOrdinal @c) of (SOrdinal a
SOZ, SOrdinal b
SOZ, SOrdinal c
SOZ) -> ((a || b) ** c) ~> ((a ** c) || (b ** c))
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ
  absorbL :: forall (a :: ORDINAL ('S 'Z)).
Ob a =>
(a ** InitialObject) ~> InitialObject
absorbL @a = case forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S 'Z)). IsOrdinal a => SOrdinal a
singOrdinal @a of SOrdinal a
SOZ -> (a ** InitialObject) ~> InitialObject
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ
  absorbR :: forall (a :: ORDINAL ('S 'Z)).
Ob a =>
(InitialObject ** a) ~> InitialObject
absorbR @a = case forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S 'Z)). IsOrdinal a => SOrdinal a
singOrdinal @a of SOrdinal a
SOZ -> (InitialObject ** a) ~> InitialObject
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ

-- | A chain is a distributive lattice: the meet is the minimum and the join the maximum. By
-- recursion on the objects, as the products and coproducts are. A bottom on either side makes
-- both sides the same object, and otherwise both sides are a successor.
instance (Distributive (ORDINAL (S n)), MonoidalOrdinal (S n)) => Distributive (ORDINAL (S (S n))) where
  distL :: forall (a :: ORDINAL ('S ('S n))) (b :: ORDINAL ('S ('S n)))
       (c :: ORDINAL ('S ('S n))).
(Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL @a @b @c = case forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S ('S n))). IsOrdinal a => SOrdinal a
singOrdinal @a of
    SOrdinal a
SOZ -> (a ** (b || c)) ~> ((a ** b) || (a ** c))
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ
    SOS @a' -> case forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S ('S n))). IsOrdinal a => SOrdinal a
singOrdinal @b of
      SOrdinal b
SOZ -> forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @_ @a @c (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: ORDINAL ('S ('S n))).
(CategoryOf (ORDINAL ('S ('S n))), Ob a) =>
Obj a
obj @(a && c))
      SOS @b' -> case forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S ('S n))). IsOrdinal a => SOrdinal a
singOrdinal @c of
        SOrdinal c
SOZ -> forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @_ @a @b (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: ORDINAL ('S ('S n))).
(CategoryOf (ORDINAL ('S ('S n))), Ob a) =>
Obj a
obj @(a && b))
        SOS @c' -> LTE (a && (a || a)) ((a && a) || (a && a))
-> LTE (OS (a && (a || a))) (OS ((a && a) || (a && a)))
forall {n :: Nat} (b :: ORDINAL ('S n)) (b :: ORDINAL ('S n)).
LTE b b -> LTE (OS b) (OS b)
SLT (forall k (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL @_ @a' @b' @c')
  distR :: forall (a :: ORDINAL ('S ('S n))) (b :: ORDINAL ('S ('S n)))
       (c :: ORDINAL ('S ('S n))).
(Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR @a @b @c = case forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S ('S n))). IsOrdinal a => SOrdinal a
singOrdinal @c of
    SOrdinal c
SOZ -> ((a || b) ** c) ~> ((a ** c) || (b ** c))
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ
    SOS @c' -> case forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S ('S n))). IsOrdinal a => SOrdinal a
singOrdinal @a of
      SOrdinal a
SOZ -> forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @_ @b @c (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: ORDINAL ('S ('S n))).
(CategoryOf (ORDINAL ('S ('S n))), Ob a) =>
Obj a
obj @(b && c))
      SOS @a' -> case forall {n :: Nat} (a :: ORDINAL n). IsOrdinal a => SOrdinal a
forall (a :: ORDINAL ('S ('S n))). IsOrdinal a => SOrdinal a
singOrdinal @b of
        SOrdinal b
SOZ -> forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @_ @a @c (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: ORDINAL ('S ('S n))).
(CategoryOf (ORDINAL ('S ('S n))), Ob a) =>
Obj a
obj @(a && c))
        SOS @b' -> LTE ((a || a) && a) ((a && a) || (a && a))
-> LTE (OS ((a || a) && a)) (OS ((a && a) || (a && a)))
forall {n :: Nat} (b :: ORDINAL ('S n)) (b :: ORDINAL ('S n)).
LTE b b -> LTE (OS b) (OS b)
SLT (forall k (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR @_ @a' @b' @c')
  absorbL :: forall (a :: ORDINAL ('S ('S n))).
Ob a =>
(a ** InitialObject) ~> InitialObject
absorbL = (a ** InitialObject) ~> InitialObject
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ
  absorbR :: forall (a :: ORDINAL ('S ('S n))).
Ob a =>
(InitialObject ** a) ~> InitialObject
absorbR = (InitialObject ** a) ~> InitialObject
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ

-- | @LTE@ is thin, so equalizers are trivial. @factorEqualizer incl h@ just needs @h@'s domain to be
-- @<=@ @incl@'s domain. Since both share the codomain @x@, this can only fail when @incl@'s
-- domain is @OZ@ (nothing below it) but @h@'s domain is a successor (necessarily above @OZ@).
instance HasEqualizers (ORDINAL n) where
  equalize :: forall (a :: ORDINAL n) (b :: ORDINAL n) r.
(a ~> b)
-> (a ~> b) -> (forall (e :: ORDINAL n). (e ~> a) -> r) -> r
equalize = (a ~> b)
-> (a ~> b) -> (forall (e :: ORDINAL n). (e ~> a) -> r) -> r
forall {k} (a :: k) (b :: k) r.
Thin k =>
(a ~> b) -> (a ~> b) -> (forall (e :: k). (e ~> a) -> r) -> r
thinEqualize
  factorEqualizer :: forall (e :: ORDINAL n) (x :: ORDINAL n) (e' :: ORDINAL n).
(e ~> x) -> (e' ~> x) -> e' ~> e
factorEqualizer e ~> x
LTE e x
ZEQ e' ~> x
LTE e' OZ
ZEQ = e' ~> e
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ
  factorEqualizer (ZLT LTE OZ b
_) (ZLT LTE OZ b
_) = e' ~> e
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ
  factorEqualizer (SLT @e0 LTE a b
incl) (ZLT LTE OZ b
_) = LTE OZ a -> LTE OZ (OS a)
forall {n :: Nat} (b :: ORDINAL ('S n)). LTE OZ b -> LTE OZ (OS b)
ZLT (forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @_ @e0 ((Ob a, Ob b) => LTE OZ a) -> LTE a b -> LTE OZ a
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: ORDINAL ('S n)) (b :: ORDINAL ('S n)) r.
((Ob a, Ob b) => r) -> LTE a b -> r
\\ LTE a b
incl)
  factorEqualizer (SLT LTE a b
incl) (SLT LTE a b
h) = LTE a a -> LTE (OS a) (OS a)
forall {n :: Nat} (b :: ORDINAL ('S n)) (b :: ORDINAL ('S n)).
LTE b b -> LTE (OS b) (OS b)
SLT ((a ~> b) -> (a ~> b) -> a ~> a
forall k (e :: k) (x :: k) (e' :: k).
HasEqualizers k =>
(e ~> x) -> (e' ~> x) -> e' ~> e
forall (e :: ORDINAL ('S n)) (x :: ORDINAL ('S n))
       (e' :: ORDINAL ('S n)).
(e ~> x) -> (e' ~> x) -> e' ~> e
factorEqualizer a ~> b
LTE a b
incl a ~> b
LTE a b
h)
  factorEqualizer (ZLT LTE OZ b
_) (SLT LTE a b
_) = [Char] -> LTE (OS a) OZ
forall a. HasCallStack => [Char] -> a
P.error [Char]
"factorEqualizer: h's image must lie within incl's image"

-- | Dual to the 'HasEqualizers' instance above.
instance HasCoequalizers (ORDINAL n) where
  coequalize :: forall (a :: ORDINAL n) (b :: ORDINAL n) r.
(a ~> b)
-> (a ~> b) -> (forall (c :: ORDINAL n). (b ~> c) -> r) -> r
coequalize = (a ~> b)
-> (a ~> b) -> (forall (c :: ORDINAL n). (b ~> c) -> r) -> r
forall {k} (a :: k) (b :: k) r.
Thin k =>
(a ~> b) -> (a ~> b) -> (forall (c :: k). (b ~> c) -> r) -> r
thinCoequalize
  factorCoequalizer :: forall (c :: ORDINAL n) (x :: ORDINAL n) (c' :: ORDINAL n).
(x ~> c) -> (x ~> c') -> c ~> c'
factorCoequalizer x ~> c
LTE x c
ZEQ x ~> c'
LTE OZ c'
ZEQ = c ~> c'
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ
  factorCoequalizer x ~> c
LTE x c
ZEQ (ZLT @c0' LTE OZ b
h) = LTE OZ b -> LTE OZ (OS b)
forall {n :: Nat} (b :: ORDINAL ('S n)). LTE OZ b -> LTE OZ (OS b)
ZLT (forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @_ @c0' ((Ob OZ, Ob b) => LTE OZ b) -> LTE OZ b -> LTE OZ b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: ORDINAL ('S n)) (b :: ORDINAL ('S n)) r.
((Ob a, Ob b) => r) -> LTE a b -> r
\\ LTE OZ b
h)
  factorCoequalizer (ZLT LTE OZ b
_) x ~> c'
LTE OZ c'
ZEQ = [Char] -> LTE (OS b) OZ
forall a. HasCallStack => [Char] -> a
P.error [Char]
"factorCoequalizer: h must be constant on q's fibers"
  factorCoequalizer (ZLT LTE OZ b
q) (ZLT LTE OZ b
h) = LTE b b -> LTE (OS b) (OS b)
forall {n :: Nat} (b :: ORDINAL ('S n)) (b :: ORDINAL ('S n)).
LTE b b -> LTE (OS b) (OS b)
SLT ((OZ ~> b) -> (OZ ~> b) -> b ~> b
forall k (c :: k) (x :: k) (c' :: k).
HasCoequalizers k =>
(x ~> c) -> (x ~> c') -> c ~> c'
forall (c :: ORDINAL ('S n)) (x :: ORDINAL ('S n))
       (c' :: ORDINAL ('S n)).
(x ~> c) -> (x ~> c') -> c ~> c'
factorCoequalizer OZ ~> b
LTE OZ b
q OZ ~> b
LTE OZ b
h)
  factorCoequalizer (SLT LTE a b
q) (SLT LTE a b
h) = LTE b b -> LTE (OS b) (OS b)
forall {n :: Nat} (b :: ORDINAL ('S n)) (b :: ORDINAL ('S n)).
LTE b b -> LTE (OS b) (OS b)
SLT ((a ~> b) -> (a ~> b) -> b ~> b
forall k (c :: k) (x :: k) (c' :: k).
HasCoequalizers k =>
(x ~> c) -> (x ~> c') -> c ~> c'
forall (c :: ORDINAL ('S n)) (x :: ORDINAL ('S n))
       (c' :: ORDINAL ('S n)).
(x ~> c) -> (x ~> c') -> c ~> c'
factorCoequalizer a ~> b
LTE a b
q a ~> b
LTE a b
h)

-- | Pullbacks in a thin category are just meets. Computed directly, not via
-- 'Proarrow.Limit.Pullback.thinPullback', which would need @HasProducts (ORDINAL n)@. That is
-- unavailable for an abstract @n@, since 'HasBinaryProducts' and 'HasTerminalObject' are only
-- resolvable for a syntactically concrete @n@.
instance HasPullbacks (ORDINAL n) where
  pullback :: forall (o :: ORDINAL n) (a :: ORDINAL n) (b :: ORDINAL n) r.
(a ~> o)
-> (b ~> o)
-> (forall (p :: ORDINAL n). (p ~> a) -> (p ~> b) -> r)
-> r
pullback (ZLT LTE OZ b
_) (ZLT LTE OZ b
_) forall (p :: ORDINAL n). (p ~> a) -> (p ~> b) -> r
k = (OZ ~> a) -> (OZ ~> b) -> r
forall (p :: ORDINAL n). (p ~> a) -> (p ~> b) -> r
k OZ ~> a
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ OZ ~> b
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ
  pullback (ZLT LTE OZ b
_) (SLT @b' LTE a b
g) forall (p :: ORDINAL n). (p ~> a) -> (p ~> b) -> r
k = (OZ ~> a) -> (OZ ~> b) -> r
forall (p :: ORDINAL n). (p ~> a) -> (p ~> b) -> r
k OZ ~> a
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ (LTE OZ a -> LTE OZ (OS a)
forall {n :: Nat} (b :: ORDINAL ('S n)). LTE OZ b -> LTE OZ (OS b)
ZLT (forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @_ @b' ((Ob a, Ob b) => LTE OZ a) -> LTE a b -> LTE OZ a
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: ORDINAL ('S n)) (b :: ORDINAL ('S n)) r.
((Ob a, Ob b) => r) -> LTE a b -> r
\\ LTE a b
g))
  pullback (SLT @a' LTE a b
f) (ZLT LTE OZ b
_) forall (p :: ORDINAL n). (p ~> a) -> (p ~> b) -> r
k = (OZ ~> a) -> (OZ ~> b) -> r
forall (p :: ORDINAL n). (p ~> a) -> (p ~> b) -> r
k (LTE OZ a -> LTE OZ (OS a)
forall {n :: Nat} (b :: ORDINAL ('S n)). LTE OZ b -> LTE OZ (OS b)
ZLT (forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @_ @a' ((Ob a, Ob b) => LTE OZ a) -> LTE a b -> LTE OZ a
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: ORDINAL ('S n)) (b :: ORDINAL ('S n)) r.
((Ob a, Ob b) => r) -> LTE a b -> r
\\ LTE a b
f)) OZ ~> b
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ
  pullback (SLT LTE a b
f) (SLT LTE a b
g) forall (p :: ORDINAL n). (p ~> a) -> (p ~> b) -> r
k = (a ~> b)
-> (a ~> b)
-> (forall (p :: ORDINAL ('S n)). (p ~> a) -> (p ~> a) -> r)
-> r
forall k (o :: k) (a :: k) (b :: k) r.
HasPullbacks k =>
(a ~> o)
-> (b ~> o) -> (forall (p :: k). (p ~> a) -> (p ~> b) -> r) -> r
forall (o :: ORDINAL ('S n)) (a :: ORDINAL ('S n))
       (b :: ORDINAL ('S n)) r.
(a ~> o)
-> (b ~> o)
-> (forall (p :: ORDINAL ('S n)). (p ~> a) -> (p ~> b) -> r)
-> r
pullback a ~> b
LTE a b
f a ~> b
LTE a b
g \p ~> a
p1 p ~> a
p2 -> (OS p ~> a) -> (OS p ~> b) -> r
forall (p :: ORDINAL n). (p ~> a) -> (p ~> b) -> r
k (LTE p a -> LTE (OS p) (OS a)
forall {n :: Nat} (b :: ORDINAL ('S n)) (b :: ORDINAL ('S n)).
LTE b b -> LTE (OS b) (OS b)
SLT p ~> a
LTE p a
p1) (LTE p a -> LTE (OS p) (OS a)
forall {n :: Nat} (b :: ORDINAL ('S n)) (b :: ORDINAL ('S n)).
LTE b b -> LTE (OS b) (OS b)
SLT p ~> a
LTE p a
p2)
  pullback a ~> o
LTE a o
ZEQ b ~> o
LTE b OZ
ZEQ forall (p :: ORDINAL n). (p ~> a) -> (p ~> b) -> r
k = (OZ ~> a) -> (OZ ~> b) -> r
forall (p :: ORDINAL n). (p ~> a) -> (p ~> b) -> r
k OZ ~> a
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ OZ ~> b
LTE OZ OZ
forall {n :: Nat}. LTE OZ OZ
ZEQ

  -- @p1@ and @k1@ already share a codomain (@a@), which is all 'factorEqualizer' needs to compare
  -- @q@ against @p@. @p2@/@k2@ carry no extra information once @p1, p2@ are known to be a pullback.
  factorPullback :: forall (a :: ORDINAL n) (b :: ORDINAL n) (p :: ORDINAL n)
       (q :: ORDINAL n).
(p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p
factorPullback p ~> a
p1 p ~> b
_ q ~> a
k1 q ~> b
_ = (p ~> a) -> (q ~> a) -> q ~> p
forall k (e :: k) (x :: k) (e' :: k).
HasEqualizers k =>
(e ~> x) -> (e' ~> x) -> e' ~> e
forall (e :: ORDINAL n) (x :: ORDINAL n) (e' :: ORDINAL n).
(e ~> x) -> (e' ~> x) -> e' ~> e
factorEqualizer p ~> a
p1 q ~> a
k1

-- | Dual to the 'HasPullbacks' instance above: pushouts in a thin category are joins.
instance HasPushouts (ORDINAL n) where
  pushout :: forall (o :: ORDINAL n) (a :: ORDINAL n) (b :: ORDINAL n) r.
(o ~> a)
-> (o ~> b)
-> (forall (p :: ORDINAL n). (a ~> p) -> (b ~> p) -> r)
-> r
pushout o ~> a
LTE o a
ZEQ o ~> b
g forall (p :: ORDINAL n). (a ~> p) -> (b ~> p) -> r
k = (a ~> b) -> (b ~> b) -> r
forall (p :: ORDINAL n). (a ~> p) -> (b ~> p) -> r
k o ~> b
a ~> b
g (LTE b b
(Ob OZ, Ob b) => LTE b b
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: ORDINAL n). Ob a => LTE a a
id ((Ob OZ, Ob b) => LTE b b) -> LTE OZ b -> LTE b b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: ORDINAL ('S n)) (b :: ORDINAL n) r.
((Ob a, Ob b) => r) -> LTE a b -> r
\\ o ~> b
LTE OZ b
g)
  pushout o ~> a
f o ~> b
LTE o b
ZEQ forall (p :: ORDINAL n). (a ~> p) -> (b ~> p) -> r
k = (a ~> a) -> (b ~> a) -> r
forall (p :: ORDINAL n). (a ~> p) -> (b ~> p) -> r
k (LTE a a
(Ob OZ, Ob a) => LTE a a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: ORDINAL n). Ob a => LTE a a
id ((Ob OZ, Ob a) => LTE a a) -> LTE OZ a -> LTE a a
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: ORDINAL ('S n)) (b :: ORDINAL n) r.
((Ob a, Ob b) => r) -> LTE a b -> r
\\ o ~> a
LTE OZ a
f) o ~> a
b ~> a
f
  pushout (ZLT LTE OZ b
f) (ZLT LTE OZ b
g) forall (p :: ORDINAL n). (a ~> p) -> (b ~> p) -> r
k = (OZ ~> b)
-> (OZ ~> b)
-> (forall (p :: ORDINAL ('S n)). (b ~> p) -> (b ~> p) -> r)
-> r
forall k (o :: k) (a :: k) (b :: k) r.
HasPushouts k =>
(o ~> a)
-> (o ~> b) -> (forall (p :: k). (a ~> p) -> (b ~> p) -> r) -> r
forall (o :: ORDINAL ('S n)) (a :: ORDINAL ('S n))
       (b :: ORDINAL ('S n)) r.
(o ~> a)
-> (o ~> b)
-> (forall (p :: ORDINAL ('S n)). (a ~> p) -> (b ~> p) -> r)
-> r
pushout OZ ~> b
LTE OZ b
f OZ ~> b
LTE OZ b
g \b ~> p
q1 b ~> p
q2 -> (a ~> OS p) -> (b ~> OS p) -> r
forall (p :: ORDINAL n). (a ~> p) -> (b ~> p) -> r
k (LTE b p -> LTE (OS b) (OS p)
forall {n :: Nat} (b :: ORDINAL ('S n)) (b :: ORDINAL ('S n)).
LTE b b -> LTE (OS b) (OS b)
SLT b ~> p
LTE b p
q1) (LTE b p -> LTE (OS b) (OS p)
forall {n :: Nat} (b :: ORDINAL ('S n)) (b :: ORDINAL ('S n)).
LTE b b -> LTE (OS b) (OS b)
SLT b ~> p
LTE b p
q2)
  pushout (SLT LTE a b
f) (SLT LTE a b
g) forall (p :: ORDINAL n). (a ~> p) -> (b ~> p) -> r
k = (a ~> b)
-> (a ~> b)
-> (forall (p :: ORDINAL ('S n)). (b ~> p) -> (b ~> p) -> r)
-> r
forall k (o :: k) (a :: k) (b :: k) r.
HasPushouts k =>
(o ~> a)
-> (o ~> b) -> (forall (p :: k). (a ~> p) -> (b ~> p) -> r) -> r
forall (o :: ORDINAL ('S n)) (a :: ORDINAL ('S n))
       (b :: ORDINAL ('S n)) r.
(o ~> a)
-> (o ~> b)
-> (forall (p :: ORDINAL ('S n)). (a ~> p) -> (b ~> p) -> r)
-> r
pushout a ~> b
LTE a b
f a ~> b
LTE a b
g \b ~> p
q1 b ~> p
q2 -> (a ~> OS p) -> (b ~> OS p) -> r
forall (p :: ORDINAL n). (a ~> p) -> (b ~> p) -> r
k (LTE b p -> LTE (OS b) (OS p)
forall {n :: Nat} (b :: ORDINAL ('S n)) (b :: ORDINAL ('S n)).
LTE b b -> LTE (OS b) (OS b)
SLT b ~> p
LTE b p
q1) (LTE b p -> LTE (OS b) (OS p)
forall {n :: Nat} (b :: ORDINAL ('S n)) (b :: ORDINAL ('S n)).
LTE b b -> LTE (OS b) (OS b)
SLT b ~> p
LTE b p
q2)

  factorPushout :: forall (a :: ORDINAL n) (b :: ORDINAL n) (p :: ORDINAL n)
       (q :: ORDINAL n).
(a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q
factorPushout a ~> p
p1 b ~> p
_ a ~> q
k1 b ~> q
_ = (a ~> p) -> (a ~> q) -> p ~> q
forall k (c :: k) (x :: k) (c' :: k).
HasCoequalizers k =>
(x ~> c) -> (x ~> c') -> c ~> c'
forall (c :: ORDINAL n) (x :: ORDINAL n) (c' :: ORDINAL n).
(x ~> c) -> (x ~> c') -> c ~> c'
factorCoequalizer a ~> p
p1 a ~> q
k1

instance HasEpiMonoFactorization (ORDINAL n)