proarrow
Safe HaskellNone
LanguageGHC2024

Proarrow.Category.Instance.Bool

Description

The thin category of booleans: objects FLS and TRU with one non-identity arrow FLS ~> TRU, the poset False <= True, a.k.a. the walking arrow. It is a core type. Thin categories are enriched in it (Proarrow.Category.Enriched.Thin), so this module depends on nothing but Proarrow.Core. The further structure of BOOL (conjunction as product and tensor, disjunction as coproduct, closed, star-autonomous, (co)equalizers, pullbacks/pushouts, a parameterized NNO) is instantiated in the modules that define those classes.

Synopsis

Documentation

data BOOL Source Github #

Constructors

FLS 
TRU 

Instances

Instances details
Quantale BOOL Source Github #

The walking arrow: the tensor is conjunction, the join disjunction.

Instance details

Defined in Proarrow.Category.Enriched.Quantale

Methods

minIs :: forall (x :: BOOL) (y :: BOOL). (Ob x, Ob y) => MinIs x y Source Github #

unitIsNotBottom :: ((Unit :: BOOL) ~> (InitialObject :: BOOL)) -> r Source Github #

unitIsTop :: forall (w :: BOOL) r. Ob w => ((Unit :: BOOL) ~> w) -> (w ~ (Unit :: BOOL) => r) -> r Source Github #

Enumerable BOOL Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Methods

withIndex :: forall (a :: BOOL) r. Ob a => (KnownIndex a => r) -> r Source Github #

withOb :: forall (a :: BOOL) r. KnownIndex a => (Ob a => r) -> r Source Github #

atOb :: forall (i :: Nat). SNat i -> AtOb BOOL (At BOOL i) Source Github #

Finite BOOL Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Associated Types

type Objects BOOL 
Instance details

Defined in Proarrow.Category.Enriched.Thin

type Objects BOOL = '['FLS, 'TRU]

Methods

finite :: IndexedList (Objects BOOL) Source Github #

withAtLookup :: forall (i :: Nat) r. SNat i -> (Lookup (Objects BOOL) i ~ At BOOL i => r) -> r Source Github #

Indexed BOOL Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Associated Types

type Index (a :: BOOL) 
Instance details

Defined in Proarrow.Category.Enriched.Thin

type Index (a :: BOOL) = IndexOf a (Objects BOOL)
type At BOOL i 
Instance details

Defined in Proarrow.Category.Enriched.Thin

type At BOOL i = Lookup (Objects BOOL) i
Monoidal BOOL Source Github #

Products as monoidal structure.

Instance details

Defined in Proarrow.Limit.BinaryProduct

Associated Types

type Unit 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type Unit = TerminalObject :: BOOL
type (a :: BOOL) ** (b :: BOOL) 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type (a :: BOOL) ** (b :: BOOL) = a && b

Methods

withOb2 :: forall (a :: BOOL) (b :: BOOL) r. (Ob a, Ob b) => (Ob (a ** b) => r) -> r Source Github #

leftUnitor :: forall (a :: BOOL). Ob a => ((Unit :: BOOL) ** a) ~> a Source Github #

leftUnitorInv :: forall (a :: BOOL). Ob a => a ~> ((Unit :: BOOL) ** a) Source Github #

rightUnitor :: forall (a :: BOOL). Ob a => (a ** (Unit :: BOOL)) ~> a Source Github #

rightUnitorInv :: forall (a :: BOOL). Ob a => a ~> (a ** (Unit :: BOOL)) Source Github #

associator :: forall (a :: BOOL) (b :: BOOL) (c :: BOOL). (Ob a, Ob b, Ob c) => ((a ** b) ** c) ~> (a ** (b ** c)) Source Github #

associatorInv :: forall (a :: BOOL) (b :: BOOL) (c :: BOOL). (Ob a, Ob b, Ob c) => (a ** (b ** c)) ~> ((a ** b) ** c) Source Github #

SymMonoidal BOOL Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Methods

swap :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b) => (a ** b) ~> (b ** a) Source Github #

Closed BOOL Source Github #

Implication is the internal hom of the walking arrow: a ~~> b is BoolLeq a b.

Instance details

Defined in Proarrow.Category.Monoidal.Closed

Associated Types

type (a :: BOOL) ~~> (b :: BOOL) 
Instance details

Defined in Proarrow.Category.Monoidal.Closed

type (a :: BOOL) ~~> (b :: BOOL) = BoolLeq a b

Methods

withObExp :: forall (a :: BOOL) (b :: BOOL) r. (Ob a, Ob b) => (Ob (a ~~> b) => r) -> r Source Github #

curry :: forall (a :: BOOL) (b :: BOOL) (c :: BOOL). (Ob a, Ob b) => ((a ** b) ~> c) -> a ~> (b ~~> c) Source Github #

apply :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b) => ((a ~~> b) ** a) ~> b Source Github #

(^^^) :: forall (a :: BOOL) (b :: BOOL) (x :: BOOL) (y :: BOOL). (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y) Source Github #

CopyDiscard BOOL Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.CopyDiscard

Methods

copy :: forall (a :: BOOL). Ob a => a ~> (a ** a) Source Github #

discard :: forall (a :: BOOL). Ob a => a ~> (Unit :: BOOL) Source Github #

Distributive BOOL Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.Distributive

Methods

distL :: forall (a :: BOOL) (b :: BOOL) (c :: BOOL). (Ob a, Ob b, Ob c) => (a ** (b || c)) ~> ((a ** b) || (a ** c)) Source Github #

