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

import Data.Kind (Constraint, Type)

import Proarrow.Category.Enriched.Thin (ThinProfunctor (..))
import Proarrow.Category.Topos (HasEpiMonoFactorization (..), defaultFactorize)
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 (..))
import Proarrow.Limit.Equalizer (HasEqualizers (..), thinEqualize)
import Proarrow.Limit.Pullback (HasPullbacks (..))
import Proarrow.Limit.Terminal (HasTerminalObject (..))
import Prelude qualified as P

type data NAT = Z | S NAT

type data FIN n where
  FZ :: FIN (S n)
  FS :: FIN (S n) -> FIN (S (S n))

type FIN0 = FIN Z
type FIN1 = FIN (S Z)
type FIN2 = FIN (S (S Z))
type FIN3 = FIN (S (S (S Z)))

type SFin :: forall {n :: NAT}. FIN n -> Type
data SFin a where
  SZ :: SFin FZ
  SS :: (IsFin a) => SFin (FS a)

type LTE :: forall {n :: NAT}. CAT (FIN n)
data LTE a b where
  ZEQ :: LTE FZ FZ
  ZLT :: LTE FZ b -> LTE FZ (FS b)
  SLT :: LTE a b -> LTE (FS a) (FS b)

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

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

type IsFin :: forall {n :: NAT}. FIN n -> Constraint
class IsFin (a :: FIN n) where
  singFin :: SFin a
instance IsFin (a :: FIN Z) where
  singFin :: SFin a
singFin = SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin
instance IsFin FZ where
  singFin :: SFin FZ
singFin = SFin FZ
forall (n :: NAT). SFin FZ
SZ
instance (IsFin b) => IsFin (FS b) where
  singFin :: SFin (FS b)
singFin = SFin (FS b)
forall (n :: NAT) (b :: FIN (S n)). IsFin b => SFin (FS b)
SS

instance Profunctor LTE where
  dimap :: forall (c :: FIN n) (a :: FIN n) (b :: FIN n) (d :: FIN 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 :: k +-> 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 :: FIN n) (b :: FIN 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 FZ b
b = r
(Ob a, Ob b) => r
(Ob FZ, Ob b) => r
r ((Ob FZ, Ob b) => r) -> LTE FZ 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 :: FIN (S n)) (b :: FIN (S n)) r.
((Ob a, Ob b) => r) -> LTE a b -> r
\\ LTE FZ 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 :: FIN (S n)) (b :: FIN (S n)) r.
((Ob a, Ob b) => r) -> LTE a b -> r
\\ LTE a b
ab
instance Promonad LTE where
  id :: forall (a :: FIN n). Ob a => LTE a a
id @a = case forall (a :: FIN n). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @a of
    SFin a
SZ -> LTE a a
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
    SFin a
SS -> LTE a a -> LTE (FS a) (FS a)
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS b)
SLT LTE a a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: FIN (S n)). Ob a => LTE a a
id
  LTE b c
ZEQ . :: forall (b :: FIN n) (c :: FIN n) (a :: FIN n).
LTE b c -> LTE a b -> LTE a c
. LTE a b
ZEQ = LTE a c
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
  ZLT LTE FZ b
b . LTE a b
ZEQ = LTE FZ b -> LTE FZ (FS b)
forall {n :: NAT} (b :: FIN (S n)). LTE FZ b -> LTE FZ (FS b)
ZLT LTE FZ b
b
  SLT LTE a b
ab . ZLT LTE FZ b
za = LTE FZ b -> LTE FZ (FS b)
forall {n :: NAT} (b :: FIN (S n)). LTE FZ b -> LTE FZ (FS b)
ZLT (LTE a b
ab LTE a b -> LTE FZ a -> LTE FZ b
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: FIN (S n)) (c :: FIN (S n)) (a :: FIN (S n)).
LTE b c -> LTE a b -> LTE a c
. LTE FZ a
LTE FZ b
za)
  SLT LTE a b
