{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Topos where

import Proarrow.Category.Monoidal.Closed (CCC)
import Proarrow.Colimit.BinaryCoproduct (HasBinaryCoproducts (..), HasCoproducts)
import Proarrow.Colimit.Coequalizer (HasCoequalizers (..))
import Proarrow.Colimit.Initial (HasInitialObject (..))
import Proarrow.Colimit.Pushout (HasPushouts (..), cokernelPair)
import Proarrow.Core (CategoryOf (..), Hom, Promonad (..), obj)
import Proarrow.Limit.BinaryProduct (HasBinaryProducts (..), HasProducts)
import Proarrow.Limit.Equalizer (HasEqualizers (..))
import Proarrow.Limit.Pullback (HasPullbacks (..))
import Proarrow.Limit.Terminal (HasTerminalObject (..))
import Proarrow.Object (pattern Objs)
import Proarrow.Profunctor.Instance.Composition ((:.:))

class (HasProducts k, Ob (Omega :: k)) => HasSubobjectClassifier k where
  type Omega :: k
  true :: TerminalObject ~> (Omega :: k)
  default true :: (HasProducts k, HasPushouts k) => TerminalObject ~> (Omega :: k)
  true = (TerminalObject ~> TerminalObject) -> TerminalObject ~> Omega
forall {k} (a :: k) (b :: k).
(HasSubobjectClassifier k, HasPushouts k) =>
(a ~> b) -> b ~> Omega
classifyImage (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @TerminalObject)

  -- | Classify the graph (@id *** f :: a ~> a && b@) of a morphism @f@.
  -- This is a minimal primitive that works for any morphism.
  classifyGraph :: a ~> b -> a && b ~> (Omega :: k)

isEq :: forall {k} (a :: k). (HasSubobjectClassifier k, Ob a) => a && a ~> Omega
isEq :: forall {k} (a :: k).
(HasSubobjectClassifier k, Ob a) =>
(a && a) ~> Omega
isEq = (a ~> a) -> (a && a) ~> Omega
forall (a :: k) (b :: k). (a ~> b) -> (a && b) ~> Omega
forall k (a :: k) (b :: k).
HasSubobjectClassifier k =>
(a ~> b) -> (a && b) ~> Omega
classifyGraph (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a)

-- | @classify f@ classifies the image of @f@. If @f@ is mono, then this returns its characteristic map.
classifyImage :: forall {k} (a :: k) b. (HasSubobjectClassifier k, HasPushouts k) => a ~> b -> b ~> Omega
classifyImage :: forall {k} (a :: k) (b :: k).
(HasSubobjectClassifier k, HasPushouts k) =>
(a ~> b) -> b ~> Omega
classifyImage a ~> b
f = (a ~> b)
-> (forall (p :: k). (b ~> p) -> (b ~> p) -> b ~> Omega)
-> b ~> Omega
forall k (a :: k) (b :: k) r.
HasPushouts k =>
(a ~> b) -> (forall (p :: k). (b ~> p) -> (b ~> p) -> r) -> r
cokernelPair a ~> b
f \ @im g1 :: b ~> p
g1@b ~> p
Objs b ~> p
g2 -> forall (a :: k).
(HasSubobjectClassifier k, Ob a) =>
(a && a) ~> Omega
forall {k} (a :: k).
(HasSubobjectClassifier k, Ob a) =>
(a && a) ~> Omega
isEq @im ((p && p) ~> Omega) -> (b ~> (p && p)) -> b ~> Omega
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (b ~> p
g1 (b ~> p) -> (b ~> p) -> b ~> (p && p)
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& b ~> p
g2)

classifyKernelPair :: forall {k} (a :: k) b. (HasSubobjectClassifier k) => a ~> b -> (a && a) ~> Omega
classifyKernelPair :: forall {k} (a :: k) (b :: k).
HasSubobjectClassifier k =>
(a ~> b) -> (a && a) ~> Omega
classifyKernelPair f :: a ~> b
f@a ~> b
Objs = forall (a :: k).
(HasSubobjectClassifier k, Ob a) =>
(a && a) ~> Omega
forall {k} (a :: k).
(HasSubobjectClassifier k, Ob a) =>
(a && a) ~> Omega
isEq @b ((b && b) ~> Omega) -> ((a && a) ~> (b && b)) -> (a && a) ~> Omega
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a ~> b
f (a ~> b) -> (a ~> b) -> (a && a) ~> (b && b)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
*** a ~> b
f)

