Proarrow

https://sjoerdvisscher.github.io/proarrow/
Admin
Proarrow is a Haskell library providing kind-indexed category theory machinery and a core vocabulary...
Tokens:2,003,711
Snippets:7,616
Trust Score:9.7
Update:1 month ago
Show doc for...
Tokens:
Raw
### EqP Fin usage examples

Source: https://sjoerdvisscher.github.io/proarrow/Proarrow-Category-Instance-Simplex.html

Examples demonstrating the behavior of eqp on Fin values.

```haskell
>>> **eqp FZ FZ
**True
```

```haskell
>>> **eqp FZ (FS FZ)
**False
```

```haskell
>>> **let xs = universe @N.Nat4; ys = universe @N.Nat6 in traverse_ print [ [ eqp x y | y <- ys ] | x <- xs ]
**[True,False,False,False,False,False]
[False,True,False,False,False,False]
[False,False,True,False,False,False]
[False,False,False,True,False,False]
```

--------------------------------

### Pushout example for FinSet

Source: https://sjoerdvisscher.github.io/proarrow/src/Proarrow.Category.Instance.FinSet.html

Shows how to compute a pushout in FinSet using the pushout function. The example defines two morphisms l and r and prints the resulting pushout morphisms.

```haskell
-- | >>> import Data.Fin
-- >>> import Data.Type.Nat
-- >>> let l :: FinSet (FS Nat4) (FS Nat3) = FinSet $ fin0 ::: fin0 ::: fin1 ::: fin2 ::: VNil
-- >>> let r :: FinSet (FS Nat4) (FS Nat5) = FinSet $ fin0 ::: fin2 ::: fin4 ::: fin4 ::: VNil
-- >>> (pushout l r \(FinSet l') (FinSet r') -> P.show (l', r')) :: P.String
-- "(1 ::: 3 ::: 3 ::: VNil,1 ::: 0 ::: 1 ::: 2 ::: 3 ::: VNil)"
```

--------------------------------

### Doctest examples for FinHask operations

Source: https://sjoerdvisscher.github.io/proarrow/src/Proarrow.Category.Instance.FinHask.html

Doctest examples demonstrating pushout, pullback, epi/mono checks, factorization, image classification, and logical operations on FinHask morphisms. These examples show expected outputs for the given functions.

```haskell
-- | >>> import Proarrow.Colimit.Pushout (isEpi)
-- >>> let f :: FinHask (FH (Fin 3)) (FH (Fin 3)) = fromList [(0,2), (1,0), (2,1)]
-- >>> (pushout f f \(FinHask g1) (FinHask g2) -> P.show (g1, g2)) :: P.String
-- "(fromList [(0,0),(1,1),(2,2)],fromList [(0,0),(1,1),(2,2)])"
-- >>> isEpi (f :: FinHask (FH (Fin 3)) (FH (Fin 3)))
-- True
-- >>> import Proarrow.Limit.Pullback (isMono)
-- >>> (pullback f f \(FinHask l) (FinHask r) -> P.show (l, r)) :: P.String
-- "(fromList [(0,0),(1,1),(2,2)],fromList [(0,0),(1,1),(2,2)])"
-- >>> isMono f
-- True
-- >>> import Proarrow.Category.Topos (classifyImage, classifyKernelPair, and, or, implies, false)
-- >>> (case factorize f of p :.: q -> P.show (p, q) \\ p \\ q) :: P.String
-- "(fromList [(0,0),(1,1),(2,2)],fromList [(0,2),(1,0),(2,1)])"
-- >>> (classifyImage f, classifyKernelPair f)
-- (fromList [(0,True),(1,True),(2,True)],fromList [((0,0),True),((0,1),False),((0,2),False),((1,0),False),((1,1),True),((1,2),False),((2,0),False),((2,1),False),((2,2),True)])
-- >>> [and, or, implies] :: [FinHask (FH (Bool, Bool)) (FH Bool)]
-- [fromList [((False,False),False),((False,True),False),((True,False),False),((True,True),True)],fromList [((False,False),False),((False,True),True),((True,False),True),((True,True),True)],fromList [((False,False),True),((False,True),True),((True,False),False),((True,True),True)]]
-- >>> false :: FinHask (FH ()) (FH Bool)
-- fromList [((),False)]
```

--------------------------------

### Pullback Example

Source: https://sjoerdvisscher.github.io/proarrow/src/Proarrow.Category.Instance.Mat.html

Demonstrates the usage of pullback with Mat instances.