ab . SLT LTE a b
bc = LTE a b -> LTE (FS a) (FS b)
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS b)
SLT (LTE a b
ab LTE a b -> LTE a a -> LTE a b
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: FIN (S n)) (c :: FIN (S n)) (a :: FIN (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 (FIN n) where
  type (~>) = LTE
  type Ob a = IsFin a

class IsLTE (a :: FIN n) (b :: FIN n) where
  lte :: a ~> b
instance IsLTE FZ FZ where
  lte :: FZ ~> FZ
lte = FZ ~> FZ
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
instance (IsLTE FZ b) => IsLTE FZ (FS b) where
  lte :: FZ ~> FS b
lte = LTE FZ b -> LTE FZ (FS b)
forall {n :: NAT} (b :: FIN (S n)). LTE FZ b -> LTE FZ (FS b)
ZLT FZ ~> b
LTE FZ b
forall (n :: NAT) (a :: FIN n) (b :: FIN n). IsLTE a b => a ~> b
lte
instance (IsLTE a b) => IsLTE (FS a) (FS b) where
  lte :: FS a ~> FS b
lte = LTE a b -> LTE (FS a) (FS b)
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS b)
SLT a ~> b
LTE a b
forall (n :: NAT) (a :: FIN n) (b :: FIN n). IsLTE a b => a ~> b
lte
instance ThinProfunctor LTE where
  type HasArrow LTE a b = IsLTE a b
  arr :: forall (a :: FIN n) (b :: FIN n).
(Ob a, Ob b, HasArrow LTE a b) =>
LTE a b
arr = a ~> b
LTE a b
forall (n :: NAT) (a :: FIN n) (b :: FIN n). IsLTE a b => a ~> b
lte
  withArr :: forall (a :: FIN n) (b :: FIN n) r.
LTE a b -> ((HasArrow LTE a b, Ob a, Ob b) => r) -> r
withArr LTE a b
ZEQ (HasArrow LTE a b, Ob a, Ob b) => r
r = r
(HasArrow LTE a b, Ob a, Ob b) => r
r
  withArr (ZLT LTE FZ b
b) (HasArrow LTE a b, Ob a, Ob b) => r
r = LTE FZ b -> ((HasArrow LTE FZ b, Ob FZ, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
forall (a :: FIN (S n)) (b :: FIN (S n)) r.
LTE a b -> ((HasArrow LTE a b, Ob a, Ob b) => r) -> r
withArr LTE FZ b
b r
(HasArrow LTE a b, Ob a, Ob b) => r
(HasArrow LTE FZ b, Ob FZ, Ob b) => r
r
  withArr (SLT LTE a b
ab) (HasArrow LTE a b, Ob a, Ob b) => r
r = LTE a b -> ((HasArrow LTE a b, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
forall (a :: FIN (S n)) (b :: FIN (S n)) r.
LTE a b -> ((HasArrow LTE a b, Ob a, Ob b) => r) -> r
withArr LTE a b
ab r
(HasArrow LTE a b, Ob a, Ob b) => r
(HasArrow LTE a b, Ob a, Ob b) => r
r

instance HasInitialObject (FIN (S n)) where
  type InitialObject = FZ
  initiate :: forall (a :: FIN (S n)). Ob a => InitialObject ~> a
initiate @a = case forall (a :: FIN (S n)). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @a of
    SFin a
SZ -> InitialObject ~> a
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
    SS @a' -> LTE FZ a -> LTE FZ (FS a)
forall {n :: NAT} (b :: FIN (S n)). LTE FZ b -> LTE FZ (FS b)
ZLT (forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @_ @a')

instance HasTerminalObject (FIN (S Z)) where
  type TerminalObject = FZ
  terminate :: forall (a :: FIN (S Z)). Ob a => a ~> TerminalObject
terminate @a = case forall (a :: FIN (S Z)). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @a of SFin a
SZ -> a ~> TerminalObject
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ

instance (HasTerminalObject (FIN (S n))) => HasTerminalObject (FIN (S (S n))) where
  type TerminalObject = FS TerminalObject
  terminate :: forall (a :: FIN (S (S n))). Ob a => a ~> TerminalObject
terminate @a = case forall (a :: FIN (S (S n))). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @a of
    SFin a
SZ -> LTE FZ TerminalObject -> LTE FZ (FS TerminalObject)
forall {n :: NAT} (b :: FIN (S n)). LTE FZ b -> LTE FZ (FS b)
ZLT FZ ~> TerminalObject
LTE FZ TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
forall (a :: FIN (S n)). Ob a => a ~> TerminalObject
terminate
    SS @a' -> LTE a TerminalObject -> LTE (FS a) (FS TerminalObject)
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS b)
SLT (forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate @_ @a')

instance HasBinaryCoproducts (FIN Z) where
  type a || b = a
  withObCoprod :: forall (a :: FIN Z) (b :: FIN 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 :: FIN Z) (b :: FIN Z). (Ob a, Ob b) => a ~> (a || b)
lft = a ~> a
a ~> (a || b)
forall (a :: FIN Z) (b :: FIN Z). a ~> b
absurdR
  rgt :: forall (a :: FIN Z) (b :: FIN Z). (Ob a, Ob b) => b ~> (a || b)
rgt = b ~> a
b ~> (a || b)
forall (a :: FIN Z) (b :: FIN Z). a ~> b
absurdR
  ||| :: forall (x :: FIN Z) (a :: FIN Z) (y :: FIN Z).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
(|||) = \case {}

instance HasBinaryCoproducts (FIN (S Z)) where
  type FZ || FZ = FZ
  withObCoprod :: forall (a :: FIN (S Z)) (b :: FIN (S Z)) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @a @b Ob (a || b) => r
r = case (forall (a :: FIN (S Z)). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @a, forall (a :: FIN (S Z)). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @b) of (SFin a
SZ, SFin b
SZ) -> r
Ob (a || b) => r
r
  lft :: forall (a :: FIN (S Z)) (b :: FIN (S Z)).
(Ob a, Ob b) =>
a ~> (a || b)
lft @a @b = case (forall (a :: FIN (S Z)). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @a, forall (a :: FIN (S Z)). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @b) of (SFin a
SZ, SFin b
SZ) -> a ~> (a || b)
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
  rgt :: forall (a :: FIN (S Z)) (b :: FIN (S Z)).
(Ob a, Ob b) =>
b ~> (a || b)
rgt @a @b = case (forall (a :: FIN (S Z)). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @a, forall (a :: FIN (S Z)). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @b) of (SFin a
SZ, SFin b
SZ) -> b ~> (a || b)
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
  x ~> a
LTE x a
ZEQ ||| :: forall (x :: FIN (S Z)) (a :: FIN (S Z)) (y :: FIN (S Z)).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| y ~> a
LTE y FZ
ZEQ = (x || y) ~> a
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ

-- | Maximum
instance (HasBinaryCoproducts (FIN (S n))) => HasBinaryCoproducts (FIN (S (S n))) where
  type FZ || b = b
  type a || FZ = a
  type FS a || FS b = FS (a || b)
  withObCoprod :: forall (a :: FIN (S (S n))) (b :: FIN (S (S n))) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @a @b Ob (a || b) => r
r = case forall (a :: FIN (S (S n))). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @a of
    SFin a
SZ -> r
Ob (a || b) => r
r
    SS @a' -> case forall (a :: FIN (S (S n))). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @b of
      SFin b
SZ -> r
Ob (a || b) => r
r
      SS @b' -> forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @(FIN (S n)) @a' @b' r
Ob (a || a) => r
Ob (a || b) => r
r

  lft :: forall (a :: FIN (S (S n))) (b :: FIN (S (S n))).
(Ob a, Ob b) =>
a ~> (a || b)
lft @a @b = case forall (a :: FIN (S (S n))). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @b of
    SFin b
SZ -> forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: FIN (S (S n))).
(CategoryOf (FIN (S (S n))), Ob a) =>
Obj a
obj @a
    SS @b' -> case forall (a :: FIN (S (S n))). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @a of
      SFin a
SZ -> LTE FZ a -> LTE FZ (FS a)
forall {n :: NAT} (b :: FIN (S n)). LTE FZ b -> LTE FZ (FS b)
ZLT (forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @_ @b')
      SS @a' -> LTE a (a || a) -> LTE (FS a) (FS (a || a))
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS b)
SLT (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @_ @a' @b')

  rgt :: forall (a :: FIN (S (S n))) (b :: FIN (S (S n))).
(Ob a, Ob b) =>
b ~> (a || b)
rgt @a @b = case forall (a :: FIN (S (S n))). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @a of
    SFin a
SZ -> forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: FIN (S (S n))).
(CategoryOf (FIN (S (S n))), Ob a) =>
Obj a
obj @b
    SS @a' -> case forall (a :: FIN (S (S n))). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @b of
      SFin b
SZ -> LTE FZ a -> LTE FZ (FS a)
forall {n :: NAT} (b :: FIN (S n)). LTE FZ b -> LTE FZ (FS b)
ZLT (forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @_ @a')
      SS @b' -> LTE a (a || a) -> LTE (FS a) (FS (a || a))
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS 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 :: FIN (S (S n))) (a :: FIN (S (S n)))
       (y :: FIN (S (S n))).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| y ~> a
LTE y FZ
ZEQ = (x || y) ~> a
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
  ZLT LTE FZ b
ZEQ ||| y ~> a
a = y ~> a
(x || y) ~> a
a
  x ~> a
a ||| ZLT LTE FZ b
ZEQ = x ~> a
(x || y) ~> a
a
  ZLT a :: LTE FZ b
a@ZLT{} ||| ZLT b :: LTE FZ b
b@ZLT{} = LTE FZ (FS b) -> LTE FZ (FS (FS b))
forall {n :: NAT} (b :: FIN (S n)). LTE FZ b -> LTE FZ (FS b)
ZLT (FZ ~> FS b
LTE FZ b
a (FZ ~> FS b) -> (FZ ~> FS b) -> (FZ || FZ) ~> FS b
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall (x :: FIN (S (S n))) (a :: FIN (S (S n)))
       (y :: FIN (S (S n))).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| FZ ~> FS b
LTE FZ b
b)
  ZLT a :: LTE FZ b
a@ZLT{} ||| SLT LTE a b
bc = LTE (FZ || a) (FS b) -> LTE (FS (FZ || a)) (FS (FS b))
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS b)
SLT (FZ ~> FS b
LTE FZ b
a (FZ ~> FS b) -> (a ~> FS b) -> (FZ || a) ~> FS b
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall (x :: FIN (S (S n))) (a :: FIN (S (S n)))
       (y :: FIN (S (S n))).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| a ~> FS b
LTE a b
bc)
  SLT LTE a b
ab ||| ZLT c :: LTE FZ b
c@ZLT{} = LTE (a || FZ) (FS b) -> LTE (FS (a || FZ)) (FS (FS b))
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS b)
SLT (a ~> FS b
LTE a b
ab (a ~> FS b) -> (FZ ~> FS b) -> (a || FZ) ~> FS b
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall (x :: FIN (S (S n))) (a :: FIN (S (S n)))
       (y :: FIN (S (S n))).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| FZ ~> FS b
LTE FZ b
c)
  SLT LTE a b
a ||| SLT LTE a b
b = LTE (a || a) b -> LTE (FS (a || a)) (FS b)
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS 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 :: FIN (S n)) (a :: FIN (S n)) (y :: FIN (S n)).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| a ~> b
LTE a b
b)

