{-# OPTIONS_GHC -Wno-orphans #-}

-- | Pushouts: 'HasPushouts' with 'pushout' in continuation-passing style (the apex type depends on the
-- given arrows, so it is hidden behind an existential), and 'factorPushout' for the universal property,
-- defaulting to coproduct-then-coequalizer where those exist.
module Proarrow.Colimit.Pushout where

import Prelude (Bool, const, ($), (==))

import Proarrow.Category.Enriched.Thin (Thin)
import Proarrow.Category.Instance.Bool (BOOL (..))
import Proarrow.Category.Instance.Opposite (OPPOSITE, Op (..))
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Unit (Unit (..))
import Proarrow.Colimit.BinaryCoproduct (HasBinaryCoproducts (..), HasCoproducts)
import Proarrow.Colimit.Coequalizer (HasCoequalizers, factorPushoutDefault, pushoutDefault)
import Proarrow.Core (CategoryOf (..), Eq2, Hom, obj, (//))
import Proarrow.Limit.BinaryProduct (PROD, Prod (..))
import Proarrow.Limit.Pullback (HasPullbacks (..))
import Proarrow.Object (pattern Objs)

-- | Pushouts are an inherently dependently typed concept:
-- The type of the apex object depends on the values of the given arrows.
-- But at runtime we can still calculate the arrows and the type, which we hide behind an existential.
class (CategoryOf k) => HasPushouts k where
  pushout :: forall (o :: k) a b r. o ~> a -> o ~> b -> (forall p. a ~> p -> b ~> p -> r) -> r
  default pushout
    :: forall (o :: k) a b r
     . (HasCoequalizers k, HasCoproducts k)
    => o ~> a -> o ~> b -> (forall p. a ~> p -> b ~> p -> r) -> r
  pushout = (o ~> a)
-> (o ~> b) -> (forall (p :: k). (a ~> p) -> (b ~> p) -> r) -> r
forall {k} (o :: k) (a :: k) (b :: k) r.
(HasCoequalizers k, HasCoproducts k) =>
(o ~> a)
-> (o ~> b) -> (forall (p :: k). (a ~> p) -> (b ~> p) -> r) -> r
pushoutDefault

  -- | @factorPushout p1 p2 k1 k2@ requires @k1, k2@ to be a compatible cocone for whichever cospan
  -- @p1, p2@ happen to be a pushout of. @p1, p2@ need not literally be @pushout@'s own output.
  factorPushout :: forall (a :: k) b p q. a ~> p -> b ~> p -> a ~> q -> b ~> q -> p ~> q
  default factorPushout
    :: forall (a :: k) b p q. (HasCoequalizers k, HasCoproducts k) => a ~> p -> b ~> p -> a ~> q -> b ~> q -> p ~> q
  factorPushout = (a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q
forall {k} (a :: k) (b :: k) (p :: k) (q :: k).
(HasCoequalizers k, HasCoproducts k) =>
(a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q
factorPushoutDefault

instance HasPushouts () where
  pushout :: forall (o :: ()) (a :: ()) (b :: ()) r.
(o ~> a)
-> (o ~> b) -> (forall (p :: ()). (a ~> p) -> (b ~> p) -> r) -> r
pushout o ~> a
Unit o a
Unit o ~> b
Unit '() b
Unit forall (p :: ()). (a ~> p) -> (b ~> p) -> r
k = (a ~> '()) -> (b ~> '()) -> r
forall (p :: ()). (a ~> p) -> (b ~> p) -> r
k a ~> '()
Unit '() '()
Unit b ~> '()
Unit '() '()
Unit
  factorPushout :: forall (a :: ()) (b :: ()) (p :: ()) (q :: ()).
(a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q
factorPushout a ~> p
Unit a p
Unit b ~> p
Unit b '()
Unit a ~> q
Unit '() q
Unit b ~> q
Unit '() '()
Unit = p ~> q
Unit '() '()
Unit

instance HasPushouts BOOL where
  pushout :: forall (o :: BOOL) (a :: BOOL) (b :: BOOL) r.
(o ~> a)
-> (o ~> b) -> (forall (p :: BOOL). (a ~> p) -> (b ~> p) -> r) -> r
pushout = (o ~> a)
-> (o ~> b) -> (forall (p :: BOOL). (a ~> p) -> (b ~> p) -> r) -> r
forall {k} (o :: k) (a :: k) (b :: k) r.
(Thin k, HasCoproducts k) =>
(o ~> a)
-> (o ~> b) -> (forall (p :: k). (a ~> p) -> (b ~> p) -> r) -> r
thinPushout

instance (HasPushouts k1, HasPushouts k2) => HasPushouts (k1, k2) where
  pushout :: forall (o :: (k1, k2)) (a :: (k1, k2)) (b :: (k1, k2)) r.
(o ~> a)
-> (o ~> b)
-> (forall (p :: (k1, k2)). (a ~> p) -> (b ~> p) -> r)
-> r
pushout (a1 ~> b1
l1 :**: a2 ~> b2
l2) (a1 ~> b1
r1 :**: a2 ~> b2
r2) forall (p :: (k1, k2)). (a ~> p) -> (b ~> p) -> r
k = (a1 ~> b1)
-> (a1 ~> b1)
-> (forall (p :: k1). (b1 ~> p) -> (b1 ~> p) -> r)
-> r
forall (o :: k1) (a :: k1) (b :: k1) r.
(o ~> a)
-> (o ~> b) -> (forall (p :: k1). (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 a1 ~> b1
l1 a1 ~> b1
a1 ~> b1
r1 \b1 ~> p
f1 b1 ~> p
g1 -> (a2 ~> b2)
-> (a2 ~> b2)
-> (forall (p :: k2). (b2 ~> p) -> (b2 ~> p) -> r)
-> r
forall (o :: k2) (a :: k2) (b :: k2) r.
(o ~> a)
-> (o ~> b) -> (forall (p :: k2). (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 a2 ~> b2
l2 a2 ~> b2
a2 ~> b2
r2 \b2 ~> p
f2 b2 ~> p
g2 -> (a ~> '(p, p)) -> (b ~> '(p, p)) -> r
forall (p :: (k1, k2)). (a ~> p) -> (b ~> p) -> r
k (b1 ~> p
f1 (b1 ~> p) -> (b2 ~> p) -> (:**:) (~>) (~>) '(b1, b2) '(p, p)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: b2 ~> p
f2) (b1 ~> p
g1 (b1 ~> p) -> (b2 ~> p) -> (:**:) (~>) (~>) '(b1, b2) '(p, p)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: b2 ~> p
g2)
  factorPushout :: forall (a :: (k1, k2)) (b :: (k1, k2)) (p :: (k1, k2))
       (q :: (k1, k2)).
(a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q
factorPushout (a1 ~> b1
p1a :**: a2 ~> b2
p1b) (a1 ~> b1
p2a :**: a2 ~> b2
p2b) (a1 ~> b1
k1a :**: a2 ~> b2
k1b) (a1 ~> b1
k2a :**: a2 ~> b2
k2b) =
    (a1 ~> b1) -> (a1 ~> b1) -> (a1 ~> b1) -> (a1 ~> b1) -> b1 ~> b1
forall (a :: k1) (b :: k1) (p :: k1) (q :: k1).
(a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q
forall k (a :: k) (b :: k) (p :: k) (q :: k).
HasPushouts k =>
(a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q
factorPushout a1 ~> b1
p1a a1 ~> b1
a1 ~> b1
p2a a1 ~> b1
a1 ~> b1
k1a a1 ~> b1
a1 ~> b1
k2a (b1 ~> b1) -> (b2 ~> b2) -> (:**:) (~>) (~>) '(b1, b2) '(b1, b2)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: (a2 ~> b2) -> (a2 ~> b2) -> (a2 ~> b2) -> (a2 ~> b2) -> b2 ~> b2
forall (a :: k2) (b :: k2) (p :: k2) (q :: k2).
(a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q
forall k (a :: k) (b :: k) (p :: k) (q :: k).
HasPushouts k =>
(a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q
factorPushout a2 ~> b2
p1b a2 ~> b2
a2 ~> b2
p2b a2 ~> b2
a2 ~> b2
k1b a2 ~> b2
a2 ~> b2
k2b

-- | Pushouts are unchanged by making the tensor the product.
instance (HasPushouts k) => HasPushouts (PROD k) where
  pushout :: forall (o :: PROD k) (a :: PROD k) (b :: PROD k) r.
(o ~> a)
-> (o ~> b)
-> (forall (p :: PROD k). (a ~> p) -> (b ~> p) -> r)
-> r
pushout (Prod a1 ~> b1
f) (Prod a1 ~> b1
g) forall (p :: PROD k). (a ~> p) -> (b ~> p) -> r
k = (a1 ~> b1)
-> (a1 ~> b1)
-> (forall (p :: k). (b1 ~> p) -> (b1 ~> p) -> r)
-> r
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 a1 ~> b1
f a1 ~> b1
a1 ~> b1
g \b1 ~> p
p1 b1 ~> p
p2 -> (a ~> PR p) -> (b ~> PR p) -> r
forall (p :: PROD k). (a ~> p) -> (b ~> p) -> r
k ((b1 ~> p) -> Prod (~>) (PR b1) (PR p)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p (PR a1) (PR b1)
Prod b1 ~> p
p1) ((b1 ~> p) -> Prod (~>) (PR b1) (PR p)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p (PR a1) (PR b1)
Prod b1 ~> p
p2)
  factorPushout :: forall (a :: PROD k) (b :: PROD k) (p :: PROD k) (q :: PROD k).
(a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q
factorPushout (Prod a1 ~> b1
p1) (Prod a1 ~> b1
p2) (Prod a1 ~> b1
k1) (Prod a1 ~> b1
k2) = (b1 ~> b1) -> Prod (~>) (PR b1) (PR b1)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p (PR a1) (PR b1)
Prod ((a1 ~> b1) -> (a1 ~> b1) -> (a1 ~> b1) -> (a1 ~> b1) -> b1 ~> b1
forall (a :: k) (b :: k) (p :: k) (q :: k).
(a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q
forall k (a :: k) (b :: k) (p :: k) (q :: k).
HasPushouts k =>
(a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q
factorPushout a1 ~> b1
p1 a1 ~> b1
a1 ~> b1
p2 a1 ~> b1
a1 ~> b1
k1 a1 ~> b1
a1 ~> b1
k2)

-- | In a thin category, arrows don't carry information, so pushouts are just coproducts.
thinPushout
  :: forall {k} (o :: k) a b r. (Thin k, HasCoproducts k) => o ~> a -> o ~> b -> (forall p. a ~> p -> b ~> p -> r) -> r
thinPushout :: forall {k} (o :: k) (a :: k) (b :: k) r.
(Thin k, HasCoproducts k) =>
(o ~> a)
-> (o ~> b) -> (forall (p :: k). (a ~> p) -> (b ~> p) -> r) -> r
thinPushout o ~> a
l o ~> b
r forall (p :: k). (a ~> p) -> (b ~> p) -> r
k = o ~> a
l (o ~> a) -> ((Ob o, Ob a) => r) -> r
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// o ~> b
r (o ~> b) -> ((Ob o, Ob b) => r) -> r
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @a @b ((Ob (a || b) => r) -> r) -> (Ob (a || b) => r) -> r
forall a b. (a -> b) -> a -> b
$ (a ~> (a || b)) -> (b ~> (a || b)) -> r
forall (p :: k). (a ~> p) -> (b ~> p) -> r
k (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @a @b) (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @a @b)

coequalizerDefault
  :: forall {k} (a :: k) b r. (HasPushouts k, HasCoproducts k) => a ~> b -> a ~> b -> (forall c. b ~> c -> r) -> r
coequalizerDefault :: forall {k} (a :: k) (b :: k) r.
(HasPushouts k, HasCoproducts k) =>
(a ~> b) -> (a ~> b) -> (forall (c :: k). (b ~> c) -> r) -> r
coequalizerDefault f :: a ~> b
f@a ~> b
Objs a ~> b
g forall (c :: k). (b ~> c) -> r
k = ((b || a) ~> b)
-> ((b || a) ~> b)
-> (forall (p :: k). (b ~> p) -> (b ~> p) -> r)
-> r
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 (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b Obj b -> (a ~> b) -> (b || a) ~> b
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
||| a ~> b
f) (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b Obj b -> (a ~> b) -> (b || a) ~> b
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
||| a ~> b
g) (((b ~> p) -> r) -> (b ~> p) -> (b ~> p) -> r
forall a b. a -> b -> a
const (b ~> p) -> r
forall (c :: k). (b ~> c) -> r
k)

cokernelPair :: (HasPushouts k) => (a :: k) ~> b -> (forall p. b ~> p -> b ~> p -> r) -> r
cokernelPair :: forall k (a :: k) (b :: k) r.
HasPushouts k =>
(a ~> b) -> (forall (p :: k). (b ~> p) -> (b ~> p) -> r) -> r
cokernelPair a ~> b
f = (a ~> b)
-> (a ~> b) -> (forall (p :: k). (b ~> p) -> (b ~> p) -> r) -> r
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

isEpi :: (HasPushouts k, Eq2 (Hom k)) => (a :: k) ~> b -> Bool
isEpi :: forall k (a :: k) (b :: k).
(HasPushouts k, Eq2 (Hom k)) =>
(a ~> b) -> Bool
isEpi f :: a ~> b
f@a ~> b
Objs = (a ~> b) -> (forall (p :: k). (b ~> p) -> (b ~> p) -> Bool) -> Bool
forall k (a :: k) (b :: k) r.
HasPushouts k =>
(a ~> b) -> (forall (p :: k). (b ~> p) -> (b ~> p) -> r) -> r
cokernelPair a ~> b
f \l :: b ~> p
l@b ~> p
Objs b ~> p
r -> b ~> p
l (b ~> p) -> (b ~> p) -> Bool
forall a. Eq a => a -> a -> Bool
== b ~> p
r

instance (HasPullbacks k) => HasPushouts (OPPOSITE k) where
  pushout :: forall (o :: OPPOSITE k) (a :: OPPOSITE k) (b :: OPPOSITE k) r.
(o ~> a)
-> (o ~> b)
-> (forall (p :: OPPOSITE k). (a ~> p) -> (b ~> p) -> r)
-> r
pushout (Op b1 ~> a1
l) (Op b1 ~> a1
r) forall (p :: OPPOSITE k). (a ~> p) -> (b ~> p) -> r
k = (b1 ~> a1)
-> (b1 ~> a1)
-> (forall (p :: k). (p ~> b1) -> (p ~> b1) -> r)
-> r
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 b1 ~> a1
l b1 ~> a1
b1 ~> a1
r \p ~> b1
f p ~> b1
g -> (a ~> OP p) -> (b ~> OP p) -> r
forall (p :: OPPOSITE k). (a ~> p) -> (b ~> p) -> r
k ((p ~> b1) -> Op (~>) (OP b1) (OP p)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p (OP a1) (OP b1)
Op p ~> b1
f) ((p ~> b1) -> Op (~>) (OP b1) (OP p)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p (OP a1) (OP b1)
Op p ~> b1
g)
  factorPushout :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) (p :: OPPOSITE k)
       (q :: OPPOSITE k).
(a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q
factorPushout (Op b1 ~> a1
p1) (Op b1 ~> a1
p2) (Op b1 ~> a1
k1) (Op b1 ~> a1
k2) = (b1 ~> b1) -> Op (~>) (OP b1) (OP b1)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p (OP a1) (OP b1)
Op ((b1 ~> a1) -> (b1 ~> a1) -> (b1 ~> a1) -> (b1 ~> a1) -> b1 ~> b1
forall (a :: k) (b :: k) (p :: k) (q :: k).
(p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p
forall k (a :: k) (b :: k) (p :: k) (q :: k).
HasPullbacks k =>
(p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p
factorPullback b1 ~> a1
p1 b1 ~> a1
b1 ~> a1
p2 b1 ~> a1
b1 ~> a1
k1 b1 ~> a1
b1 ~> a1
k2)

instance (HasPushouts k) => HasPullbacks (OPPOSITE k) where
  pullback :: forall (o :: OPPOSITE k) (a :: OPPOSITE k) (b :: OPPOSITE k) r.
(a ~> o)
-> (b ~> o)
-> (forall (p :: OPPOSITE k). (p ~> a) -> (p ~> b) -> r)
-> r
pullback (Op b1 ~> a1
l) (Op b1 ~> a1
r) forall (p :: OPPOSITE k). (p ~> a) -> (p ~> b) -> r
k = (b1 ~> a1)
-> (b1 ~> a1)
-> (forall (p :: k). (a1 ~> p) -> (a1 ~> p) -> r)
-> r
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 b1 ~> a1
l b1 ~> a1
b1 ~> a1
r \a1 ~> p
f a1 ~> p
g -> (OP p ~> a) -> (OP p ~> b) -> r
forall (p :: OPPOSITE k). (p ~> a) -> (p ~> b) -> r
k ((a1 ~> p) -> Op (~>) (OP p) (OP a1)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p (OP a1) (OP b1)
Op a1 ~> p
f) ((a1 ~> p) -> Op (~>) (OP p) (OP a1)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p (OP a1) (OP b1)
Op a1 ~> p
g)
  factorPullback :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) (p :: OPPOSITE k)
       (q :: OPPOSITE k).
(p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p
factorPullback (Op b1 ~> a1
p1) (Op b1 ~> a1
p2) (Op b1 ~> a1
k1) (Op b1 ~> a1
k2) = (a1 ~> a1) -> Op (~>) (OP a1) (OP a1)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p (OP a1) (OP b1)
Op ((b1 ~> a1) -> (b1 ~> a1) -> (b1 ~> a1) -> (b1 ~> a1) -> a1 ~> a1
forall (a :: k) (b :: k) (p :: k) (q :: k).
(a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q
forall k (a :: k) (b :: k) (p :: k) (q :: k).
HasPushouts k =>
(a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q
factorPushout b1 ~> a1
p1 b1 ~> a1
b1 ~> a1
p2 b1 ~> a1
b1 ~> a1
k1 b1 ~> a1
b1 ~> a1
k2)