```haskell
>>> let f = Mat @(S Z) @(S Z) ((2 ::: VNil) ::: VNil) :: Mat (M (S Z)) (M (S Z) :: MatK P.Double)
>>> let g = Mat @(S Z) @(S Z) ((3 ::: VNil) ::: VNil) :: Mat (M (S Z)) (M (S Z) :: MatK P.Double)
>>> (pullback f g \p q -> case (p, q) of (Mat pv, Mat qv) -> P.show (pv, qv)) :: P.String
"((1.5 ::: VNil) ::: VNil,(1.0 ::: VNil) ::: VNil)"
```

--------------------------------

### OrdP Fin usage example

Source: https://sjoerdvisscher.github.io/proarrow/Proarrow-Category-Instance-Simplex.html

Example demonstrating the behavior of comparep on Fin values.

```haskell
>>> **let xs = universe @N.Nat4; ys = universe @N.Nat6 in traverse_ print [ [ comparep x y | y <- ys ] | x <- xs ]
**[EQ,LT,LT,LT,LT,LT]
[GT,EQ,LT,LT,LT,LT]
[GT,GT,EQ,LT,LT,LT]
[GT,GT,GT,EQ,LT,LT]
```

--------------------------------

### Equalize example in FinHask

Source: https://sjoerdvisscher.github.io/proarrow/Proarrow-Category-Instance-FinHask.html

Example showing how to compute an equalizer in the FinHask category. It defines two morphisms f and g, then uses equalize to compute the inclusion incl and a factor p, displaying the result as a string.

```haskell
>>> let f :: FinHask (FH (Fin 4)) (FH (Fin 3)) = fromList [(0,0), (1,1), (2,1), (3,0)]
>>> let g :: FinHask (FH (Fin 4)) (FH (Fin 3)) = fromList [(0,2), (1,0), (2,1), (3,0)]
>>> let h :: FinHask (FH (Fin 3)) (FH (Fin 4)) = fromList [(0,3), (1,2), (2,3)]
>>> (equalize f g \incl -> let p = factorEqualizer incl h in P.show (incl, p, incl . p)) :: P.String
"(fromList [(0,2),(1,3)],fromList [(0,1),(1,0),(2,1)],fromList [(0,3),(1,2),(2,3)])"
```

--------------------------------

### Equalize matrices example

Source: https://sjoerdvisscher.github.io/proarrow/Proarrow-Category-Instance-Mat.html

Demonstrates the use of equalize and factorEqualizer to find the kernel of the difference between two linear maps.

```haskell
>>> **import Data.Vec.Lazy (Vec(..))
**>>> **let f = Mat @(S (S Z)) @(S Z) ((1 ::: 2 ::: VNil) ::: VNil) :: Mat (M (S (S Z))) (M (S Z) :: MatK P.Double)
**>>> **let g = Mat @(S (S Z)) @(S Z) ((3 ::: 0 ::: VNil) ::: VNil) :: Mat (M (S (S Z))) (M (S Z) :: MatK P.Double)
**>>> **let h = Mat @(S Z) @(S (S Z)) ((1 ::: VNil) ::: (1 ::: VNil) ::: VNil) :: Mat (M (S Z)) (M (S (S Z)) :: MatK P.Double)
**>>> **(equalize f g \incl@(Mat inclv) -> case factorEqualizer incl h of p@(Mat pv) -> P.show (inclv, pv, unMat (incl . p))) :: P.String
**"((1.0 ::: VNil) ::: (1.0 ::: VNil) ::: VNil,(1.0 ::: VNil) ::: VNil,(1.0 ::: VNil) ::: (1.0 ::: VNil) ::: VNil)"
```

--------------------------------

### MatK Equalizer Example

Source: https://sjoerdvisscher.github.io/proarrow/Proarrow-Limit-Equalizer.html

Demonstrates the equalizer of two linear maps in MatK, which corresponds to the kernel of their difference.

```haskell
>>> import Data.Vec.Lazy (Vec(..))
>>> let f = Mat @(S (S Z)) @(S Z) ((1 ::: 2 ::: VNil) ::: VNil) :: Mat (M (S (S Z))) (M (S Z) :: MatK P.Double)
>>> let g = Mat @(S (S Z)) @(S Z) ((3 ::: 0 ::: VNil) ::: VNil) :: Mat (M (S (S Z))) (M (S Z) :: MatK P.Double)
>>> let h = Mat @(S Z) @(S (S Z)) ((1 ::: VNil) ::: (1 ::: VNil) ::: VNil) :: Mat (M (S Z)) (M (S (S Z)) :: MatK P.Double)
>>> (equalize f g \incl@(Mat inclv) -> case factorEqualizer incl h of p@(Mat pv) -> P.show (inclv, pv, unMat (incl . p))) :: P.String
"((1.0 ::: VNil) ::: (1.0 ::: VNil) ::: VNil,(1.0 ::: VNil) ::: VNil,(1.0 ::: VNil) ::: (1.0 ::: VNil) ::: VNil)"
```