instance HasBinaryProducts (FIN Z) where
  type a && b = a
  withObProd :: forall (a :: FIN Z) (b :: FIN 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 :: FIN Z) (b :: FIN Z). (Ob a, Ob b) => (a && b) ~> a
fst = a ~> a
(a && b) ~> a
forall (a :: FIN Z) (b :: FIN Z). a ~> b
absurdR
  snd :: forall (a :: FIN Z) (b :: FIN Z). (Ob a, Ob b) => (a && b) ~> b
snd = a ~> b
(a && b) ~> b
forall (a :: FIN Z) (b :: FIN Z). a ~> b
absurdR
  &&& :: forall (a :: FIN Z) (x :: FIN Z) (y :: FIN Z).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
(&&&) = \case {}

instance HasBinaryProducts (FIN (S Z)) where
  type FZ && FZ = FZ
  withObProd :: forall (a :: FIN (S Z)) (b :: FIN (S Z)) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @a @b Ob (a && b) => r
r = case (forall (a :: FIN (S Z)). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @a, forall (a :: FIN (S Z)). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @b) of (SFin a
SZ, SFin b
SZ) -> r
Ob (a && b) => r
r
  fst :: forall (a :: FIN (S Z)) (b :: FIN (S Z)).
(Ob a, Ob b) =>
(a && b) ~> a
fst @a @b = case (forall (a :: FIN (S Z)). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @a, forall (a :: FIN (S Z)). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @b) of (SFin a
SZ, SFin b
SZ) -> (a && b) ~> a
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
  snd :: forall (a :: FIN (S Z)) (b :: FIN (S Z)).
