Safe Haskell	None
Language	GHC2024

Proarrow.Category.Bicategory.Strictified

Synopsis

data Path (kk :: CAT k) (j :: k) (k1 :: k) where
- Nil :: forall {k} (kk :: CAT k) (j :: k). Path kk j j
- (:::) :: forall {k} (kk :: CAT k) (j :: k) (j1 :: k) (k1 :: k). kk j j1 -> Path kk j1 k1 -> Path kk j k1
type family (ps :: Path kk a b) +++ (qs :: Path kk b c) :: Path kk a c
data SPath (ps :: Path kk j k1) where
- SNil :: forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath ('Nil :: Path kk j j)
- SCons :: forall {k} {kk :: CAT k} {j :: k} {j1 :: k} {k1 :: k} (p :: kk j j1) (ps1 :: Path kk j1 k1). Ob0 kk j => Obj p -> SPath ps1 -> SPath (p '::: ps1)
class ((as +++ bs) +++ cs) ~ (as +++ (bs +++ cs)) => Assoc (as :: Path kk a a1) (bs :: Path kk a1 b) (cs :: Path kk b c)
class (Bicategory kk, Ob0 kk j, Ob0 kk k1, (ps +++ ('Nil :: Path kk k1 k1)) ~ ps, forall (i :: k) (h :: k) (qs :: Path kk k1 h) (rs :: Path kk h i). Assoc ps qs rs) => IsPath (ps :: Path kk j k1) where
- singPath :: SPath ps
- withIsPath2 :: forall {c :: k} (qs :: Path kk k1 c) r. IsPath qs => (Ob (ps +++ qs) => r) -> r
- withPathO2 :: forall {c :: k} tag (qs :: Path kk k1 c) r. (IsOb tag ps, IsOb tag qs, Ob qs) => ((IsOb tag (ps +++ qs), Ob (ps +++ qs)) => r) -> r
withIsPath :: forall {k1} (kk :: CAT k1) (j :: k1) (k2 :: k1) (ps :: Path kk j k2) r. Bicategory kk => SPath ps -> ((Ob ps, Ob0 kk j, Ob0 kk k2) => r) -> r
append :: forall {k1} {kk :: CAT k1} {j :: k1} {b :: k1} {k2 :: k1} (ps :: Path kk j b) (qs :: Path kk b k2). SPath ps -> SPath qs -> SPath (ps +++ qs)
singleton :: forall {k} (kk :: CAT k) (i :: k) (j :: k) (p :: kk i j) (q :: kk i j). Bicategory kk => (p ~> q) -> (p '::: ('Nil :: Path kk j j)) ~> (q '::: ('Nil :: Path kk j j))
obj1 :: forall {k} {kk :: CAT k} {i :: k} {j :: k} (p :: kk i j). (Bicategory kk, Ob p, Ob0 kk i, Ob0 kk j) => Obj (p '::: ('Nil :: Path kk j j))
asObj :: forall {k} (kk :: CAT k) (i :: k) (j :: k) (ps :: Path kk i j). Bicategory kk => SPath ps -> Obj ps
concatFold :: forall {k1} {kk :: CAT k1} {i :: k1} {j :: k1} {k2 :: k1} (as :: Path kk i j) (bs :: Path kk j k2). Bicategory kk => SPath as -> SPath bs -> O (Fold bs) (Fold as) ~> Fold (as +++ bs)
splitFold :: forall {k1} {kk :: CAT k1} {i :: k1} {j :: k1} {k2 :: k1} (as :: Path kk i j) (bs :: Path kk j k2). Bicategory kk => SPath as -> SPath bs -> Fold (as +++ bs) ~> O (Fold bs) (Fold as)
type family Fold (as :: Path kk j k1) :: kk j k1
fold :: forall {k} {kk :: CAT k} {i :: k} {j :: k} (as :: Path kk i j). Bicategory kk => SPath as -> Fold as ~> Fold as
combineAll :: forall {k} {kk :: CAT k} {i :: k} {j :: k} (as :: Path kk i j). (Bicategory kk, Ob as) => as ~> (Fold as '::: ('Nil :: Path kk j j))
splitAll :: forall {k} {kk :: CAT k} {i :: k} {j :: k} (as :: Path kk i j). (Bicategory kk, Ob as) => (Fold as '::: ('Nil :: Path kk j j)) ~> as
data Strictified (ps :: Path kk j k1) (qs :: Path kk j k1) where
- St :: forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1) (qs :: Path kk j k1). (Ob ps, Ob qs) => (Fold ps ~> Fold qs) -> Strictified ps qs
view :: forall {k1} (kk :: CAT k1) (j :: k1) (k2 :: k1) (ps :: Path kk j k2) (qs :: Path kk j k2). Strictified ps qs -> (Strictified ps qs, SPath ps, SPath qs)
pattern Str :: Bicategory kk => (Ob0 kk j, Ob0 kk k2) => SPath ps -> SPath qs -> (Fold ps ~> Fold qs) -> Strictified ps qs
unStr :: forall {k1} {kk :: CAT k1} {j :: k1} {k2 :: k1} (ps :: Path kk j k2) (qs :: Path kk j k2). Strictified ps qs -> Fold ps ~> Fold qs
introI :: forall {k} {kk :: CAT k} {j :: k}. (Ob0 kk j, Bicategory kk) => ('Nil :: Path kk j j) ~> ((I :: kk j j) '::: ('Nil :: Path kk j j))
elimI :: forall {s} {kk :: CAT s} {j :: s}. (Ob0 kk j, Bicategory kk) => ((I :: kk j j) '::: ('Nil :: Path kk j j)) ~> ('Nil :: Path kk j j)
introO :: forall {k1} {kk :: k1 -> k1 -> Type} {i :: k1} {j :: k1} {k2 :: k1} (p :: kk i j) (q :: kk j k2). (Ob0 kk i, Ob0 kk j, Ob0 kk k2, Bicategory kk, Ob p, Ob q) => (p '::: (q '::: ('Nil :: Path kk k2 k2))) ~> (O q p '::: ('Nil :: Path kk k2 k2))
elimO :: forall {k1} {kk :: k1 -> k1 -> Type} {i :: k1} {j :: k1} {k2 :: k1} (p :: kk i j) (q :: kk j k2). (Ob0 kk i, Ob0 kk j, Ob0 kk k2, Bicategory kk, Ob p, Ob q) => (O q p '::: ('Nil :: Path kk k2 k2)) ~> (p '::: (q '::: ('Nil :: Path kk k2 k2)))
stUnit :: forall {k} {kk :: k -> k -> Type} {i :: k} {j :: k} (p :: kk i j) (q :: kk j i). (Adjunction p q, Ob p, Ob q) => ('Nil :: Path kk i i) ~> (p '::: (q '::: ('Nil :: Path kk i i)))
stCounit :: forall {k} {kk :: k -> k -> Type} {i :: k} {j :: k} (p :: kk i j) (q :: kk j i). (Adjunction p q, Ob p, Ob q) => (q '::: (p '::: ('Nil :: Path kk j j))) ~> ('Nil :: Path kk j j)
withIsObTagFold :: forall {k1} {kk :: CAT k1} {j :: k1} {k2 :: k1} tag (ps :: Path kk j k2) r. (Bicategory (SUBCAT tag kk), WithObO2 tag kk, IsOb tag ps, Ob ps) => ((IsOb tag (Fold ps), Ob (Fold ps)) => r) -> r

Documentation

data Path (kk :: CAT k) (j :: k) (k1 :: k) where Source Comments #

The type of 2-parameter kind constructors.

A type-level kind-threaded list. Used to strictify the bicategory and double category definitions. kk is a kind constructor, which creates a kind given two other kinds. (Each kind representing a 0-cell.)

Constructors

Nil :: forall {k} (kk :: CAT k) (j :: k). Path kk j j
(:::) :: forall {k} (kk :: CAT k) (j :: k) (j1 :: k) (k1 :: k). kk j j1 -> Path kk j1 k1 -> Path kk j k1 infixr 5

Instances

Instances details

WithObO2 tag kk => WithObO2 tag (Path kk :: s -> s -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Strictified

Methods

withObO2 :: forall {i :: s} {j :: s} {k :: s} (a :: Path kk j k) (b :: Path kk i j) r. (Ob a, Ob b, IsOb tag a, IsOb tag b) => ((IsOb tag (O a b), Ob (O a b)) => r) -> r Source Comments #

Bicategory kk => Bicategory (Path kk :: s -> s -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Strictified

Methods

o :: forall {i :: s} (j :: s) (k :: s) (a :: Path kk j k) (b :: Path kk j k) (c :: Path kk i j) (d :: Path kk i j). (a ~> b) -> (c ~> d) -> O a c ~> O b d Source Comments #

withOb2 :: forall {i :: s} {j :: s} {k :: s} (a :: Path kk j k) (b :: Path kk i j) r. (Ob a, Ob b, Ob0 (Path kk) i, Ob0 (Path kk) j, Ob0 (Path kk) k) => (Ob (O a b) => r) -> r Source Comments #

withOb0s :: forall {j :: s} {k :: s} (a :: Path kk j k) r. Ob a => ((Ob0 (Path kk) j, Ob0 (Path kk) k) => r) -> r Source Comments #

(\\\) :: forall (i :: s) (j :: s) (ps :: Path kk i j) (qs :: Path kk i j) r. ((Ob0 (Path kk) i, Ob0 (Path kk) j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r Source Comments #

leftUnitor :: forall {i :: s} {j :: s} (a :: Path kk i j). (Ob0 (Path kk) i, Ob0 (Path kk) j, Ob a) => O (I :: Path kk j j) a ~> a Source Comments #

leftUnitorInv :: forall {i :: s} {j :: s} (a :: Path kk i j). (Ob0 (Path kk) i, Ob0 (Path kk) j, Ob a) => a ~> O (I :: Path kk j j) a Source Comments #

rightUnitor :: forall {i :: s} {j :: s} (a :: Path kk i j). (Ob0 (Path kk) i, Ob0 (Path kk) j, Ob a) => O a (I :: Path kk i i) ~> a Source Comments #

rightUnitorInv :: forall {i :: s} {j :: s} (a :: Path kk i j). (Ob0 (Path kk) i, Ob0 (Path kk) j, Ob a) => a ~> O a (I :: Path kk i i) Source Comments #

associator :: forall {h :: s} {i :: s} {j :: s} {k :: s} (a :: Path kk j k) (b :: Path kk i j) (c :: Path kk h i). (Ob0 (Path kk) h, Ob0 (Path kk) i, Ob0 (Path kk) j, Ob0 (Path kk) k, Ob a, Ob b, Ob c) => O (O a b) c ~> O a (O b c) Source Comments #

associatorInv :: forall {h :: s} {i :: s} {j :: s} {k :: s} (a :: Path kk j k) (b :: Path kk i j) (c :: Path kk h i). (Ob0 (Path kk) h, Ob0 (Path kk) i, Ob0 (Path kk) j, Ob0 (Path kk) k, Ob a, Ob b, Ob c) => O a (O b c) ~> O (O a b) c Source Comments #

(Bicategory kk, Ob0 kk a) => Adjunction_ ('Nil :: Path kk a a) ('Nil :: Path kk a a) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Strictified

Methods

adj :: Adj ('Nil :: Path kk a a) ('Nil :: Path kk a a) Source Comments #

(Bicategory kk, Adjunction l r, Ob0 kk j, Ob0 kk k2) => Adjunction_ (l '::: ('Nil :: Path kk k2 k2) :: Path kk j k2) (r '::: ('Nil :: Path kk j j) :: Path kk k2 j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Strictified

Methods

adj :: Adj (l '::: ('Nil :: Path kk k2 k2)) (r '::: ('Nil :: Path kk j j)) Source Comments #

(Bicategory kk, Ob0 kk a) => Comonad ('Nil :: Path kk a a) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Strictified

Methods

epsilon :: ('Nil :: Path kk a a) ~> (I :: Path kk a a) Source Comments #

delta :: ('Nil :: Path kk a a) ~> O ('Nil :: Path kk a a) ('Nil :: Path kk a a) Source Comments #

(Bicategory kk, Ob0 kk a) => Monad ('Nil :: Path kk a a) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Strictified

Methods

eta :: (I :: Path kk a a) ~> ('Nil :: Path kk a a) Source Comments #

mu :: O ('Nil :: Path kk a a) ('Nil :: Path kk a a) ~> ('Nil :: Path kk a a) Source Comments #

(Adjunction l r, Ob r, Ob l, Ob0 kk i, Ob0 kk j) => Comonad (r '::: (l '::: ('Nil :: Path kk i i)) :: Path kk i i) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Strictified

Methods

epsilon :: (r '::: (l '::: ('Nil :: Path kk i i))) ~> (I :: Path kk i i) Source Comments #

delta :: (r '::: (l '::: ('Nil :: Path kk i i))) ~> O (r '::: (l '::: ('Nil :: Path kk i i))) (r '::: (l '::: ('Nil :: Path kk i i))) Source Comments #

(Monad s, Ob s, Ob0 kk a) => Monad (s '::: ('Nil :: Path kk a a) :: Path kk a a) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Strictified

Methods

eta :: (I :: Path kk a a) ~> (s '::: ('Nil :: Path kk a a)) Source Comments #

mu :: O (s '::: ('Nil :: Path kk a a)) (s '::: ('Nil :: Path kk a a)) ~> (s '::: ('Nil :: Path kk a a)) Source Comments #

(Adjunction l r, Ob r, Ob l, Ob0 kk i, Ob0 kk j) => Monad (l '::: (r '::: ('Nil :: Path kk j j)) :: Path kk j j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Strictified

Methods

eta :: (I :: Path kk j j) ~> (l '::: (r '::: ('Nil :: Path kk j j))) Source Comments #

mu :: O (l '::: (r '::: ('Nil :: Path kk j j))) (l '::: (r '::: ('Nil :: Path kk j j))) ~> (l '::: (r '::: ('Nil :: Path kk j j))) Source Comments #

(CategoryOf (kk j k2), Bicategory kk) => CategoryOf (Path kk j k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Strictified

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Bicategory.Strictified type (~>) = Strictified :: Path kk j k2 -> Path kk j k2 -> Type

(CategoryOf (kk j k2), Bicategory kk) => Promonad (Strictified :: Path kk j k2 -> Path kk j k2 -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Strictified

Methods

id :: forall (a :: Path kk j k2). Ob a => Strictified a a Source Comments #

(.) :: forall (b :: Path kk j k2) (c :: Path kk j k2) (a :: Path kk j k2). Strictified b c -> Strictified a b -> Strictified a c Source Comments #

(CategoryOf (kk j k2), Bicategory kk) => Profunctor (Strictified :: Path kk j k2 -> Path kk j k2 -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Strictified

Methods

dimap :: forall (c :: Path kk j k2) (a :: Path kk j k2) (b :: Path kk j k2) (d :: Path kk j k2). (c ~> a) -> (b ~> d) -> Strictified a b -> Strictified c d Source Comments #

(\\) :: forall (a :: Path kk j k2) (b :: Path kk j k2) r. ((Ob a, Ob b) => r) -> Strictified a b -> r Source Comments #

type Ob0 (Path kk :: s -> s -> Type) (j :: k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Strictified

type Ob0 (Path kk :: s -> s -> Type) (j :: k) = Ob0 kk j

type IsOb tag ('Nil :: Path kk i i) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Strictified

type IsOb tag ('Nil :: Path kk i i) = ()

type IsOb tag (p '::: ps :: Path kk i1 j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Strictified

type IsOb tag (p '::: ps :: Path kk i1 j) = (IsOb tag p, IsOb tag ps)

type I Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Strictified

type I = 'Nil :: Path kk i i

type O (ps :: Path kk b c) (qs :: Path kk a b) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Strictified

type O (ps :: Path kk b c) (qs :: Path kk a b) = qs +++ ps

type (~>) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Strictified

type (~>) = Strictified :: Path kk j k2 -> Path kk j k2 -> Type

type Ob (ps :: Path kk j k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Strictified

type Ob (ps :: Path kk j k2) = (IsPath ps, Ob0 kk j, Ob0 kk k2)

type UN ('AK :: Path ABK i j -> ADJK i j) ('AK ps :: ADJK i j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

type UN ('AK :: Path ABK i j -> ADJK i j) ('AK ps :: ADJK i j) = ps

type family (ps :: Path kk a b) +++ (qs :: Path kk b c) :: Path kk a c infixl 5 Source Comments #

Instances

Instances details

type ('Nil :: Path kk b b) +++ (qs :: Path kk b c) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Strictified type ('Nil :: Path kk b b) +++ (qs :: Path kk b c) = qs
type (p '::: ps :: Path kk i b) +++ (qs :: Path kk b k2) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Strictified type (p '::: ps :: Path kk i b) +++ (qs :: Path kk b k2) = p '::: (ps +++ qs)

data SPath (ps :: Path kk j k1) where Source Comments #

Constructors

SNil :: forall {k} (kk :: CAT k) (j :: k). Ob0 kk j => SPath ('Nil :: Path kk j j)
SCons :: forall {k} {kk :: CAT k} {j :: k} {j1 :: k} {k1 :: k} (p :: kk j j1) (ps1 :: Path kk j1 k1). Ob0 kk j => Obj p -> SPath ps1 -> SPath (p '::: ps1)

class ((as +++ bs) +++ cs) ~ (as +++ (bs +++ cs)) => Assoc (as :: Path kk a a1) (bs :: Path kk a1 b) (cs :: Path kk b c) Source Comments #

Instances

Instances details

(as +++ (bs +++ cs)) ~ ((as +++ bs) +++ cs) => Assoc (as :: Path kk a1 a2) (bs :: Path kk a2 b) (cs :: Path kk b c) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Strictified

class (Bicategory kk, Ob0 kk j, Ob0 kk k1, (ps +++ ('Nil :: Path kk k1 k1)) ~ ps, forall (i :: k) (h :: k) (qs :: Path kk k1 h) (rs :: Path kk h i). Assoc ps qs rs) => IsPath (ps :: Path kk j k1) where Source Comments #

Methods

singPath :: SPath ps Source Comments #

withIsPath2 :: forall {c :: k} (qs :: Path kk k1 c) r. IsPath qs => (Ob (ps +++ qs) => r) -> r Source Comments #

withPathO2 :: forall {c :: k} tag (qs :: Path kk k1 c) r. (IsOb tag ps, IsOb tag qs, Ob qs) => ((IsOb tag (ps +++ qs), Ob (ps +++ qs)) => r) -> r Source Comments #

Instances

Instances details

(Bicategory kk, Ob0 kk k2) => IsPath ('Nil :: Path kk k2 k2) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Strictified Methods singPath :: SPath ('Nil :: Path kk k2 k2) Source Comments # withIsPath2 :: forall {c :: k1} (qs :: Path kk k2 c) r. IsPath qs => (Ob (('Nil :: Path kk k2 k2) +++ qs) => r) -> r Source Comments # withPathO2 :: forall {c :: k1} tag (qs :: Path kk k2 c) r. (IsOb tag ('Nil :: Path kk k2 k2), IsOb tag qs, Ob qs) => ((IsOb tag (('Nil :: Path kk k2 k2) +++ qs), Ob (('Nil :: Path kk k2 k2) +++ qs)) => r) -> r Source Comments #
(Ob0 kk i, Ob p, IsPath ps) => IsPath (p '::: ps :: Path kk i k2) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Strictified Methods singPath :: SPath (p '::: ps) Source Comments # withIsPath2 :: forall {c :: k1} (qs :: Path kk k2 c) r. IsPath qs => (Ob ((p '::: ps) +++ qs) => r) -> r Source Comments # withPathO2 :: forall {c :: k1} tag (qs :: Path kk k2 c) r. (IsOb tag (p '::: ps), IsOb tag qs, Ob qs) => ((IsOb tag ((p '::: ps) +++ qs), Ob ((p '::: ps) +++ qs)) => r) -> r Source Comments #

withIsPath :: forall {k1} (kk :: CAT k1) (j :: k1) (k2 :: k1) (ps :: Path kk j k2) r. Bicategory kk => SPath ps -> ((Ob ps, Ob0 kk j, Ob0 kk k2) => r) -> r Source Comments #

append :: forall {k1} {kk :: CAT k1} {j :: k1} {b :: k1} {k2 :: k1} (ps :: Path kk j b) (qs :: Path kk b k2). SPath ps -> SPath qs -> SPath (ps +++ qs) Source Comments #

singleton :: forall {k} (kk :: CAT k) (i :: k) (j :: k) (p :: kk i j) (q :: kk i j). Bicategory kk => (p ~> q) -> (p '::: ('Nil :: Path kk j j)) ~> (q '::: ('Nil :: Path kk j j)) Source Comments #

obj1 :: forall {k} {kk :: CAT k} {i :: k} {j :: k} (p :: kk i j). (Bicategory kk, Ob p, Ob0 kk i, Ob0 kk j) => Obj (p '::: ('Nil :: Path kk j j)) Source Comments #

asObj :: forall {k} (kk :: CAT k) (i :: k) (j :: k) (ps :: Path kk i j). Bicategory kk => SPath ps -> Obj ps Source Comments #

concatFold :: forall {k1} {kk :: CAT k1} {i :: k1} {j :: k1} {k2 :: k1} (as :: Path kk i j) (bs :: Path kk j k2). Bicategory kk => SPath as -> SPath bs -> O (Fold bs) (Fold as) ~> Fold (as +++ bs) Source Comments #

splitFold :: forall {k1} {kk :: CAT k1} {i :: k1} {j :: k1} {k2 :: k1} (as :: Path kk i j) (bs :: Path kk j k2). Bicategory kk => SPath as -> SPath bs -> Fold (as +++ bs) ~> O (Fold bs) (Fold as) Source Comments #

type family Fold (as :: Path kk j k1) :: kk j k1 Source Comments #

Instances

Instances details

type Fold ('Nil :: Path kk j j) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Strictified type Fold ('Nil :: Path kk j j) = I :: kk j j
type Fold (p '::: (q '::: ps) :: Path kk i k2) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Strictified type Fold (p '::: (q '::: ps) :: Path kk i k2) = O (Fold (q '::: ps)) p
type Fold (p '::: ('Nil :: Path kk k2 k2) :: Path kk j k2) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Strictified type Fold (p '::: ('Nil :: Path kk k2 k2) :: Path kk j k2) = p

fold :: forall {k} {kk :: CAT k} {i :: k} {j :: k} (as :: Path kk i j). Bicategory kk => SPath as -> Fold as ~> Fold as Source Comments #

combineAll :: forall {k} {kk :: CAT k} {i :: k} {j :: k} (as :: Path kk i j). (Bicategory kk, Ob as) => as ~> (Fold as '::: ('Nil :: Path kk j j)) Source Comments #

splitAll :: forall {k} {kk :: CAT k} {i :: k} {j :: k} (as :: Path kk i j). (Bicategory kk, Ob as) => (Fold as '::: ('Nil :: Path kk j j)) ~> as Source Comments #

data Strictified (ps :: Path kk j k1) (qs :: Path kk j k1) where Source Comments #

Constructors

St :: forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (ps :: Path kk j k1) (qs :: Path kk j k1). (Ob ps, Ob qs) => (Fold ps ~> Fold qs) -> Strictified ps qs

Instances

Instances details

(CategoryOf (kk j k2), Bicategory kk) => Promonad (Strictified :: Path kk j k2 -> Path kk j k2 -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Strictified Methods id :: forall (a :: Path kk j k2). Ob a => Strictified a a Source Comments # (.) :: forall (b :: Path kk j k2) (c :: Path kk j k2) (a :: Path kk j k2). Strictified b c -> Strictified a b -> Strictified a c Source Comments #
(CategoryOf (kk j k2), Bicategory kk) => Profunctor (Strictified :: Path kk j k2 -> Path kk j k2 -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Strictified Methods dimap :: forall (c :: Path kk j k2) (a :: Path kk j k2) (b :: Path kk j k2) (d :: Path kk j k2). (c ~> a) -> (b ~> d) -> Strictified a b -> Strictified c d Source Comments # (\\) :: forall (a :: Path kk j k2) (b :: Path kk j k2) r. ((Ob a, Ob b) => r) -> Strictified a b -> r Source Comments #

view :: forall {k1} (kk :: CAT k1) (j :: k1) (k2 :: k1) (ps :: Path kk j k2) (qs :: Path kk j k2). Strictified ps qs -> (Strictified ps qs, SPath ps, SPath qs) Source Comments #

pattern Str :: Bicategory kk => (Ob0 kk j, Ob0 kk k2) => SPath ps -> SPath qs -> (Fold ps ~> Fold qs) -> Strictified ps qs Source Comments #

unStr :: forall {k1} {kk :: CAT k1} {j :: k1} {k2 :: k1} (ps :: Path kk j k2) (qs :: Path kk j k2). Strictified ps qs -> Fold ps ~> Fold qs Source Comments #

introI :: forall {k} {kk :: CAT k} {j :: k}. (Ob0 kk j, Bicategory kk) => ('Nil :: Path kk j j) ~> ((I :: kk j j) '::: ('Nil :: Path kk j j)) Source Comments #

elimI :: forall {s} {kk :: CAT s} {j :: s}. (Ob0 kk j, Bicategory kk) => ((I :: kk j j) '::: ('Nil :: Path kk j j)) ~> ('Nil :: Path kk j j) Source Comments #

introO :: forall {k1} {kk :: k1 -> k1 -> Type} {i :: k1} {j :: k1} {k2 :: k1} (p :: kk i j) (q :: kk j k2). (Ob0 kk i, Ob0 kk j, Ob0 kk k2, Bicategory kk, Ob p, Ob q) => (p '::: (q '::: ('Nil :: Path kk k2 k2))) ~> (O q p '::: ('Nil :: Path kk k2 k2)) Source Comments #

elimO :: forall {k1} {kk :: k1 -> k1 -> Type} {i :: k1} {j :: k1} {k2 :: k1} (p :: kk i j) (q :: kk j k2). (Ob0 kk i, Ob0 kk j, Ob0 kk k2, Bicategory kk, Ob p, Ob q) => (O q p '::: ('Nil :: Path kk k2 k2)) ~> (p '::: (q '::: ('Nil :: Path kk k2 k2))) Source Comments #

stUnit :: forall {k} {kk :: k -> k -> Type} {i :: k} {j :: k} (p :: kk i j) (q :: kk j i). (Adjunction p q, Ob p, Ob q) => ('Nil :: Path kk i i) ~> (p '::: (q '::: ('Nil :: Path kk i i))) Source Comments #

stCounit :: forall {k} {kk :: k -> k -> Type} {i :: k} {j :: k} (p :: kk i j) (q :: kk j i). (Adjunction p q, Ob p, Ob q) => (q '::: (p '::: ('Nil :: Path kk j j))) ~> ('Nil :: Path kk j j) Source Comments #

withIsObTagFold :: forall {k1} {kk :: CAT k1} {j :: k1} {k2 :: k1} tag (ps :: Path kk j k2) r. (Bicategory (SUBCAT tag kk), WithObO2 tag kk, IsOb tag ps, Ob ps) => ((IsOb tag (Fold ps), Ob (Fold ps)) => r) -> r Source Comments #