--------------------------------

### Setup test environment for closed categories

Source: https://sjoerdvisscher.github.io/proarrow/src/Proarrow.Testing.Laws.html

Helper function that adapts the generic propClosed test to use the TestOb constraints from the testing framework. It provides the necessary witnesses for the monoidal and exponential structures.

```haskell
propClosed_
  :: forall k
   . (Testable k, Exponential.Closed k, TestObIsOb k)
  => TestTree
propClosed_ :: forall k. (Testable k, Closed k, TestObIsOb k) => TestTree
propClosed_ =
  forall k.
(Testable k, Closed k, TestOb Unit) =>
(forall (a :: k) (b :: k) r.
 (TestOb a, TestOb b) =>
 (TestOb (a ** b) => r) -> r)
-> (forall (a :: k) (b :: k) r.
    (TestOb a, TestOb b) =>
    (TestOb (a ~~> b) => r) -> r)
-> TestTree
propClosed @k
    (\ @a @b TestOb (a ** b) => r
r -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
M.withOb2 @k @a @b r
Ob (a ** b) => r
TestOb (a ** b) => r
r)
    (\ @a @b TestOb (a ~~> b) => r
r -> forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
Exponential.withObExp @k @a @b r
Ob (a ~~> b) => r
TestOb (a ~~> b) => r
r)
```

--------------------------------

### Swap a product in FBC - Proarrow docs (swapProduct)

Source: https://sjoerdvisscher.github.io/proarrow/Proarrow-Tools-CCC.html

Example of using `swapProduct` to swap a product's elements. It imports `Bool (..)` and uses `swapProduct` on a tuple `(True, False)` to get `(False, True)` with the FBC product operator `&&`.

```haskell
>>> import Prelude (Bool (..))
>>> swapProduct @Bool @Bool (True, False)
(False,True)

```

--------------------------------

### Promonad instance for product promonad

Source: https://sjoerdvisscher.github.io/proarrow/src/Proarrow.Category.Instance.Product.html

Defines the product promonad instance, providing identity and composition for pairs of promonads.

```haskell
-- | The product promonad of promonads `p` and `q`.
instance (Promonad p, Promonad q) => Promonad (p :**: q) where
  id :: forall (a :: (j1, j2)). Ob a => (:**:) p q a a
id = p (Fst @ a) (Fst @ a)
forall (a :: j1). Ob a => p a a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id p (Fst @ a) (Fst @ a)
-> q (Snd @ a) (Snd @ a)
-> (:**:) p q '(Fst @ a, Snd @ a) '(Fst @ a, Snd @ a)
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)
:**: q (Snd @ a) (Snd @ a)
forall (a :: j2). Ob a => q a a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  (p a1 b1
f1 :**: q a2 b2
f2) . :: forall (b :: (j1, j2)) (c :: (j1, j2)) (a :: (j1, j2)).
(:**:) p q b c -> (:**:) p q a b -> (:**:) p q a c
. (p a1 b1
g1 :**: q a2 b2
g2) = (p a1 b1
f1 p a1 b1 -> p a1 a1 -> p a1 b1
forall (b :: j1) (c :: j1) (a :: j1). p b c -> p a b -> p a c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p a1 a1
p a1 b1
g1) p a1 b1 -> q a2 b2 -> (:**:) p q '(a1, a2) '(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)
:**: (q a2 b2
f2 q a2 b2 -> q a2 a2 -> q a2 b2
forall (b :: j2) (c :: j2) (a :: j2). q b c -> q a b -> q a c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. q a2 a2
q a2 b2
g2)
```

--------------------------------

### get Operation

Source: https://sjoerdvisscher.github.io/proarrow/src/Proarrow.Promonad.State.html

The get operation for StateT, which retrieves the current state.