(Ob a, Ob b) =>
(a && b) ~> b
snd @a @b = case (forall (a :: FIN (S Z)). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @a, forall (a :: FIN (S Z)). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @b) of (SFin a
SZ, SFin b
SZ) -> (a && b) ~> b
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
  a ~> x
LTE a x
ZEQ &&& :: forall (a :: FIN (S Z)) (x :: FIN (S Z)) (y :: FIN (S Z)).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& a ~> y
LTE FZ y
ZEQ = a ~> (x && y)
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ

-- | Minimum
instance (HasBinaryProducts (FIN (S n))) => HasBinaryProducts (FIN (S (S n))) where
  type FZ && b = FZ
  type a && FZ = FZ
  type FS a && FS b = FS (a && b)
  withObProd :: forall (a :: FIN (S (S n))) (b :: FIN (S (S n))) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @a @b Ob (a && b) => r
r = case forall (a :: FIN (S (S n))). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @a of
    SFin a
SZ -> r
Ob (a && b) => r
r
    SS @a' -> case forall (a :: FIN (S (S n))). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @b of
      SFin b
SZ -> r
Ob (a && b) => r
r
      SS @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 :: FIN (S (S n))) (b :: FIN (S (S n))).
(Ob a, Ob b) =>
(a && b) ~> a
fst @a @b = case forall (a :: FIN (S (S n))). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @b of
    SFin b
