Safe Haskell	None
Language	GHC2024

Proarrow.Category.Instance.FinSet

Documentation

data FINSET Source Github #

Constructors

FS Nat

Instances

Instances details

Monoidal FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Associated Types

type Unit
Instance details Defined in Proarrow.Category.Instance.FinSet type Unit = 'FS Nat1
type (a :: FINSET) ** (b :: FINSET)
Instance details Defined in Proarrow.Category.Instance.FinSet type (a :: FINSET) ** (b :: FINSET) = a && b

Methods

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

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

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

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

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

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

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

SymMonoidal FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Methods

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

Closed FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Associated Types

type ('FS a :: FINSET) ~~> ('FS b :: FINSET)
Instance details Defined in Proarrow.Category.Instance.FinSet type ('FS a :: FINSET) ~~> ('FS b :: FINSET) = 'FS (Exp b a)

Methods

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

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

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

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

CopyDiscard FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Methods

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

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

Distributive FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Methods

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

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

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

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

ElementaryTopos FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

HasEpiMonoFactorization FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Methods

factorize :: forall (a :: FINSET) (b :: FINSET). (a ~> b) -> (Hom FINSET :.: Hom FINSET) a b Source Github #

HasSubobjectClassifier FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Associated Types

type Omega
Instance details Defined in Proarrow.Category.Instance.FinSet type Omega = 'FS Nat2

Methods

true :: (TerminalObject :: FINSET) ~> (Omega :: FINSET) Source Github #

classifyGraph :: forall (a :: FINSET) (b :: FINSET). (a ~> b) -> (a && b) ~> (Omega :: FINSET) Source Github #

HasBinaryCoproducts FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Associated Types

type ('FS a :: FINSET) \|\| ('FS b :: FINSET)
Instance details Defined in Proarrow.Category.Instance.FinSet type ('FS a :: FINSET) \|\| ('FS b :: FINSET) = 'FS (Plus a b)

Methods

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

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

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

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

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

HasCoequalizers FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Methods

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

factorCoequalizer :: forall (a :: FINSET) (b :: FINSET) (c :: FINSET). (a ~> b) -> (a ~> b) -> (b ~> c) -> (Hom FINSET :.: Hom FINSET) b c Source Github #

HasInitialObject FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Associated Types

type InitialObject
Instance details Defined in Proarrow.Category.Instance.FinSet type InitialObject = 'FS Nat0

Methods

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

HasPushouts FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Methods

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

CategoryOf FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Instance.FinSet type (~>) = FinSet
type Ob (a :: FINSET)
Instance details Defined in Proarrow.Category.Instance.FinSet type Ob (a :: FINSET) = (Is 'FS a, SNatI (UN 'FS a))

HasBinaryProducts FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Associated Types

type ('FS a :: FINSET) && ('FS b :: FINSET)
Instance details Defined in Proarrow.Category.Instance.FinSet type ('FS a :: FINSET) && ('FS b :: FINSET) = 'FS (Mult a b)

Methods

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

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

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

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

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

HasEqualizers FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Methods

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

factorEqualizer :: forall (a :: FINSET) (b :: FINSET) (c :: FINSET). (a ~> b) -> (a ~> b) -> (c ~> a) -> (Hom FINSET :.: Hom FINSET) c a Source Github #

HasPullbacks FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Methods

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

HasTerminalObject FINSET Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.FinSet type TerminalObject = 'FS Nat1

Methods

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

Promonad FinSet Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Methods

id :: forall (a :: FINSET). Ob a => FinSet a a Source Github #

(.) :: forall (b :: FINSET) (c :: FINSET) (a :: FINSET). FinSet b c -> FinSet a b -> FinSet a c Source Github #

InternalIn BOOL FINSET Source Github #

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 FinSet Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Methods

one :: FinSet (Unit :: FINSET) (Unit :: FINSET) Source Github #

(**) :: forall (x1 :: FINSET) (x2 :: FINSET) (y1 :: FINSET) (y2 :: FINSET). FinSet x1 x2 -> FinSet y1 y2 -> FinSet (x1 ** y1) (x2 ** y2) Source Github #

Profunctor FinSet Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Methods

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

lmap :: forall (c :: FINSET) (a :: FINSET) (b :: FINSET). (c ~> a) -> FinSet a b -> FinSet c b Source Github #

rmap :: forall (b :: FINSET) (d :: FINSET) (a :: FINSET). (b ~> d) -> FinSet a b -> FinSet a d Source Github #

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

FunctorForRep Fun Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinRel

Associated Types