```haskell
get :: forall {k} p s. (Promonad p, Monoidal k, Comonoid (s :: k)) => StateT s p Unit s
get :: forall {k :: Kind} (p :: k +-> k) (s :: k).
(Promonad p, Monoidal k, Comonoid s) =>
StateT s p Unit s
get = (:.:) (Reader ('OP s) :.: p) (Writer s) Unit s -> StateT s p Unit s
forall {i :: Kind} (s :: i) (p :: i +-> i) (a :: i) (b :: i).
(:.:) (Reader ('OP s) :.: p) (Writer s) a b -> StateT s p a b
StateT (((s ** Unit) ~> s) -> Reader ('OP s) Unit s
forall {k :: Kind} (a :: k) (b :: k) (r1 :: k).
Ob a =>
((r1 ** a) ~> b) -> Reader ('OP r1) a b
Reader (forall (k :: Kind) (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor @k @s) Reader ('OP s) Unit s -> p s s -> (:.:) (Reader ('OP s)) p Unit s
forall {j :: Kind} {k :: Kind} {i :: Kind} (b :: j) (a :: k)
       (c :: i) (p :: j +-> k) (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: p s s
forall (a :: k). Ob a => p a a
forall {k :: Kind} (p :: k +-> k) (a :: k).
(Promonad p, Ob a) =>
p a a
id (:.:) (Reader ('OP s)) p Unit s
-> Writer s s s -> (:.:) (Reader ('OP s) :.: p) (Writer s) Unit s
forall {j :: Kind} {k :: Kind} {i :: Kind} (b :: j) (a :: k)
       (c :: i) (p :: j +-> k) (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (s ~> (s ** s)) -> Writer s s s
forall {k :: Kind} (b :: k) (a :: k) (w :: k).
Ob b =>
(a ~> (w ** b)) -> Writer w a b
Writer (forall (c :: k). Comonoid c => c ~> (c ** c)
forall {k :: Kind} (c :: k). Comonoid c => c ~> (c ** c)
comult @s))
```

--------------------------------

### Pullback operation example

Source: https://sjoerdvisscher.github.io/proarrow/src/Proarrow.Category.Internal.html

Example usage of the pullback operation for BOOL and FINSET.

```haskell
-- | >>> import Data.Fin
-- >>> import Data.Type.Nat
-- >>> import Data.Vec.Lazy
-- >>> import Proarrow.Limit.Pullback
-- >>> import Prelude qualified as P
-- >>> (pullback (source @BOOL @FINSET) (target @BOOL @FINSET) \(FinSet l) (FinSet r) -> P.show (l, r)) :: P.String
-- "(0 ::: 1 ::: 2 ::: 2 ::: VNil,0 ::: 0 ::: 1 ::: 2 ::: VNil)"
```

--------------------------------

### Promonad (Star (Rift ('OP j2)))

Source: https://sjoerdvisscher.github.io/proarrow/Proarrow-Profunctor-Instance-Rift.html