SZ -> forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @_ @a
    SS @b' -> case forall (a :: FIN (S (S n))). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @a of
      SFin a
SZ -> (a && b) ~> a
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
      SS @a' -> LTE (a && a) a -> LTE (FS (a && a)) (FS a)
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS b)
SLT (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @_ @a' @b')

  snd :: forall (a :: FIN (S (S n))) (b :: FIN (S (S n))).
(Ob a, Ob b) =>
(a && b) ~> b
snd @a @b = case forall (a :: FIN (S (S n))). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @a of
    SFin a
SZ -> forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @_ @b
    SS @a' -> case forall (a :: FIN (S (S n))). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @b of
      SFin b
SZ -> (a && b) ~> b
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
      SS @b' -> LTE (a && a) a -> LTE (FS (a && a)) (FS a)
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS 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 :: FIN (S (S n))) (x :: FIN (S (S n)))
       (y :: FIN (S (S n))).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& a ~> y
LTE FZ y
ZEQ = a ~> (x && y)
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
  ZLT LTE FZ b
_ &&& a ~> y
LTE FZ y
ZEQ = a ~> (x && y)
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
  a ~> x
LTE a x
ZEQ &&& ZLT LTE FZ b
_ = a ~> (x && y)
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
  ZLT LTE FZ b
a &&& ZLT LTE FZ b
b = LTE FZ (b && b) -> LTE FZ (FS (b && b))
forall {n :: NAT} (b :: FIN (S n)). LTE FZ b -> LTE FZ (FS b)
ZLT (FZ ~> b
LTE FZ b
a (FZ ~> b) -> (FZ ~> b) -> FZ ~> (b && b)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall (a :: FIN (S n)) (x :: FIN (S n)) (y :: FIN (S n)).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& FZ ~> b
LTE FZ b
b)
  SLT LTE a b