type Fun @ ('FS a :: FINSET)
Instance details Defined in Proarrow.Category.Instance.FinRel type Fun @ ('FS a :: FINSET) = 'FR a

Methods

fmap :: forall (a :: FINSET) (b :: FINSET). (a ~> b) -> (Fun @ a) ~> (Fun @ b) Source Github #

MonoidalProfunctor (Rep Fun) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinRel

Methods

one :: Rep Fun (Unit :: FINREL) (Unit :: FINSET) Source Github #

(**) :: forall (x1 :: FINREL) (x2 :: FINSET) (y1 :: FINREL) (y2 :: FINSET). Rep Fun x1 x2 -> Rep Fun y1 y2 -> Rep Fun (x1 ** y1) (x2 ** y2) Source Github #

SNatI a => Comonoid ('FS a :: FINSET) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Methods

counit :: 'FS a ~> (Unit :: FINSET) Source Github #

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

Monoid ('FS Nat1) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

Methods

mempty :: (Unit :: FINSET) ~> 'FS Nat1 Source Github #

mappend :: ('FS Nat1 ** 'FS Nat1) ~> 'FS Nat1 Source Github #

MonoidalProfunctor (Coprod (Rep Fun)) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinRel

Methods

one :: Coprod (Rep Fun) (Unit :: COPROD FINREL) (Unit :: COPROD FINSET) Source Github #

(**) :: forall (x1 :: COPROD FINREL) (x2 :: COPROD FINSET) (y1 :: COPROD FINREL) (y2 :: COPROD FINSET). Coprod (Rep Fun) x1 x2 -> Coprod (Rep Fun) y1 y2 -> Coprod (Rep Fun) (x1 ** y1) (x2 ** y2) Source Github #

type Unit Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

type Unit = 'FS Nat1

type Omega Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

type Omega = 'FS Nat2

type InitialObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

type InitialObject = 'FS Nat0

type (~>) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

type (~>) = FinSet

type TerminalObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

type TerminalObject = 'FS Nat1

type Ob (a :: FINSET) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

type Ob (a :: FINSET) = (Is 'FS a, SNatI (UN 'FS a))

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 :: FINSET) ** (b :: FINSET) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

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

type Fun @ ('FS a :: FINSET) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinRel

type Fun @ ('FS a :: FINSET) = 'FR a

type ('FS a :: FINSET) ~~> ('FS b :: FINSET) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

type ('FS a :: FINSET) ~~> ('FS b :: FINSET) = 'FS (Exp b a)

type ('FS a :: FINSET) || ('FS b :: FINSET) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

type ('FS a :: FINSET) || ('FS b :: FINSET) = 'FS (Plus a b)

type ('FS a :: FINSET) && ('FS b :: FINSET) Source Github #

Instance details

Defined in Proarrow.Category.Instance.FinSet

type ('FS a :: FINSET) && ('FS b :: FINSET) = 'FS (Mult a b)

data FinSet (a :: FINSET) (b :: FINSET) where Source Github #

Constructors

FinSet
Fields :: forall (n :: Nat) (m :: Nat). (SNatI n, SNatI m) => { unFinSet :: Vec n (Fin m) } -> FinSet ('FS n) ('FS m)

Instances

Instances details

Promonad FinSet Source Github #
Instance details Defined in Proarrow.Category.Instance.FinSet Methods id :: forall (a :: FINSET). Ob a => FinSet a a Source Github # (.) :: forall (b :: FINSET) (c :: FINSET) (a :: FINSET). FinSet b c -> FinSet a b -> FinSet a c Source Github #
MonoidalProfunctor FinSet Source Github #
Instance details Defined in Proarrow.Category.Instance.FinSet Methods one :: FinSet (Unit :: FINSET) (Unit :: FINSET) Source Github # () :: forall (x1 :: FINSET) (x2 :: FINSET) (y1 :: FINSET) (y2 :: FINSET). FinSet x1 x2 -> FinSet y1 y2 -> FinSet (x1 y1) (x2 ** y2) Source Github #
Profunctor FinSet Source Github #
Instance details Defined in Proarrow.Category.Instance.FinSet Methods dimap :: forall (c :: FINSET) (a :: FINSET) (b :: FINSET) (d :: FINSET). (c ~> a) -> (b ~> d) -> FinSet a b -> FinSet c d Source Github # lmap :: forall (c :: FINSET) (a :: FINSET) (b :: FINSET). (c ~> a) -> FinSet a b -> FinSet c b Source Github # rmap :: forall (b :: FINSET) (d :: FINSET) (a :: FINSET). (b ~> d) -> FinSet a b -> FinSet a d Source Github # (\\) :: forall (a :: FINSET) (b :: FINSET) r. ((Ob a, Ob b) => r) -> FinSet a b -> r Source Github #
Show (FinSet a b) Source Github #
Instance details Defined in Proarrow.Category.Instance.FinSet Methods showsPrec :: Int -> FinSet a b -> ShowS Github # show :: FinSet a b -> String Github # showList :: [FinSet a b] -> ShowS Github #
Eq (FinSet a b) Source Github #
Instance details Defined in Proarrow.Category.Instance.FinSet Methods (==) :: FinSet a b -> FinSet a b -> Bool Github # (/=) :: FinSet a b -> FinSet a b -> Bool Github #

mult :: forall (n :: Nat) (m :: Nat). (SNatI n, SNatI m) => Fin n -> Fin m -> Fin (Mult n m) Source Github #

unmult :: forall (n :: Nat) (m :: Nat). (SNatI n, SNatI m) => Fin (Mult n m) -> (Fin n, Fin m) Source Github #

type family Exp (a :: Nat) (b :: Nat) :: Nat where ... Source Github #

Equations

Exp a 'Z = 'S 'Z
Exp a ('S n) = Mult a (Exp a n)

exp :: forall (n :: Nat) (m :: Nat). (SNatI n, SNatI m) => Vec n (Fin m) -> Fin (Exp m n) Source Github #

unExp :: forall (n :: Nat) (m :: Nat). (SNatI n, SNatI m) => Fin (Exp m n) -> Vec n (Fin m) Source Github #

findIso :: forall (n :: Nat). SNatI n => [(Fin n, Fin n)] -> Maybe (Iso' ('FS n) ('FS n)) Source Github #

findArr :: forall (n :: Nat). SNatI n => [(Fin n, Fin n)] -> Maybe ('FS n ~> 'FS n) Source Github #

findIndex :: forall a (n :: Nat). (a -> Bool) -> Vec n a -> Fin n Source Github #