Promonad instance for Star (Rift ('OP j2)) with methods id and (.).

```APIDOC
## Instance: Promonad (Star (Rift ('OP j2)))

### Description
Promonad instance for `Star (Rift ('OP j2))`.

### Methods

#### id
```haskell
id :: forall (a :: k -> j1 -> Type). Ob a => Star (Rift ('OP j2) :: (j1 +-> k) -> k -> j1 -> Type) a a
```

#### (.)
```haskell
(.) :: forall (b :: k -> j1 -> Type) (c :: k -> j1 -> Type) (a :: k -> j1 -> Type). Star (Rift ('OP j2) :: (j1 +-> k) -> k -> j1 -> Type) b c -> Star (Rift ('OP j2) :: (j1 +-> k) -> k -> j1 -> Type) a b -> Star (Rift ('OP j2) :: (j1 +-> k) -> k -> j1 -> Type) a c
```
```

--------------------------------

### Promonad Instance for Free

Source: https://sjoerdvisscher.github.io/proarrow/src/Proarrow.Category.Instance.Free.html

Implements the Promonad instance for Free, defining identity and composition rules for various constructors.

```haskell
instance Promonad (Free :: CAT (FREE cs p)) where
  id :: forall (a :: FREE cs p). Ob a => Free a a
id = Free a a
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Free a a
Id
  Free b c
Id . :: forall (b :: FREE cs p) (c :: FREE cs p) (a :: FREE cs p).
Free b c -> Free a b -> Free a c
. Free a b
g = Free a b
Free a c
g
  Free b c
f . Free a b
Id = Free b c
Free a c
f
  Emb p a b
p Free b ('EMB a)
f . Free a b
g = p a b -> Free a ('EMB a) -> Free a ('EMB b)
forall {j :: Kind} (c :: j) (a :: j) (p :: j -> j -> Kind)
       (cs :: [Kind -> Constraint]) (i :: FREE cs p).
(Ob c, Ob a) =>
p c a -> Free i ('EMB c) -> Free i ('EMB a)
Emb p a b
p (Free b ('EMB a)
f Free b ('EMB a) -> Free a b -> Free a ('EMB a)
forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: FREE cs p) (c :: FREE cs p) (a :: FREE cs p).
Free b c -> Free a b -> Free a c
. Free a b
g)
  St Struct c a c
s Free b a
f . Free a b
g = Struct c a c -> Free a a -> Free a c
forall {j :: Kind} {cs :: [Kind -> Constraint]} {p :: CAT j}
       (c :: Kind -> Constraint) (a :: FREE cs p) (b :: FREE cs p)
       (i :: FREE cs p).
(HasStructure cs p c, Ob a, Ob b) =>
Struct c a b -> Free i a -> Free i b
St Struct c a c
s (Free b a
f Free b a -> Free a b -> Free a a
forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: FREE cs p) (c :: FREE cs p) (a :: FREE cs p).
Free b c -> Free a b -> Free a c
. Free a b
g)
```

--------------------------------

### Promonad (Rift ('OP j) p)

Source: https://sjoerdvisscher.github.io/proarrow/Proarrow-Profunctor-Instance-Rift.html

Promonad instance for Rift with methods id and (.).

```APIDOC
## Instance: Promonad (Rift ('OP j) p)

### Description
Promonad instance for `Rift ('OP j) p`.

### Methods

#### id
```haskell
id :: forall (a :: k). Ob a => Rift ('OP j) p a a
```

#### (.)
```haskell
(.) :: forall (b :: k) (c :: k) (a :: k). Rift ('OP j) p b c -> Rift ('OP j) p a b -> Rift ('OP j) p a c
```
```

--------------------------------

### Show (InitialProfunctor a b) instance methods

Source: https://sjoerdvisscher.github.io/proarrow/Proarrow-Profunctor-Instance-Initial.html

Methods for the Show instance of InitialProfunctor a b.

```APIDOC
## Show (InitialProfunctor a b) instance methods

### Description
Methods for the Show instance of InitialProfunctor a b.

### Methods

#### showsPrec
- **Signature**: showsPrec :: Int -> InitialProfunctor a b -> ShowS
- **Description**: Converts an InitialProfunctor value to a show function with precedence.

#### show
- **Signature**: show :: InitialProfunctor a b -> String
- **Description**: Converts an InitialProfunctor value to a string.

#### showList
- **Signature**: showList :: [InitialProfunctor a b] -> ShowS
- **Description**: Converts a list of InitialProfunctor values to a show function.
```

--------------------------------

### Show instance for Struct HasInitialObject

Source: https://sjoerdvisscher.github.io/proarrow/src/Proarrow.Colimit.Initial.html

Provides a Show instance for Struct HasInitialObject, displaying the string "initiate" for the Initial constructor.

```haskell
instance Show (Struct HasInitialObject a b) where
  showsPrec :: Int -> Struct HasInitialObject a b -> ShowS
showsPrec Int
_ Struct HasInitialObject a b
R:StructjcspHasInitialObjectab j cs p a b
Initial = String -> ShowS
P.showString String
"initiate"
```

--------------------------------

### caseEither usage examples

Source: https://sjoerdvisscher.github.io/proarrow/src/Proarrow.Tools.CCC.html

Examples demonstrating the elimination of sum types using caseEither with Bool values.

```haskell
-- >>> import Prelude (Bool (..), Either (..), not)
-- >>> caseEither @Bool @Bool @Bool (Left True, (not, id))
-- False
-- >>> caseEither @Bool @Bool @Bool (Right True, (not, id))
-- True
```

--------------------------------

### Pullback example for FinSet

Source: https://sjoerdvisscher.github.io/proarrow/Proarrow-Limit-Pullback.html

Example for the FinSet instance of HasPullbacks. Imports Data.Fin, Data.Type.Nat, and Data.Vec.Lazy, defines two FinSet arrows f and g, then computes their pullback and shows the resulting vectors.

```haskell
>>> **import Data.Fin
**>>> **import Data.Type.Nat
**>>> **import Data.Vec.Lazy
**>>> **let f :: FinSet (FS Nat6) (FS Nat3) = FinSet $ fin0 ::: fin1 ::: fin0 ::: fin0 ::: fin2 ::: fin1 ::: VNil
**>>> **let g :: FinSet (FS Nat4) (FS Nat3) = FinSet $ fin2 ::: fin0 ::: fin1 ::: fin0 ::: VNil
**>>> **(pullback f g \(FinSet l) (FinSet r) -> P.show (l, r)) :: P.String
**"(0 ::: 0 ::: 1 ::: 2 ::: 2 ::: 3 ::: 3 ::: 4 ::: 5 ::: VNil,1 ::: 3 ::: 2 ::: 1 ::: 3 ::: 1 ::: 3 ::: 0 ::: 2 ::: VNil)"
```

--------------------------------

### TestingEqShow instance for product profunctor (:**:)

Source: https://sjoerdvisscher.github.io/proarrow/src/Proarrow.Testing.html

Defines eqP and showP for the product profunctor (:**:), combining equality and display of the two component profunctors.

```haskell
instance (TestingEqShow (catk a1 b1), TestingEqShow (catj a2 b2)) => TestingEqShow ((catk :**: catj) '(a1, a2) '(b1, b2)) where
  eqP :: (:**:) catk catj '(a1, a2) '(b1, b2)
-> (:**:) catk catj '(a1, a2) '(b1, b2) -> Property Bool
eqP (catk a1 b1
l1 :**: catj a2 b2
l2) (catk a1 b1
r1 :**: catj a2 b2
r2) = (Bool -> Bool -> Bool)
-> Property Bool -> Property Bool -> Property Bool
forall a b c.
(a -> b -> c)
-> Property' [Char] a -> Property' [Char] b -> Property' [Char] c
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bool -> Bool -> Bool
(&&) (catk a1 b1 -> catk a1 b1 -> Property Bool
forall a. TestingEqShow a => a -> a -> Property Bool
eqP catk a1 b1
l1 catk a1 b1
catk a1 b1
r1) (catj a2 b2 -> catj a2 b2 -> Property Bool
forall a. TestingEqShow a => a -> a -> Property Bool
eqP catj a2 b2
l2 catj a2 b2
catj a2 b2
r2)
  showP :: (:**:) catk catj '(a1, a2) '(b1, b2) -> [Char]
showP (catk a1 b1
l1 :**: catj a2 b2
l2) = [Char]
"(" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ catk a1 b1 -> [Char]
forall a. TestingEqShow a => a -> [Char]
showP catk a1 b1
l1 [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
") :**: (" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ catj a2 b2 -> [Char]
forall a. TestingEqShow a => a -> [Char]
showP catj a2 b2
l2 [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
")"
```

--------------------------------

### (^.)

Source: https://sjoerdvisscher.github.io/proarrow/Proarrow-Optics.html

Gets the target of a getter optic.

```APIDOC
## (^.)

### Description
Gets the target of a getter optic.

### Signature
(^.) :: forall (c :: (Type -> Type -> Type) -> Constraint) a b s t. c (ExOptic (GetterFl :: (Type +-> Type) -> (Type +-> Type) -> Constraint) a b) => s -> Optic c s t a b -> a

### Parameters
- **s** (s) - Required - The source structure.
- **optic** (Optic c s t a b) - Required - The getter optic.

### Returns
- **a** - The target value.
```

--------------------------------

### HasInitialObject (FREE cs p)

Source: https://sjoerdvisscher.github.io/proarrow/Proarrow-Category-Instance-Free.html

Provides an initial object for the free category.

```APIDOC
## HasInitialObject (FREE cs p)

### Description
Provides an initial object for the free category.

### Associated Types
- **type InitialObject** = InitF :: FREE cs p

### Methods
- **initiate** :: forall (a :: FREE cs p). Ob a => (InitialObject :: FREE cs p) ~> a

```

--------------------------------

### Pullback example for FinHask (Seven Sketches 3.84)

Source: https://sjoerdvisscher.github.io/proarrow/Proarrow-Limit-Pullback.html

Example 3.84 of Seven Sketches (A: 0=red, 1=blue, 2=black). Defines a Color type and two FinHask arrows f and g, then computes their pullback and shows the resulting pairs.

```haskell
data Color = Red | Blue | Black deriving (P.Eq, P.Ord, P.Show, P.Enum, P.Bounded, Universe, Finite)
```

```haskell
let f :: FinHask (FH (Fin 6)) (FH Color) = fromList [(0,Red), (1,Blue), (2,Red), (3,Red), (4,Black), (5,Blue)]
```

```haskell
let g :: FinHask (FH (Fin 4)) (FH Color) = fromList [(0,Black), (1,Red), (2,Blue), (3,Red)]
```

```haskell
(pullback f g (FinHask l) (FinHask r) -> P.show (P.zip (M.elems l) (M.elems r))) :: P.String
```

```haskell
"[(0,1),(0,3),(1,2),(2,1),(2,3),(3,1),(3,3),(4,0),(5,2)]"
```

--------------------------------

### Promonad (Codiscrete) instance methods

Source: https://sjoerdvisscher.github.io/proarrow/Proarrow-Category-Instance-Discrete.html

Methods for the Promonad instance: id and composition (.).

```APIDOC
## Promonad (Codiscrete) methods

### id
```haskell
id :: forall (a :: CODISCRETE k). Ob a => Codiscrete a a
```

### (.)
```haskell
(.) :: forall (b :: CODISCRETE k) (c :: CODISCRETE k) (a :: CODISCRETE k). Codiscrete b c -> Codiscrete a b -> Codiscrete a c
```
```

--------------------------------

### mkAlgebraicLens

Source: https://sjoerdvisscher.github.io/proarrow/Proarrow-Optic-Action.html

Constructs an AlgebraicLens from get and put functions.

```APIDOC
## mkAlgebraicLens

### Description
Constructs an `AlgebraicLens` from a getter and a putter.

### Signature

```haskell
mkAlgebraicLens :: forall m s t a b. Monad m => (s -> a) -> (m s -> b -> t) -> AlgebraicLens m s t a b
```

### Parameters
- `s -> a` - The getter function.
- `m s -> b -> t` - The putter function.

### Returns
- `AlgebraicLens m s t a b` - The constructed lens.
```

--------------------------------

### HasBinaryProducts (FREE cs p)

Source: https://sjoerdvisscher.github.io/proarrow/Proarrow-Category-Instance-Free.html

Provides binary products for the free category, including projections and pairing.

```APIDOC
## HasBinaryProducts (FREE cs p)

### Description
Provides binary products for the free category, including projections and pairing.

### Methods
- **withObProd** :: forall (a :: FREE cs p) (b :: FREE cs p) r. (Ob a, Ob b) => (Ob (a && b) => r) -> r
- **fst** :: forall (a :: FREE cs p) (b :: FREE cs p). (Ob a, Ob b) => (a && b) ~> a
- **snd** :: forall (a :: FREE cs p) (b :: FREE cs p). (Ob a, Ob b) => (a && b) ~> b
- **(&&&)** :: forall (a :: FREE cs p) (x :: FREE cs p) (y :: FREE cs p). (a ~> x) -> (a ~> y) -> a ~> (x && y)
- **(***)** :: forall (a :: FREE cs p) (b :: FREE cs p) (x :: FREE cs p) (y :: FREE cs p). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)

```

--------------------------------

### Pullback example with BOOL and FINSET

Source: https://sjoerdvisscher.github.io/proarrow/Proarrow-Category-Instance-Bool.html

This example computes a pullback using the source and target morphisms of the BOOL internal category in FINSET, showing the resulting pair of finite sets. It requires importing Data.Fin, Data.Type.Nat, Data.Vec.Lazy, Proarrow.Limit.Pullback, and Prelude qualified as P.

```haskell
>>> **import Data.Fin
>>> **import Data.Type.Nat
>>> **import Data.Vec.Lazy
>>> **import Proarrow.Limit.Pullback
>>> **import Prelude qualified as P
>>> **(pullback (source @BOOL @FINSET) (target @BOOL @FINSET) \(FinSet l) (FinSet r) -> P.show (l, r)) :: P.String
**"(0 ::: 1 ::: 2 ::: 2 ::: VNil,0 ::: 0 ::: 1 ::: 2 ::: VNil)"
```

--------------------------------

### HasInitialObject (PROD k)

Source: https://sjoerdvisscher.github.io/proarrow/Proarrow-Colimit-Initial.html

Instance for the product category, where the initial object is the product of the initial object.

```APIDOC
## HasInitialObject (PROD k)

### Description
Instance of HasInitialObject for the product category, providing the initial object as the product of the initial object.

### Associated Type
- **InitialObject** = 'PR (InitialObject :: k)

### Methods
- **initiate** :: forall (a :: PROD k). Ob a => (InitialObject :: PROD k) ~> a
```

--------------------------------

### (^?)

Source: https://sjoerdvisscher.github.io/proarrow/Proarrow-Optics.html

Gets the target of an affine fold optic, returning Maybe.

```APIDOC
## (^?)

### Description
Gets the target of an affine fold optic, returning Maybe.

### Signature
(^?) :: forall s t a b (c :: (Type -> Type -> Type) -> Constraint). c (ExOptic (AffineFoldFl :: (Type +-> Type) -> (Type +-> Type) -> Constraint) a b) => s -> Optic c s t a b -> Maybe a

### Parameters
- **s** (s) - Required - The source structure.
- **optic** (Optic c s t a b) - Required - The affine fold optic.

### Returns
- **Maybe a** - The target value if present.
```

--------------------------------

### Show (FinRel a b)

Source: https://sjoerdvisscher.github.io/proarrow/Proarrow-Category-Instance-FinRel.html

Show instance for finite relations, providing showsPrec, show, and showList methods.

```APIDOC
## Show (FinRel a b)

### Description
Provides string representation for finite relations.

### Instance
Show (FinRel a b)

### Methods
#### showsPrec
- **Signature**: showsPrec :: Int -> FinRel a b -> ShowS
- **Description**: Precedence-aware show.

#### show
- **Signature**: show :: FinRel a b -> String
- **Description**: Converts a finite relation to a string.

#### showList
- **Signature**: showList :: [FinRel a b] -> ShowS
- **Description**: Shows a list of finite relations.
```

--------------------------------

### Promonad (Star (Prelude m))

Source: https://sjoerdvisscher.github.io/proarrow/Proarrow.html

Promonad instance for Star (Prelude m), providing identity and composition for star promonads.

```APIDOC
## Promonad (Star (Prelude m))

### Description
Promonad instance for Star (Prelude m), providing identity and composition for star promonads.

### Methods
- **id** :: Ob a => Star (Prelude m) a a
- **(.)** :: Star (Prelude m) b c -> Star (Prelude m) a b -> Star (Prelude m) a c

### Defined In
Proarrow.Profunctor.Instance.Star
```

--------------------------------

### Pushout example in FinHask

Source: https://sjoerdvisscher.github.io/proarrow/Proarrow-Category-Instance-FinHask.html

Example from Exercise 6.22 of Seven Sketches showing how to compute a pushout in the FinHask category. It defines two morphisms l and r using fromList and then uses pushout to compute the pushout morphisms l' and r', displaying the result as a string.

```haskell
>>> let l :: FinHask (FH (Fin 4)) (FH (Fin 3)) = fromList [(0,0), (1,0), (2,1), (3,2)]
>>> let r :: FinHask (FH (Fin 4)) (FH (Fin 5)) = fromList [(0,0), (1,2), (2,4), (3,4)]
>>> (pushout l r l' r' -> P.show (l', r')) :: P.String
"(fromList [(0,1),(1,3),(2,3)],fromList [(0,1),(1,0),(2,1),(3,2),(4,3)])"
```

--------------------------------

### v1Optic

Source: https://sjoerdvisscher.github.io/proarrow/src/Proarrow.Optic.MonoidalTraversal.html

An example PTraversal for the V1 type, mapping a to a' in V1 a to V1 a'.

```APIDOC
## v1Optic

### Description
An example PTraversal for the V1 type, mapping a to a' in V1 a to V1 a'.

### Signature
v1Optic :: PTraversal (G.V1 a) (G.V1 a') a a'

### Returns
- **PTraversal (G.V1 a) (G.V1 a') a a'** - The PTraversal for V1.
```

--------------------------------

### Dimap operation usage

Source: https://sjoerdvisscher.github.io/proarrow/src/Proarrow.Category.Monoidal.Strength.html

Example of using dimap with swap operations.

```haskell
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @u @x) (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @y @u) p (x ** u) (y ** u)
p) ((Ob (x ** u), Ob (y ** u)) => p x y)
-> p (x ** u) (y ** u) -> p x y
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p 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
\\ p (x ** u) (y ** u)
p
```

--------------------------------

### Promonad (p :**: q)

Source: https://sjoerdvisscher.github.io/proarrow/Proarrow-Core.html

The product promonad of promonads p and q. Requires Promonad p and Promonad q. Provides identity and composition methods.

```APIDOC
## Promonad (p :**: q)

### Description
The product promonad of promonads p and q. Requires Promonad p and Promonad q. Provides identity and composition methods.

### Methods

#### id
- **Signature**: id :: forall (a :: (j1, j2)). Ob a => (p :**: q) a a
- **Description**: Identity morphism for the promonad.

#### (.)
- **Signature**: (.) :: forall (b :: (j1, j2)) (c :: (j1, j2)) (a :: (j1, j2)). (p :**: q) b c -> (p :**: q) a b -> (p :**: q) a c
- **Description**: Composition of morphisms in the promonad.
```
Tokens:
Raw