distR :: forall (a :: BOOL) (b :: BOOL) (c :: BOOL). (Ob a, Ob b, Ob c) => ((a || b) ** c) ~> ((a ** c) || (b ** c)) Source Github #

absorbL :: forall (a :: BOOL). Ob a => (a ** (InitialObject :: BOOL)) ~> (InitialObject :: BOOL) Source Github #

absorbR :: forall (a :: BOOL). Ob a => ((InitialObject :: BOOL) ** a) ~> (InitialObject :: BOOL) Source Github #

StarAutonomous BOOL Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.StarAutonomous

Associated Types

type Dual (a :: BOOL) 
Instance details

Defined in Proarrow.Category.Monoidal.StarAutonomous

type Dual (a :: BOOL) = Not a

Methods

withObDual :: forall (a :: BOOL) r. Ob a => (Ob (Dual a) => r) -> r Source Github #

dual :: forall (a :: BOOL) (b :: BOOL). (a ~> b) -> Dual b ~> Dual a Source Github #

dualInv :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b) => (Dual a ~> Dual b) -> b ~> a Source Github #

linDist :: forall (a :: BOOL) (b :: BOOL) (c :: BOOL). (Ob a, Ob b, Ob c) => ((a ** b) ~> Dual c) -> a ~> Dual (b ** c) Source Github #

linDistInv :: forall (a :: BOOL) (b :: BOOL) (c :: BOOL). (Ob a, Ob b, Ob c) => (a ~> Dual (b ** c)) -> (a ** b) ~> Dual c Source Github #

doubleNeg :: forall (a :: BOOL). Ob a => Dual (Dual a) ~> a Source Github #

doubleNegInv :: forall (a :: BOOL). Ob a => a ~> Dual (Dual a) Source Github #

HasBinaryCoproducts BOOL Source Github # 
Instance details

Defined in Proarrow.Colimit.BinaryCoproduct

Associated Types

type 'TRU || (b :: BOOL) 
Instance details

Defined in Proarrow.Colimit.BinaryCoproduct

type 'TRU || (b :: BOOL) = 'TRU
type 'FLS || (b :: BOOL) 
Instance details

Defined in Proarrow.Colimit.BinaryCoproduct

type 'FLS || (b :: BOOL) = b
type (a :: BOOL) || 'TRU 
Instance details

Defined in Proarrow.Colimit.BinaryCoproduct

type (a :: BOOL) || 'TRU = 'TRU
type (a :: BOOL) || 'FLS 
Instance details

Defined in Proarrow.Colimit.BinaryCoproduct

type (a :: BOOL) || 'FLS = a

Methods

withObCoprod :: forall (a :: BOOL) (b :: BOOL) r. (Ob a, Ob b) => (Ob (a || b) => r) -> r Source Github #

lft :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b) => a ~> (a || b) Source Github #

rgt :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b) => b ~> (a || b) Source Github #

(|||) :: forall (x :: BOOL) (a :: BOOL) (y :: BOOL). (x ~> a) -> (y ~> a) -> (x || y) ~> a Source Github #

(+++) :: forall (a :: BOOL) (b :: BOOL) (x :: BOOL) (y :: BOOL). (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) Source Github #

HasCoequalizers BOOL Source Github #

Dual to the HasEqualizers instance for BOOL.

Instance details

Defined in Proarrow.Colimit.Coequalizer

Methods

coequalize :: forall (a :: BOOL) (b :: BOOL) r. (a ~> b) -> (a ~> b) -> (forall (c :: BOOL). (b ~> c) -> r) -> r Source Github #

factorCoequalizer :: forall (c :: BOOL) (x :: BOOL) (c' :: BOOL). (x ~> c) -> (x ~> c') -> c ~> c' Source Github #

HasInitialObject BOOL Source Github # 
Instance details

Defined in Proarrow.Colimit.Initial

Associated Types

type InitialObject 
Instance details

Defined in Proarrow.Colimit.Initial

type InitialObject = 'FLS

Methods

initiate :: forall (a :: BOOL). Ob a => (InitialObject :: BOOL) ~> a Source Github #

HasParamNNO BOOL Source Github # 
Instance details

Defined in Proarrow.Colimit.NaturalNumbers

Associated Types

type NNO 
Instance details

Defined in Proarrow.Colimit.NaturalNumbers

type NNO = 'TRU

Methods

zero :: (Unit :: BOOL) ~> (NNO :: BOOL) Source Github #

succ :: (NNO :: BOOL) ~> (NNO :: BOOL) Source Github #

nnoUniv :: forall (a :: BOOL) (x :: BOOL). (a ~> x) -> (x ~> x) -> (a ** (NNO :: BOOL)) ~> x Source Github #

HasPushouts BOOL Source Github # 
Instance details

Defined in Proarrow.Colimit.Pushout

Methods

pushout :: forall (o :: BOOL) (a :: BOOL) (b :: BOOL) r. (o ~> a) -> (o ~> b) -> (forall (p :: BOOL). (a ~> p) -> (b ~> p) -> r) -> r Source Github #