a &&& SLT LTE a b
b = LTE a (b && b) -> LTE (FS a) (FS (b && b))
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS 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 :: FIN (S n)) (x :: FIN (S n)) (y :: FIN (S n)).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& a ~> b
LTE a b
b)

-- | @LTE@ is thin, so equalizers are trivial; @factorEqualizer incl h@ just needs @h@'s domain to be
-- @<=@ @incl@'s domain, which -- since both share the codomain @x@ -- can only fail when @incl@'s
-- domain is @FZ@ (nothing below it) but @h@'s domain is a successor (necessarily above @FZ@).
instance HasEqualizers (FIN n) where
  equalize :: forall (a :: FIN n) (b :: FIN n) r.
(a ~> b) -> (a ~> b) -> (forall (e :: FIN n). (e ~> a) -> r) -> r
equalize = (a ~> b) -> (a ~> b) -> (forall (e :: FIN 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 :: FIN n) (x :: FIN n) (e' :: FIN n).
(e ~> x) -> (e' ~> x) -> e' ~> e
factorEqualizer e ~> x
LTE e x
ZEQ e' ~> x
LTE e' FZ
ZEQ = e' ~> e
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
  factorEqualizer (ZLT LTE FZ b
_) (ZLT LTE FZ b
_) = e' ~> e
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
  factorEqualizer (SLT @e0 LTE a b
incl) (ZLT LTE FZ b
_) = LTE FZ a -> LTE FZ (FS a)
forall {n :: NAT} (b :: FIN (S n)). LTE FZ b -> LTE FZ (FS b)
ZLT (forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @_ @e0 ((Ob a, Ob b) => LTE FZ a) -> LTE a b -> LTE FZ 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 :: FIN (S n)) (b :: FIN (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 (FS a) (FS a)
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS 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 :: FIN (S n)) (x :: FIN (S n)) (e' :: FIN (S n)).
(e ~> x) -> (e' ~> x) -> e' ~> e
factorEqualizer a ~> b
LTE a b
incl a ~> b
LTE a b
h)
  factorEqualizer (ZLT LTE FZ b
_) (SLT LTE a b
_) = [Char] -> LTE (FS a) FZ
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 (FIN n) where
  coequalize :: forall (a :: FIN n) (b :: FIN n) r.
(a ~> b) -> (a ~> b) -> (forall (c :: FIN n). (b ~> c) -> r) -> r
coequalize = (a ~> b) -> (a ~> b) -> (forall (c :: FIN 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 :: FIN n) (x :: FIN n) (c' :: FIN n).
(x ~> c) -> (x ~> c') -> c ~> c'
factorCoequalizer x ~> c
LTE x c
ZEQ x ~> c'
LTE FZ c'
ZEQ = c ~> c'
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
  factorCoequalizer x ~> c
LTE x c
ZEQ (ZLT @c0' LTE FZ b
h) = LTE FZ b -> LTE FZ (FS b)
forall {n :: NAT} (b :: FIN (S n)). LTE FZ b -> LTE FZ (FS b)
ZLT (forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @_ @c0' ((Ob FZ, Ob b) => LTE FZ b) -> LTE FZ b -> LTE FZ 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 :: FIN (S n)) (b :: FIN (S n)) r.
((Ob a, Ob b) => r) -> LTE a b -> r
\\ LTE FZ b
h)
  factorCoequalizer (ZLT LTE FZ b
_) x ~> c'
LTE FZ c'
ZEQ = [Char] -> LTE (FS b) FZ
forall a. HasCallStack => [Char] -> a
P.error [Char]
"factorCoequalizer: h must be constant on q's fibers"
  factorCoequalizer (ZLT LTE FZ b
q) (ZLT LTE FZ b
h) = LTE b b -> LTE (FS b) (FS b)
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS b)
SLT ((FZ ~> b) -> (FZ ~> b) -> b ~> b
forall k (c :: k) (x :: k) (c' :: k).
HasCoequalizers k =>
(x ~> c) -> (x ~> c') -> c ~> c'
forall (c :: FIN (S n)) (x :: FIN (S n)) (c' :: FIN (S n)).
(x ~> c) -> (x ~> c') -> c ~> c'
factorCoequalizer FZ ~> b
LTE FZ b
q FZ ~> b
LTE FZ b
h)
  factorCoequalizer (SLT LTE a b
q) (SLT LTE a b
h) = LTE b b -> LTE (FS b) (FS b)
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS 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 :: FIN (S n)) (x :: FIN (S n)) (c' :: FIN (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 (rather than via 'Proarrow.Limit.Pullback.thinPullback',
-- which would need @HasProducts (FIN n)@ -- unavailable for an abstract @n@, since 'HasBinaryProducts'
-- and 'HasTerminalObject' are only resolvable for a syntactically concrete @n@).
instance HasPullbacks (FIN n) where
  pullback :: forall (o :: FIN n) (a :: FIN n) (b :: FIN n) r.
(a ~> o)
-> (b ~> o)
-> (forall (p :: FIN n). (p ~> a) -> (p ~> b) -> r)
-> r
pullback (ZLT LTE FZ b
_) (ZLT LTE FZ b
_) forall (p :: FIN n). (p ~> a) -> (p ~> b) -> r
k = (FZ ~> a) -> (FZ ~> b) -> r
forall (p :: FIN n). (p ~> a) -> (p ~> b) -> r
k FZ ~> a
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ FZ ~> b
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
  pullback (ZLT LTE FZ b
_) (SLT @b' LTE a b
g) forall (p :: FIN n). (p ~> a) -> (p ~> b) -> r
k = (FZ ~> a) -> (FZ ~> b) -> r
forall (p :: FIN n). (p ~> a) -> (p ~> b) -> r
k FZ ~> a
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ (LTE FZ a -> LTE FZ (FS a)
forall {n :: NAT} (b :: FIN (S n)). LTE FZ b -> LTE FZ (FS b)
ZLT (forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @_ @b' ((Ob a, Ob b) => LTE FZ a) -> LTE a b -> LTE FZ 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 :: FIN (S n)) (b :: FIN (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 FZ b
_) forall (p :: FIN n). (p ~> a) -> (p ~> b) -> r
k = (FZ ~> a) -> (FZ ~> b) -> r
forall (p :: FIN n). (p ~> a) -> (p ~> b) -> r
k (LTE FZ a -> LTE FZ (FS a)
forall {n :: NAT} (b :: FIN (S n)). LTE FZ b -> LTE FZ (FS b)
ZLT (forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @_ @a' ((Ob a, Ob b) => LTE FZ a) -> LTE a b -> LTE FZ 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 :: FIN (S n)) (b :: FIN (S n)) r.
((Ob a, Ob b) => r) -> LTE a b -> r
\\ LTE a b
f)) FZ ~> b
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
  pullback (SLT LTE a b
f) (SLT LTE a b
g) forall (p :: FIN n). (p ~> a) -> (p ~> b) -> r
k = (a ~> b)
-> (a ~> b)
-> (forall (p :: FIN (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 :: FIN (S n)) (a :: FIN (S n)) (b :: FIN (S n)) r.
(a ~> o)
-> (b ~> o)
-> (forall (p :: FIN (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 -> (FS p ~> a) -> (FS p ~> b) -> r
forall (p :: FIN n). (p ~> a) -> (p ~> b) -> r
k (LTE p a -> LTE (FS p) (FS a)
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS b)
SLT p ~> a
LTE p a
p1) (LTE p a -> LTE (FS p) (FS a)
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS b)
SLT p ~> a
LTE p a
p2)
  pullback a ~> o
LTE a o
ZEQ b ~> o
LTE b FZ
ZEQ forall (p :: FIN n). (p ~> a) -> (p ~> b) -> r
k = (FZ ~> a) -> (FZ ~> b) -> r
forall (p :: FIN n). (p ~> a) -> (p ~> b) -> r
k FZ ~> a
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ FZ ~> b
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
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 :: FIN n) (b :: FIN n) (p :: FIN n) (q :: FIN 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 :: FIN n) (x :: FIN n) (e' :: FIN 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 (FIN n) where
  pushout :: forall (o :: FIN n) (a :: FIN n) (b :: FIN n) r.
(o ~> a)
-> (o ~> b)
-> (forall (p :: FIN n). (a ~> p) -> (b ~> p) -> r)
-> r
pushout o ~> a
LTE o a
ZEQ o ~> b
g forall (p :: FIN n). (a ~> p) -> (b ~> p) -> r
k = (a ~> b) -> (b ~> b) -> r
forall (p :: FIN n). (a ~> p) -> (b ~> p) -> r
k o ~> b
a ~> b
g (LTE b b
(Ob FZ, Ob b) => LTE b b
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: FIN n). Ob a => LTE a a
id ((Ob FZ, Ob b) => LTE b b) -> LTE FZ 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 :: FIN (S n)) (b :: FIN n) r.
((Ob a, Ob b) => r) -> LTE a b -> r
\\ o ~> b
LTE FZ b
g)
  pushout o ~> a
f o ~> b
LTE o b
ZEQ forall (p :: FIN n). (a ~> p) -> (b ~> p) -> r
k = (a ~> a) -> (b ~> a) -> r
forall (p :: FIN n). (a ~> p) -> (b ~> p) -> r
k (LTE a a
(Ob FZ, Ob a) => LTE a a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: FIN n). Ob a => LTE a a
id ((Ob FZ, Ob a) => LTE a a) -> LTE FZ 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 :: FIN (S n)) (b :: FIN n) r.
((Ob a, Ob b) => r) -> LTE a b -> r
\\ o ~> a
LTE FZ a
f) o ~> a
b ~> a
f
  pushout (ZLT LTE FZ b
f) (ZLT LTE FZ b
g) forall (p :: FIN n). (a ~> p) -> (b ~> p) -> r
k = (FZ ~> b)
-> (FZ ~> b)
-> (forall (p :: FIN (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 :: FIN (S n)) (a :: FIN (S n)) (b :: FIN (S n)) r.
(o ~> a)
-> (o ~> b)
-> (forall (p :: FIN (S n)). (a ~> p) -> (b ~> p) -> r)
-> r
pushout FZ ~> b
LTE FZ b
f FZ ~> b
LTE FZ b
g \b ~> p
q1 b ~> p
q2 -> (a ~> FS p) -> (b ~> FS p) -> r
forall (p :: FIN n). (a ~> p) -> (b ~> p) -> r
k (LTE b p -> LTE (FS b) (FS p)
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS b)
SLT b ~> p
LTE b p
q1) (LTE b p -> LTE (FS b) (FS p)
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS b)
SLT b ~> p
LTE b p
q2)
  pushout (SLT LTE a b
f) (SLT LTE a b
g) forall (p :: FIN n). (a ~> p) -> (b ~> p) -> r
k = (a ~> b)
-> (a ~> b)
-> (forall (p :: FIN (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 :: FIN (S n)) (a :: FIN (S n)) (b :: FIN (S n)) r.
(o ~> a)
-> (o ~> b)
-> (forall (p :: FIN (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 ~> FS p) -> (b ~> FS p) -> r
forall (p :: FIN n). (a ~> p) -> (b ~> p) -> r
k (LTE b p -> LTE (FS b) (FS p)
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS b)
SLT b ~> p
LTE b p
q1) (LTE b p -> LTE (FS b) (FS p)
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS b)
SLT b ~> p
LTE b p
q2)

  factorPushout :: forall (a :: FIN n) (b :: FIN n) (p :: FIN n) (q :: FIN 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 :: FIN n) (x :: FIN n) (c' :: FIN n).
(x ~> c) -> (x ~> c') -> c ~> c'
factorCoequalizer a ~> p
p1 a ~> q
k1

instance HasEpiMonoFactorization (FIN n) where
  factorize :: forall (a :: FIN n) (b :: FIN n).
(a ~> b) -> (:.:) (Hom (FIN n)) (Hom (FIN n)) a b
factorize = (a ~> b) -> (:.:) (Hom (FIN n)) (Hom (FIN n)) a b
forall k (a :: k) (b :: k).
(HasPushouts k, HasEqualizers k) =>
(a ~> b) -> (:.:) (Hom k) (Hom k) a b
defaultFactorize