class (CategoryOf k) => HasEpiMonoFactorization k where
  factorize :: (a ~> b) -> (Hom k :.: Hom k) a b

defaultFactorize :: (HasPushouts k, HasEqualizers k) => (a ~> b) -> (Hom k :.: Hom k) a b
defaultFactorize :: forall k (a :: k) (b :: k).
(HasPushouts k, HasEqualizers k) =>
(a ~> b) -> (:.:) (Hom k) (Hom k) a b
defaultFactorize a ~> b
f = (a ~> b)
-> (a ~> b)
-> (forall (p :: k). (b ~> p) -> (b ~> p) -> (:.:) (~>) (~>) a b)
-> (:.:) (~>) (~>) a b
forall (o :: k) (a :: k) (b :: k) r.
(o ~> a)
-> (o ~> b) -> (forall (p :: k). (a ~> 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
pushout a ~> b
f a ~> b
f \b ~> p
q1 b ~> p
q2 -> (b ~> p) -> (b ~> p) -> (a ~> b) -> (:.:) (~>) (~>) a b
forall (a :: k) (b :: k) (c :: k).
(a ~> b) -> (a ~> b) -> (c ~> a) -> (:.:) (~>) (~>) c a
forall k (a :: k) (b :: k) (c :: k).
HasEqualizers k =>
(a ~> b) -> (a ~> b) -> (c ~> a) -> (:.:) (Hom k) (Hom k) c a
factorEqualizer b ~> p
q1 b ~> p
q2 a ~> b
f

defaultFactorizeDual :: (HasPullbacks k, HasCoequalizers k) => a ~> b -> (Hom k :.: Hom k) a b
defaultFactorizeDual :: forall k (a :: k) (b :: k).
(HasPullbacks k, HasCoequalizers k) =>
(a ~> b) -> (:.:) (Hom k) (Hom k) a b
defaultFactorizeDual a ~> b
f = (a ~> b)
-> (a ~> b)
-> (forall (p :: k). (p ~> a) -> (p ~> a) -> (:.:) (~>) (~>) a b)
-> (:.:) (~>) (~>) a b
forall (o :: k) (a :: k) (b :: k) r.
(a ~> o)
-> (b ~> o) -> (forall (p :: k). (p ~> a) -> (p ~> b) -> 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
pullback a ~> b
f a ~> b
f \p ~> a
p1 p ~> a
p2 -> (p ~> a) -> (p ~> a) -> (a ~> b) -> (:.:) (~>) (~>) a b
forall (a :: k) (b :: k) (c :: k).
(a ~> b) -> (a ~> b) -> (b ~> c) -> (:.:) (~>) (~>) b c
forall k (a :: k) (b :: k) (c :: k).
HasCoequalizers k =>
(a ~> b) -> (a ~> b) -> (b ~> c) -> (:.:) (Hom k) (Hom k) b c
factorCoequalizer p ~> a
p1 p ~> a
p2 a ~> b
f

type HasFiniteLimits k = (HasProducts k, HasPullbacks k, HasEqualizers k)
type HasFiniteColimits k = (HasCoproducts k, HasPushouts k, HasCoequalizers k)

class
  (HasFiniteLimits k, HasFiniteColimits k, CCC k, HasSubobjectClassifier k, HasEpiMonoFactorization k) =>
  ElementaryTopos k

false :: (ElementaryTopos k) => TerminalObject ~> (Omega :: k)
false :: forall k. ElementaryTopos k => TerminalObject ~> Omega
false = (InitialObject ~> TerminalObject) -> TerminalObject ~> Omega
forall {k} (a :: k) (b :: k).
(HasSubobjectClassifier k, HasPushouts k) =>
(a ~> b) -> b ~> Omega
classifyImage InitialObject ~> TerminalObject
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate

and :: forall k. (ElementaryTopos k) => (Omega :: k) && Omega ~> Omega
and :: forall k. ElementaryTopos k => (Omega && Omega) ~> Omega
and = (TerminalObject ~> (Omega && Omega)) -> (Omega && Omega) ~> Omega
forall {k} (a :: k) (b :: k).
(HasSubobjectClassifier k, HasPushouts k) =>
(a ~> b) -> b ~> Omega
classifyImage (TerminalObject ~> Omega
forall k. HasSubobjectClassifier k => TerminalObject ~> Omega
true (TerminalObject ~> Omega)
-> (TerminalObject ~> Omega) -> TerminalObject ~> (Omega && Omega)
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& TerminalObject ~> Omega
forall k. HasSubobjectClassifier k => TerminalObject ~> Omega
true)

or :: forall k. (ElementaryTopos k) => (Omega :: k) && Omega ~> Omega
or :: forall k. ElementaryTopos k => (Omega && Omega) ~> Omega
or = ((Omega || Omega) ~> (Omega && Omega)) -> (Omega && Omega) ~> Omega
forall {k} (a :: k) (b :: k).
(HasSubobjectClassifier k, HasPushouts k) =>
(a ~> b) -> b ~> Omega
classifyImage (Omega ~> Omega
constTrue (Omega ~> Omega) -> (Omega ~> Omega) -> Omega ~> (Omega && Omega)
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Omega ~> Omega
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (Omega ~> (Omega && Omega))
-> (Omega ~> (Omega && Omega))
-> (Omega || Omega) ~> (Omega && Omega)
forall (x :: k) (a :: k) (y :: k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| Omega ~> Omega
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (Omega ~> Omega) -> (Omega ~> Omega) -> Omega ~> (Omega && Omega)
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Omega ~> Omega
constTrue)
  where
    constTrue :: Omega ~> Omega
constTrue = TerminalObject ~> Omega
forall k. HasSubobjectClassifier k => TerminalObject ~> Omega
true (TerminalObject ~> Omega)
-> (Omega ~> TerminalObject) -> Omega ~> Omega
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate @k @Omega

implies :: forall k. (ElementaryTopos k) => (Omega :: k) && Omega ~> Omega
implies :: forall k. ElementaryTopos k => (Omega && Omega) ~> Omega
implies = ((Omega && Omega) ~> Omega)
-> ((Omega && Omega) ~> Omega)
-> (forall (e :: k).
    (e ~> (Omega && Omega)) -> (Omega && Omega) ~> Omega)
-> (Omega && Omega) ~> Omega
forall (a :: k) (b :: k) r.
(a ~> b) -> (a ~> b) -> (forall (e :: k). (e ~> a) -> r) -> r
forall k (a :: k) (b :: k) r.
HasEqualizers k =>
(a ~> b) -> (a ~> b) -> (forall (e :: k). (e ~> a) -> r) -> r
equalize (Omega && Omega) ~> Omega
forall k. ElementaryTopos k => (Omega && Omega) ~> Omega
and (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @k @Omega @Omega) (e ~> (Omega && Omega)) -> (Omega && Omega) ~> Omega
forall (e :: k).
(e ~> (Omega && Omega)) -> (Omega && Omega) ~> Omega
forall {k} (a :: k) (b :: k).
(HasSubobjectClassifier k, HasPushouts k) =>
(a ~> b) -> b ~> Omega
classifyImage