factorPushout :: forall (a :: BOOL) (b :: BOOL) (p :: BOOL) (q :: BOOL). (a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q Source Github #

CategoryOf BOOL Source Github #

The category of 2 objects and one arrow between them, a.k.a. the walking arrow.

Instance details

Defined in Proarrow.Category.Instance.Bool

Associated Types

type (~>) 
Instance details

Defined in Proarrow.Category.Instance.Bool

type (~>) = Booleans
type Ob (b :: BOOL) 
Instance details

Defined in Proarrow.Category.Instance.Bool

type Ob (b :: BOOL) = IsBool b
HasBinaryProducts BOOL Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Associated Types

type 'FLS && (b :: BOOL) 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type 'FLS && (b :: BOOL) = 'FLS
type 'TRU && (b :: BOOL) 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type 'TRU && (b :: BOOL) = b
type (a :: BOOL) && 'FLS 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type (a :: BOOL) && 'FLS = 'FLS
type (a :: BOOL) && 'TRU 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type (a :: BOOL) && 'TRU = a

Methods

withObProd :: forall (a :: BOOL) (b :: BOOL) r. (Ob a, Ob b) => (Ob (a && b) => r) -> r Source Github #

fst :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b) => (a && b) ~> a Source Github #

snd :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b) => (a && b) ~> b Source Github #

(&&&) :: forall (a :: BOOL) (x :: BOOL) (y :: BOOL). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Github #

(***) :: forall (a :: BOOL) (b :: BOOL) (x :: BOOL) (y :: BOOL). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Github #

HasEqualizers BOOL Source Github #

factorEqualizer incl h requires h's image to lie within incl's. Since BOOL is the 2-element total order FLS <= TRU, that means h's domain is <= incl's domain. That's always true when incl came from equalize (which only ever produces the identity), but since BOOL is totally ordered we can case on the shapes directly (at most 5 are reachable, since both share a codomain).

Instance details

Defined in Proarrow.Limit.Equalizer

Methods

equalize :: forall (a :: BOOL) (b :: BOOL) r. (a ~> b) -> (a ~> b) -> (forall (e :: BOOL). (e ~> a) -> r) -> r Source Github #

factorEqualizer :: forall (e :: BOOL) (x :: BOOL) (e' :: BOOL). (e ~> x) -> (e' ~> x) -> e' ~> e Source Github #

HasPullbacks BOOL Source Github # 
Instance details

Defined in Proarrow.Limit.Pullback

Methods

pullback :: forall (o :: BOOL) (a :: BOOL) (b :: BOOL) r. (a ~> o) -> (b ~> o) -> (forall (p :: BOOL). (p ~> a) -> (p ~> b) -> r) -> r Source Github #

factorPullback :: forall (a :: BOOL) (b :: BOOL) (p :: BOOL) (q :: BOOL). (p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p Source Github #

HasTerminalObject BOOL Source Github # 
Instance details

Defined in Proarrow.Limit.Terminal

Associated Types

type TerminalObject 
Instance details

Defined in Proarrow.Limit.Terminal

type TerminalObject = 'TRU

Methods

terminate :: forall (a :: BOOL). Ob a => a ~> (TerminalObject :: BOOL) Source Github #

Promonad Booleans Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Bool

Methods

id :: forall (a :: BOOL). Ob a => Booleans a a Source Github #

(.) :: forall (b :: BOOL) (c :: BOOL) (a :: BOOL). Booleans b c -> Booleans a b -> Booleans a c Source Github #

Ob a => CocommutativeComonoid (a :: BOOL) Source Github # 
Instance details

Defined in Proarrow.Monoid

CommutativeMonoid 'TRU Source Github # 
Instance details

Defined in Proarrow.Monoid

Ob a => Comonoid (a :: BOOL) Source Github # 
Instance details

Defined in Proarrow.Monoid

Methods

counit :: a ~> (Unit :: BOOL) Source Github #

comult :: a ~> (a ** a) Source Github #

Monoid 'TRU Source Github # 
Instance details

Defined in Proarrow.Monoid

Methods

mempty :: (Unit :: BOOL) ~> 'TRU Source Github #

mappend :: ('TRU ** 'TRU) ~> 'TRU Source Github #

Finitary Booleans Source Github #

BOOL is thin, so each hom-set holds at most the one arrow.

Instance details

Defined in Proarrow.Category.Enriched.Finitary

Methods

size :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b) => Natural Source Github #

toIndex :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b) => Booleans a b -> Natural Source Github #

fromIndex :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b) => Natural -> Booleans a b Source Github #

elements :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b) => [Booleans a b] Source Github #

DecidableProfunctor Booleans Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Associated Types

type Holds Booleans (a :: BOOL) (b :: BOOL) 
Instance details

Defined in Proarrow.Category.Enriched.Thin

type Holds Booleans (a :: BOOL) (b :: BOOL) = BoolLeq a b

Methods

decide :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b) => Decision Booleans a b (Holds Booleans a b) Source Github #

toHolds :: forall (a :: BOOL) (b :: BOOL) r. Booleans a b -> ((Holds Booleans a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

ThinProfunctor Booleans Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Associated Types

type HasArrow Booleans (a :: BOOL) (b :: BOOL) 
Instance details

Defined in Proarrow.Category.Enriched.Thin

type HasArrow Booleans (a :: BOOL) (b :: BOOL) = Holds Booleans a b ~ 'TRU

Methods

arr :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b, HasArrow Booleans a b) => Booleans a b Source Github #

withArr :: forall (a :: BOOL) (b :: BOOL) r. Booleans a b -> ((HasArrow Booleans a b, Ob a, Ob b) => r) -> r Source Github #

InternalIn BOOL FINSET Source Github #
>>> 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)"
Instance details

Defined in Proarrow.Category.Internal

Associated Types

type C0 BOOL 
Instance details

Defined in Proarrow.Category.Internal

type C0 BOOL = 'FS Nat2
type C1 BOOL 
Instance details

Defined in Proarrow.Category.Internal

