{-# LANGUAGE AllowAmbiguousTypes #-}

-- | Elementary toposes: 'HasSubobjectClassifier' provides the object 'Omega' of truth values
-- classifying monomorphisms, 'HasEpiMonoFactorization' the image factorization, and
-- 'ElementaryTopos' combines these with finite (co)limits and exponentials, yielding the internal
-- logic ('false', 'and', 'or', 'implies').
module Proarrow.Category.Topos where

import Proarrow.Category.Monoidal.Cartesian (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, PROD, Prod (..))
import Proarrow.Limit.Equalizer (HasEqualizers (..))
import Proarrow.Limit.Pullback (HasPullbacks (..))
import Proarrow.Limit.Terminal (HasTerminalObject (..), const)
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 :: CAT 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 :: CAT 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
  -- | Factor an arrow as an epi followed by a mono. Defaults to 'defaultFactorize', the image
  -- factorization via the cokernel pair, which applies whenever @k@ has pushouts and equalizers.
  factorize :: (a ~> b) -> (Hom k :.: Hom k) a b
  default factorize :: (HasPushouts k, HasEqualizers k) => (a ~> b) -> (Hom k :.: Hom k) a b
  factorize = (a ~> b) -> (:.:) (Hom k) (Hom k) a b
forall k (a :: k) (b :: k).
(HasPushouts k, HasEqualizers k) =>
(a ~> b) -> (:.:) (Hom k) (Hom k) a b
defaultFactorize

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)
-> (forall (e :: k). (e ~> b) -> (:.:) (~>) (~>) a b)
-> (:.:) (~>) (~>) a b
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 b ~> p
q1 b ~> p
q2 \e ~> b
incl -> (e ~> b) -> (a ~> b) -> a ~> e
forall (e :: k) (x :: k) (e' :: k).
(e ~> x) -> (e' ~> x) -> e' ~> e
forall k (e :: k) (x :: k) (e' :: k).
HasEqualizers k =>
(e ~> x) -> (e' ~> x) -> e' ~> e
factorEqualizer e ~> b
incl a ~> b
f (a ~> e) -> (e ~> b) -> (:.:) (~>) (~>) a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: e ~> b
incl

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)
-> (forall (c :: k). (a ~> c) -> (:.:) (~>) (~>) a b)
-> (:.:) (~>) (~>) a b
forall (a :: k) (b :: k) r.
(a ~> b) -> (a ~> b) -> (forall (c :: k). (b ~> c) -> r) -> r
forall k (a :: k) (b :: k) r.
HasCoequalizers k =>
(a ~> b) -> (a ~> b) -> (forall (c :: k). (b ~> c) -> r) -> r
coequalize p ~> a
p1 p ~> a
p2 \a ~> c
incl -> a ~> c
incl (a ~> c) -> (c ~> b) -> (:.:) (~>) (~>) a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (a ~> c) -> (a ~> b) -> c ~> b
forall (c :: k) (x :: k) (c' :: k).
(x ~> c) -> (x ~> c') -> c ~> c'
forall k (c :: k) (x :: k) (c' :: k).
HasCoequalizers k =>
(x ~> c) -> (x ~> c') -> c ~> c'
factorCoequalizer a ~> c
incl a ~> b
f

-- | Image factorization is unchanged by making the tensor the product.
instance (HasEpiMonoFactorization k) => HasEpiMonoFactorization (PROD k) where
  factorize :: forall (a :: PROD k) (b :: PROD k).
(a ~> b) -> (:.:) (Hom (PROD k)) (Hom (PROD k)) a b
factorize (Prod a1 ~> b1
f) = case (a1 ~> b1) -> (:.:) (~>) (~>) a1 b1
forall (a :: k) (b :: k). (a ~> b) -> (:.:) (~>) (~>) a b
forall k (a :: k) (b :: k).
HasEpiMonoFactorization k =>
(a ~> b) -> (:.:) (Hom k) (Hom k) a b
factorize a1 ~> b1
f of Hom k a1 b
e :.: Hom k b b1
m -> Hom k a1 b -> Prod (~>) (PR a1) (PR b)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p (PR a1) (PR b1)
Prod Hom k a1 b
e Prod (~>) a (PR b)
-> Prod (~>) (PR b) b -> (:.:) (Prod (~>)) (Prod (~>)) a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: Hom k b b1 -> Prod (~>) (PR b) (PR b1)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p (PR a1) (PR b1)
Prod Hom k b b1
m

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 (forall (a :: k) (b :: k).
(HasTerminalObject k, Ob a) =>
El b -> a ~> b
forall {k} (a :: k) (b :: k).
(HasTerminalObject k, Ob a) =>
El b -> a ~> b
const @Omega El Omega
forall k. HasSubobjectClassifier k => TerminalObject ~> Omega
true (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 :: CAT 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 :: CAT 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)
&&& forall (a :: k) (b :: k).
(HasTerminalObject k, Ob a) =>
El b -> a ~> b
forall {k} (a :: k) (b :: k).
(HasTerminalObject k, Ob a) =>
El b -> a ~> b
const @Omega El Omega
forall k. HasSubobjectClassifier k => TerminalObject ~> Omega
true)

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

-- | Negation: the classifying map of 'false', which is a mono as every arrow out of the terminal
-- object is. The same arrow as @u ⇒ false@.
not :: forall k. (ElementaryTopos k) => (Omega :: k) ~> Omega
-- Not through 'implies', which classifies a subobject of @Omega && Omega@ where this classifies
-- one of 'Omega', and 'classifyImage' squares the cokernel pair of whatever it is given.
not :: forall k. ElementaryTopos k => Omega ~> Omega
not = (TerminalObject ~> Omega) -> Omega ~> Omega
forall {k} (a :: k) (b :: k).
(HasSubobjectClassifier k, HasPushouts k) =>
(a ~> b) -> b ~> Omega
classifyImage (forall k. ElementaryTopos k => TerminalObject ~> Omega
false @k)

-- * Lawvere–Tierney topologies

-- $topologies
-- A Lawvere–Tierney topology is an arrow @j :: 'Omega' '~>' 'Omega'@ that fixes 'true', is
-- idempotent and preserves 'and'. Its sheaves form a subtopos. Every topos has the two extremes,
-- 'id' (every object a sheaf) and @'const' 'true'@ (only the terminal one), and the internal
-- logic gives the ones below. A coverage gives another, by closing sieves:
-- 'Proarrow.Category.Enriched.Finitary.Sheaf.lawvereTierney'.
-- @Proarrow.Testing.Laws.testLawvereTierney@ checks the three laws.

-- | The double-negation topology @¬¬@, whose sheaves form the smallest dense subtopos, and a
-- Boolean one. On a presheaf topos it is the dense topology: a sieve on @a@ covers when every arrow
-- into @a@ can be extended to one in the sieve. When every cospan can be completed to a commuting
-- square (the Ore condition, which pullbacks provide), that is the atomic topology, so there
-- 'Proarrow.Category.Sheaf.Atomic' computes this by closing sieves. In a Boolean topos it is 'id'.
doubleNegation :: forall k. (ElementaryTopos k) => (Omega :: k) ~> Omega
doubleNegation :: forall k. ElementaryTopos k => Omega ~> Omega
doubleNegation = forall k. ElementaryTopos k => Omega ~> Omega
not @k (Omega ~> Omega) -> (Omega ~> Omega) -> Omega ~> Omega
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k. ElementaryTopos k => Omega ~> Omega
not @k

-- | The open topology of a truth value @u@: @u ⇒ -@. Its sheaves are the open subtopos of the
-- subterminal object @u@ classifies, the part of the topos lying over @u@. @'openTopology' 'true'@
-- is 'id' and @'openTopology' 'false'@ is @'const' 'true'@.
openTopology :: forall k. (ElementaryTopos k) => TerminalObject ~> (Omega :: k) -> (Omega :: k) ~> Omega
-- A lambda under the binding, so that 'implies' is built once and shared by every @u@. It is an
-- image to classify, and a family of topologies is typically used at many truth values.
openTopology :: forall k.
ElementaryTopos k =>
(TerminalObject ~> Omega) -> Omega ~> Omega
openTopology = \TerminalObject ~> Omega
u -> (Omega && Omega) ~> Omega
i ((Omega && Omega) ~> Omega)
-> (Omega ~> (Omega && Omega)) -> Omega ~> Omega
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. ((TerminalObject ~> Omega) -> Omega ~> Omega
forall {k} (a :: k) (b :: k).
(HasTerminalObject k, Ob a) =>
El b -> a ~> b
const TerminalObject ~> Omega
u (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 :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id)
  where
    i :: (Omega && Omega) ~> Omega
i = forall k. ElementaryTopos k => (Omega && Omega) ~> Omega
implies @k

-- | The closed topology of a truth value @u@: @u ∨ -@, complementary to 'openTopology'. Its
-- sheaves are the part of the topos lying away from @u@. @'closedTopology' 'true'@ is
-- @'const' 'true'@ and @'closedTopology' 'false'@ is 'id'.
closedTopology :: forall k. (ElementaryTopos k) => TerminalObject ~> (Omega :: k) -> (Omega :: k) ~> Omega
-- A lambda under the binding, so that 'or' is built once and shared, as in 'openTopology'.
closedTopology :: forall k.
ElementaryTopos k =>
(TerminalObject ~> Omega) -> Omega ~> Omega
closedTopology = \TerminalObject ~> Omega
u -> (Omega && Omega) ~> Omega
o ((Omega && Omega) ~> Omega)
-> (Omega ~> (Omega && Omega)) -> Omega ~> Omega
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. ((TerminalObject ~> Omega) -> Omega ~> Omega
forall {k} (a :: k) (b :: k).
(HasTerminalObject k, Ob a) =>
El b -> a ~> b
const TerminalObject ~> Omega
u (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 :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id)
  where
    o :: (Omega && Omega) ~> Omega
o = forall k. ElementaryTopos k => (Omega && Omega) ~> Omega
or @k