type C1 BOOL = 'FS Nat3

Methods

source :: (C1 BOOL :: FINSET) ~> (C0 BOOL :: FINSET) Source Github #

target :: (C1 BOOL :: FINSET) ~> (C0 BOOL :: FINSET) Source Github #

identity :: (C0 BOOL :: FINSET) ~> (C1 BOOL :: FINSET) Source Github #

compose :: Cosink '[C1 BOOL :: FINSET, C1 BOOL :: FINSET, C1 BOOL :: FINSET] Source Github #

MonoidalProfunctor Booleans Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Methods

one :: Booleans (Unit :: BOOL) (Unit :: BOOL) Source Github #

(**) :: forall (x1 :: BOOL) (x2 :: BOOL) (y1 :: BOOL) (y2 :: BOOL). Booleans x1 x2 -> Booleans y1 y2 -> Booleans (x1 ** y1) (x2 ** y2) Source Github #

Profunctor Booleans Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Bool

Methods

dimap :: forall (c :: BOOL) (a :: BOOL) (b :: BOOL) (d :: BOOL). (c ~> a) -> (b ~> d) -> Booleans a b -> Booleans c d Source Github #

lmap :: forall (c :: BOOL) (a :: BOOL) (b :: BOOL). (c ~> a) -> Booleans a b -> Booleans c b Source Github #

rmap :: forall (b :: BOOL) (d :: BOOL) (a :: BOOL). (b ~> d) -> Booleans a b -> Booleans a d Source Github #

(\\) :: forall (a :: BOOL) (b :: BOOL) r. ((Ob a, Ob b) => r) -> Booleans a b -> r Source Github #

Corepresentable Booleans Source Github # 
Instance details

Defined in Proarrow.Profunctor.Corepresentable

Associated Types

type Booleans %% (x :: BOOL) 
Instance details

Defined in Proarrow.Profunctor.Corepresentable

type Booleans %% (x :: BOOL) = x

Methods

coindex :: forall (a :: BOOL) (b :: BOOL). Booleans a b -> (Booleans %% a) ~> b Source Github #

cotabulate :: forall (a :: BOOL) (b :: BOOL). Ob a => ((Booleans %% a) ~> b) -> Booleans a b Source Github #

corepMap :: forall (a :: BOOL) (b :: BOOL). (a ~> b) -> (Booleans %% a) ~> (Booleans %% b) Source Github #

corepUniv :: forall (a :: BOOL). Ob a => Booleans a (Booleans %% a) Source Github #

Representable Booleans Source Github # 
Instance details

Defined in Proarrow.Profunctor.Representable

Associated Types

type Booleans % (x :: BOOL) 
Instance details

Defined in Proarrow.Profunctor.Representable

type Booleans % (x :: BOOL) = x

Methods

index :: forall (a :: BOOL) (b :: BOOL). Booleans a b -> a ~> (Booleans % b) Source Github #

tabulate :: forall (b :: BOOL) (a :: BOOL). Ob b => (a ~> (Booleans % b)) -> Booleans a b Source Github #

repMap :: forall (a :: BOOL) (b :: BOOL). (a ~> b) -> (Booleans % a) ~> (Booleans % b) Source Github #

repUniv :: forall (a :: BOOL). Ob a => Booleans (Booleans % a) a Source Github #

(DecidableProfunctor p, Decidable j, Decidable k) => EnrichedProfunctor BOOL (p :: j +-> k) Source Github #

A decidable thin profunctor is a profunctor enriched in the walking arrow: its hom-object is the type-level Holds, an element of it is an arrow, and composition is conjunction.

Instance details

Defined in Proarrow.Category.Enriched

Methods

withProObj :: forall (a :: k) (b :: j) r. (Ob a, Ob b) => (Ob (ProObj BOOL p a b) => r) -> r Source Github #

underlying :: forall (a :: k) (b :: j). p a b -> (Unit :: BOOL) ~> ProObj BOOL p a b Source Github #

enriched :: forall (a :: k) (b :: j). (Ob a, Ob b) => ((Unit :: BOOL) ~> ProObj BOOL p a b) -> p a b Source Github #

rmap :: forall (a :: k) (b :: j) (c :: j). (Ob a, Ob b, Ob c) => (HomObj BOOL b c ** ProObj BOOL p a b) ~> ProObj BOOL p a c Source Github #

lmap :: forall (a :: k) (b :: j) (c :: k). (Ob a, Ob b, Ob c) => (HomObj BOOL c a ** ProObj BOOL p a b) ~> ProObj BOOL p c b Source Github #

(Ob ff, Ob tt) => DecidableProfunctor (NonTrivialProfunctor '(ff, tt) :: BOOL -> BOOL -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Methods

decide :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b) => Decision (NonTrivialProfunctor '(ff, tt)) a b (Holds (NonTrivialProfunctor '(ff, tt)) a b) Source Github #

toHolds :: forall (a :: BOOL) (b :: BOOL) r. NonTrivialProfunctor '(ff, tt) a b -> ((Holds (NonTrivialProfunctor '(ff, tt)) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

(Ob ff, Ob tt) => ThinProfunctor (NonTrivialProfunctor '(ff, tt) :: BOOL -> BOOL -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Methods

arr :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b, HasArrow (NonTrivialProfunctor '(ff, tt)) a b) => NonTrivialProfunctor '(ff, tt) a b Source Github #

withArr :: forall (a :: BOOL) (b :: BOOL) r. NonTrivialProfunctor '(ff, tt) a b -> ((HasArrow (NonTrivialProfunctor '(ff, tt)) a b, Ob a, Ob b) => r) -> r Source Github #

Profunctor (NonTrivialProfunctor ft :: BOOL -> BOOL -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Bool

Methods

dimap :: forall (c :: BOOL) (a :: BOOL) (b :: BOOL) (d :: BOOL). (c ~> a) -> (b ~> d) -> NonTrivialProfunctor ft a b -> NonTrivialProfunctor ft c d Source Github #

lmap :: forall (c :: BOOL) (a :: BOOL) (b :: BOOL). (c ~> a) -> NonTrivialProfunctor ft a b -> NonTrivialProfunctor ft c b Source Github #

rmap :: forall (b :: BOOL) (d :: BOOL) (a :: BOOL). (b ~> d) -> NonTrivialProfunctor ft a b -> NonTrivialProfunctor ft a d Source Github #

(\\) :: forall (a :: BOOL) (b :: BOOL) r. ((Ob a, Ob b) => r) -> NonTrivialProfunctor ft a b -> r Source Github #

(Indexed k, KnownEdges es) => DecidableProfunctor (Edges es :: DISCRETE k -> DISCRETE k -> Type) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Instance.Edges

Methods

decide :: forall (a :: DISCRETE k) (b :: DISCRETE k). (Ob a, Ob b) => Decision (Edges es) a b (Holds (Edges es) a b) Source Github #

toHolds :: forall (a :: DISCRETE k) (b :: DISCRETE k) r. Edges es a b -> ((Holds (Edges es) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

(Indexed k, KnownEdges es) => ThinProfunctor (Edges es :: DISCRETE k -> DISCRETE k -> Type) Source Github #

A graph with BOOL weights is a relation on the points: decided by walking the edge list.

Instance details

Defined in Proarrow.Profunctor.Instance.Edges

Methods

arr :: forall (a :: DISCRETE k) (b :: DISCRETE k). (Ob a, Ob b, HasArrow (Edges es) a b) => Edges es a b Source Github #

withArr :: forall (a :: DISCRETE k) (b :: DISCRETE k) r. Edges es a b -> ((HasArrow (Edges es) a b, Ob a, Ob b) => r) -> r Source Github #

Enumerable (BOOL, BOOL) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Product

Methods

withIndex :: forall (a :: (BOOL, BOOL)) r. Ob a => (KnownIndex a => r) -> r Source Github #

withOb :: forall (a :: (BOOL, BOOL)) r. KnownIndex a => (Ob a => r) -> r Source Github #

atOb :: forall (i :: Nat). SNat i -> AtOb (BOOL, BOOL) (At (BOOL, BOOL) i) Source Github #

Finite (BOOL, BOOL) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Product

Associated Types

type Objects (BOOL, BOOL) 
Instance details

Defined in Proarrow.Category.Instance.Product

type Objects (BOOL, BOOL) = '['('FLS, 'FLS), '('FLS, 'TRU), '('TRU, 'FLS), '('TRU, 'TRU)]

Methods

finite :: IndexedList (Objects (BOOL, BOOL)) Source Github #

withAtLookup :: forall (i :: Nat) r. SNat i -> (Lookup (Objects (BOOL, BOOL)) i ~ At (BOOL, BOOL) i => r) -> r Source Github #

Indexed (BOOL, BOOL) Source Github #

The product of two enumerable kinds is enumerable, but numbering one in general needs type-level division to invert the pairing, which fin does not provide, so this instance for (BOOL, BOOL) is numbered by hand. The order matches the value-level pairIndex convention: first component slowest.

(Proarrow.Category.Sheaf uses this kind as the opens of a discrete two-point space: a pair of booleans is a subset of {x, y}.)

Instance details

Defined in Proarrow.Category.Instance.Product

Associated Types

type Index (a :: (BOOL, BOOL)) 
Instance details

Defined in Proarrow.Category.Instance.Product

type Index (a :: (BOOL, BOOL)) = IndexOf a (Objects (BOOL, BOOL))
type At (BOOL, BOOL) i 
Instance details

Defined in Proarrow.Category.Instance.Product

type At (BOOL, BOOL) i = Lookup (Objects (BOOL, BOOL)) i
Profunctor p => FunctorForRep (ProjTo2 p :: COLLAGE p +-> BOOL) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Collage

Methods

fmap :: forall (a :: COLLAGE p) (b :: COLLAGE p). (a ~> b) -> (ProjTo2 p @ a) ~> (ProjTo2 p @ b) Source Github #

type Objects BOOL Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

type Objects BOOL = '['FLS, 'TRU]
type Unit Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type Unit = TerminalObject :: BOOL
type InitialObject Source Github # 
Instance details

Defined in Proarrow.Colimit.Initial

type InitialObject = 'FLS
type NNO Source Github # 
Instance details

Defined in Proarrow.Colimit.NaturalNumbers

type NNO = 'TRU
type (~>) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Bool

type (~>) = Booleans
type TerminalObject Source Github # 
Instance details

Defined in Proarrow.Limit.Terminal

type TerminalObject = 'TRU
type At BOOL i Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

type At BOOL i = Lookup (Objects BOOL) i
type Index (a :: BOOL) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

type Index (a :: BOOL) = IndexOf a (Objects BOOL)
type Dual (a :: BOOL) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.StarAutonomous

type Dual (a :: BOOL) = Not a
type Ob (b :: BOOL) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Bool

type Ob (b :: BOOL) = IsBool b
type C0 BOOL Source Github # 
Instance details

Defined in Proarrow.Category.Internal

type C0 BOOL = 'FS Nat2
type C1 BOOL Source Github # 
Instance details

Defined in Proarrow.Category.Internal

type C1 BOOL = 'FS Nat3
type (a :: BOOL) ** (b :: BOOL) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type (a :: BOOL) ** (b :: BOOL) = a && b
type (a :: BOOL) ~~> (b :: BOOL) Source Github # 
Instance details

Defined in Proarrow.Category.Monoidal.Closed

type (a :: BOOL) ~~> (b :: BOOL) = BoolLeq a b
type 'FLS || (b :: BOOL) Source Github # 
Instance details

Defined in Proarrow.Colimit.BinaryCoproduct

type 'FLS || (b :: BOOL) = b
type 'TRU || (b :: BOOL) Source Github # 
Instance details

Defined in Proarrow.Colimit.BinaryCoproduct

type 'TRU || (b :: BOOL) = 'TRU
type (a :: BOOL) || 'FLS Source Github # 
Instance details

Defined in Proarrow.Colimit.BinaryCoproduct

type (a :: BOOL) || 'FLS = a
type (a :: BOOL) || 'TRU Source Github # 
Instance details

Defined in Proarrow.Colimit.BinaryCoproduct

type (a :: BOOL) || 'TRU = 'TRU
type 'FLS && (b :: BOOL) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type 'FLS && (b :: BOOL) = 'FLS
type 'TRU && (b :: BOOL) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type 'TRU && (b :: BOOL) = b
type (a :: BOOL) && 'FLS Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type (a :: BOOL) && 'FLS = 'FLS
type (a :: BOOL) && 'TRU Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

type (a :: BOOL) && 'TRU = a
type Booleans %% (x :: BOOL) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Corepresentable

type Booleans %% (x :: BOOL) = x
type Booleans % (x :: BOOL) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Representable

type Booleans % (x :: BOOL) = x
type HasArrow Booleans (a :: BOOL) (b :: BOOL) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

type HasArrow Booleans (a :: BOOL) (b :: BOOL) = Holds Booleans a b ~ 'TRU
type Holds Booleans (a :: BOOL) (b :: BOOL) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

type Holds Booleans (a :: BOOL) (b :: BOOL) = BoolLeq a b
type ProObj BOOL (p :: j +-> k) (a :: k) (b :: j) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched

type ProObj BOOL (p :: j +-> k) (a :: k) (b :: j) = Holds p a b
type HasArrow (NonTrivialProfunctor '(ff, tt) :: BOOL -> BOOL -> Type) (a :: BOOL) (b :: BOOL) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

type HasArrow (NonTrivialProfunctor '(ff, tt) :: BOOL -> BOOL -> Type) (a :: BOOL) (b :: BOOL) = Holds (NonTrivialProfunctor '(ff, tt)) a b ~ 'TRU
type Holds (NonTrivialProfunctor '(ff, tt) :: BOOL -> BOOL -> Type) (a :: BOOL) (b :: BOOL) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

type Holds (NonTrivialProfunctor '(ff, tt) :: BOOL -> BOOL -> Type) (a :: BOOL) (b :: BOOL) = NonTrivialHolds ff tt a b
type HasArrow (Edges es :: DISCRETE k -> DISCRETE k -> Type) (a :: DISCRETE k) (b :: DISCRETE k) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Instance.Edges

type HasArrow (Edges es :: DISCRETE k -> DISCRETE k -> Type) (a :: DISCRETE k) (b :: DISCRETE k) = Holds (Edges es) a b ~ 'TRU
type Holds (Edges es :: DISCRETE k -> DISCRETE k -> Type) (a :: DISCRETE k) (b :: DISCRETE k) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Instance.Edges

type Holds (Edges es :: DISCRETE k -> DISCRETE k -> Type) (a :: DISCRETE k) (b :: DISCRETE k) = WeightOf es a b
type Objects (BOOL, BOOL) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Product

type Objects (BOOL, BOOL) = '['('FLS, 'FLS), '('FLS, 'TRU), '('TRU, 'FLS), '('TRU, 'TRU)]
type At (BOOL, BOOL) i Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Product

type At (BOOL, BOOL) i = Lookup (Objects (BOOL, BOOL)) i
type Index (a :: (BOOL, BOOL)) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Product

type Index (a :: (BOOL, BOOL)) = IndexOf a (Objects (BOOL, BOOL))
type (ProjTo2 p :: COLLAGE p +-> BOOL) @ ('L a :: COLLAGE p) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Collage

type (ProjTo2 p :: COLLAGE p +-> BOOL) @ ('L a :: COLLAGE p) = 'FLS
type (ProjTo2 p :: COLLAGE p +-> BOOL) @ ('R a :: COLLAGE p) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Collage

type (ProjTo2 p :: COLLAGE p +-> BOOL) @ ('R a :: COLLAGE p) = 'TRU

data Booleans (a :: BOOL) (b :: BOOL) where Source Github #

Constructors

Fls :: Booleans 'FLS 'FLS 
F2T :: Booleans 'FLS 'TRU 
Tru :: Booleans 'TRU 'TRU 

Instances

Instances details
Promonad Booleans Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Bool

Methods

id :: forall (a :: BOOL). Ob a => Booleans a a Source Github #

(.) :: forall (b :: BOOL) (c :: BOOL) (a :: BOOL). Booleans b c -> Booleans a b -> Booleans a c Source Github #

Finitary Booleans Source Github #

BOOL is thin, so each hom-set holds at most the one arrow.

Instance details

Defined in Proarrow.Category.Enriched.Finitary

Methods

size :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b) => Natural Source Github #

toIndex :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b) => Booleans a b -> Natural Source Github #

fromIndex :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b) => Natural -> Booleans a b Source Github #

elements :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b) => [Booleans a b] Source Github #

DecidableProfunctor Booleans Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Associated Types

type Holds Booleans (a :: BOOL) (b :: BOOL) 
Instance details

Defined in Proarrow.Category.Enriched.Thin

type Holds Booleans (a :: BOOL) (b :: BOOL) = BoolLeq a b

Methods

decide :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b) => Decision Booleans a b (Holds Booleans a b) Source Github #

toHolds :: forall (a :: BOOL) (b :: BOOL) r. Booleans a b -> ((Holds Booleans a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

ThinProfunctor Booleans Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Associated Types

type HasArrow Booleans (a :: BOOL) (b :: BOOL) 
Instance details

Defined in Proarrow.Category.Enriched.Thin

type HasArrow Booleans (a :: BOOL) (b :: BOOL) = Holds Booleans a b ~ 'TRU

Methods

arr :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b, HasArrow Booleans a b) => Booleans a b Source Github #

withArr :: forall (a :: BOOL) (b :: BOOL) r. Booleans a b -> ((HasArrow Booleans a b, Ob a, Ob b) => r) -> r Source Github #

MonoidalProfunctor Booleans Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Methods

one :: Booleans (Unit :: BOOL) (Unit :: BOOL) Source Github #

(**) :: forall (x1 :: BOOL) (x2 :: BOOL) (y1 :: BOOL) (y2 :: BOOL). Booleans x1 x2 -> Booleans y1 y2 -> Booleans (x1 ** y1) (x2 ** y2) Source Github #

Profunctor Booleans Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Bool

Methods

dimap :: forall (c :: BOOL) (a :: BOOL) (b :: BOOL) (d :: BOOL). (c ~> a) -> (b ~> d) -> Booleans a b -> Booleans c d Source Github #

lmap :: forall (c :: BOOL) (a :: BOOL) (b :: BOOL). (c ~> a) -> Booleans a b -> Booleans c b Source Github #

rmap :: forall (b :: BOOL) (d :: BOOL) (a :: BOOL). (b ~> d) -> Booleans a b -> Booleans a d Source Github #

(\\) :: forall (a :: BOOL) (b :: BOOL) r. ((Ob a, Ob b) => r) -> Booleans a b -> r Source Github #

Corepresentable Booleans Source Github # 
Instance details

Defined in Proarrow.Profunctor.Corepresentable

Associated Types

type Booleans %% (x :: BOOL) 
Instance details

Defined in Proarrow.Profunctor.Corepresentable

type Booleans %% (x :: BOOL) = x

Methods

coindex :: forall (a :: BOOL) (b :: BOOL). Booleans a b -> (Booleans %% a) ~> b Source Github #

cotabulate :: forall (a :: BOOL) (b :: BOOL). Ob a => ((Booleans %% a) ~> b) -> Booleans a b Source Github #

corepMap :: forall (a :: BOOL) (b :: BOOL). (a ~> b) -> (Booleans %% a) ~> (Booleans %% b) Source Github #

corepUniv :: forall (a :: BOOL). Ob a => Booleans a (Booleans %% a) Source Github #

Representable Booleans Source Github # 
Instance details

Defined in Proarrow.Profunctor.Representable

Associated Types

type Booleans % (x :: BOOL) 
Instance details

Defined in Proarrow.Profunctor.Representable

type Booleans % (x :: BOOL) = x

Methods

index :: forall (a :: BOOL) (b :: BOOL). Booleans a b -> a ~> (Booleans % b) Source Github #

tabulate :: forall (b :: BOOL) (a :: BOOL). Ob b => (a ~> (Booleans % b)) -> Booleans a b Source Github #

repMap :: forall (a :: BOOL) (b :: BOOL). (a ~> b) -> (Booleans % a) ~> (Booleans % b) Source Github #

repUniv :: forall (a :: BOOL). Ob a => Booleans (Booleans % a) a Source Github #

Show (Booleans a b) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Bool

Methods

showsPrec :: Int -> Booleans a b -> ShowS Github #

show :: Booleans a b -> String Github #

showList :: [Booleans a b] -> ShowS Github #

Eq (Booleans a b) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Bool

Methods

(==) :: Booleans a b -> Booleans a b -> Bool Github #

(/=) :: Booleans a b -> Booleans a b -> Bool Github #

type Booleans %% (x :: BOOL) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Corepresentable

type Booleans %% (x :: BOOL) = x
type Booleans % (x :: BOOL) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Representable

type Booleans % (x :: BOOL) = x
type HasArrow Booleans (a :: BOOL) (b :: BOOL) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

type HasArrow Booleans (a :: BOOL) (b :: BOOL) = Holds Booleans a b ~ 'TRU
type Holds Booleans (a :: BOOL) (b :: BOOL) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

type Holds Booleans (a :: BOOL) (b :: BOOL) = BoolLeq a b

type family If (c :: BOOL) (t :: k) (e :: k) :: k where ... Source Github #

Type-level conditional on a BOOL.

Equations

If 'TRU (t :: k) (e :: k) = t 
If 'FLS (t :: k) (e :: k) = e 

type family Not (b :: BOOL) :: BOOL where ... Source Github #

Negation; the Dual of BOOL.

Equations

Not 'FLS = 'TRU 
Not 'TRU = 'FLS 

type family FromBool (b :: Bool) :: BOOL where ... Source Github #

GHC's own type-level Bool (as produced by e.g. <=? on Nat), as a BOOL.

Equations

FromBool 'True = 'TRU 
FromBool 'False = 'FLS 

class IsBool (Not b) => IsBool (b :: BOOL) where Source Github #

Methods

boolId :: b ~> b Source Github #

Instances

Instances details
IsBool 'FLS Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Bool

Methods

boolId :: 'FLS ~> 'FLS Source Github #

IsBool 'TRU Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Bool

Methods

boolId :: 'TRU ~> 'TRU Source Github #

type family BoolLeq (a :: BOOL) (b :: BOOL) :: BOOL where ... Source Github #

a <= b on the walking arrow, as a BOOL again: the hom of the walking arrow is its own internal hom.

Equations

BoolLeq 'TRU 'FLS = 'FLS 
BoolLeq a b = 'TRU 

data NonTrivialProfunctor (ft :: (BOOL, BOOL)) (a :: BOOL) (b :: BOOL) where Source Github #

The four non-trivial profunctors BOOL +-> BOOL, indexed by a pair of BOOLs selecting whether the FLS->FLS and TRU->TRU heteromorphisms are present. FLS->TRU always is.

Constructors

FF :: forall (tt :: BOOL). NonTrivialProfunctor '('TRU, tt) 'FLS 'FLS 
FT :: forall (ft :: (BOOL, BOOL)). NonTrivialProfunctor ft 'FLS 'TRU 
TT :: forall (ff :: BOOL). NonTrivialProfunctor '(ff, 'TRU) 'TRU 'TRU 

Instances

Instances details
(Ob ff, Ob tt) => DecidableProfunctor (NonTrivialProfunctor '(ff, tt) :: BOOL -> BOOL -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Methods

decide :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b) => Decision (NonTrivialProfunctor '(ff, tt)) a b (Holds (NonTrivialProfunctor '(ff, tt)) a b) Source Github #

toHolds :: forall (a :: BOOL) (b :: BOOL) r. NonTrivialProfunctor '(ff, tt) a b -> ((Holds (NonTrivialProfunctor '(ff, tt)) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

(Ob ff, Ob tt) => ThinProfunctor (NonTrivialProfunctor '(ff, tt) :: BOOL -> BOOL -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Methods

arr :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b, HasArrow (NonTrivialProfunctor '(ff, tt)) a b) => NonTrivialProfunctor '(ff, tt) a b Source Github #

withArr :: forall (a :: BOOL) (b :: BOOL) r. NonTrivialProfunctor '(ff, tt) a b -> ((HasArrow (NonTrivialProfunctor '(ff, tt)) a b, Ob a, Ob b) => r) -> r Source Github #

Profunctor (NonTrivialProfunctor ft :: BOOL -> BOOL -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Bool

Methods

dimap :: forall (c :: BOOL) (a :: BOOL) (b :: BOOL) (d :: BOOL). (c ~> a) -> (b ~> d) -> NonTrivialProfunctor ft a b -> NonTrivialProfunctor ft c d Source Github #

lmap :: forall (c :: BOOL) (a :: BOOL) (b :: BOOL). (c ~> a) -> NonTrivialProfunctor ft a b -> NonTrivialProfunctor ft c b Source Github #

rmap :: forall (b :: BOOL) (d :: BOOL) (a :: BOOL). (b ~> d) -> NonTrivialProfunctor ft a b -> NonTrivialProfunctor ft a d Source Github #

(\\) :: forall (a :: BOOL) (b :: BOOL) r. ((Ob a, Ob b) => r) -> NonTrivialProfunctor ft a b -> r Source Github #

Show (NonTrivialProfunctor ft a b) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Bool

Methods

showsPrec :: Int -> NonTrivialProfunctor ft a b -> ShowS Github #

show :: NonTrivialProfunctor ft a b -> String Github #

showList :: [NonTrivialProfunctor ft a b] -> ShowS Github #

Eq (NonTrivialProfunctor ft a b) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Bool

Methods

(==) :: NonTrivialProfunctor ft a b -> NonTrivialProfunctor ft a b -> Bool Github #

(/=) :: NonTrivialProfunctor ft a b -> NonTrivialProfunctor ft a b -> Bool Github #

type HasArrow (NonTrivialProfunctor '(ff, tt) :: BOOL -> BOOL -> Type) (a :: BOOL) (b :: BOOL) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

type HasArrow (NonTrivialProfunctor '(ff, tt) :: BOOL -> BOOL -> Type) (a :: BOOL) (b :: BOOL) = Holds (NonTrivialProfunctor '(ff, tt)) a b ~ 'TRU
type Holds (NonTrivialProfunctor '(ff, tt) :: BOOL -> BOOL -> Type) (a :: BOOL) (b :: BOOL) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

type Holds (NonTrivialProfunctor '(ff, tt) :: BOOL -> BOOL -> Type) (a :: BOOL) (b :: BOOL) = NonTrivialHolds ff tt a b

type family NonTrivialHolds (ff :: BOOL) (tt :: BOOL) (a :: BOOL) (b :: BOOL) :: BOOL where ... Source Github #

Which heteromorphisms NonTrivialProfunctor '(ff, tt) has.

Equations

NonTrivialHolds ff tt 'FLS 'FLS = ff 
NonTrivialHolds ff tt 'FLS 'TRU = 'TRU 
NonTrivialHolds ff tt 'TRU 'TRU = tt 
NonTrivialHolds ff tt 'TRU 'FLS = 'FLS