Safe Haskell	None
Language	GHC2024

Proarrow.Category.Bicategory.Adj

Synopsis

data AB
- = A
- | B
data ABK (a :: AB) (b :: AB) where
- L :: ABK 'A 'B
- R :: ABK 'B 'A
data ADJK (i :: AB) (j :: AB) = AK (Path ABK i j)
data Adj (ps :: ADJK i j) (qs :: ADJK i j) where
- AdjNil :: forall {i :: AB}. Adj ('AK ('Nil :: Path ABK i i)) ('AK ('Nil :: Path ABK i i))
- AdjR :: forall {j :: AB} (ps1 :: Path ABK 'A j) (qs1 :: Path ABK 'A j). Adj ('AK ps1) ('AK qs1) -> Adj ('AK ('R '::: ps1)) ('AK ('R '::: qs1))
- AdjL :: forall {j :: AB} (ps1 :: Path ABK 'B j) (qs1 :: Path ABK 'B j). Adj ('AK ps1) ('AK qs1) -> Adj ('AK ('L '::: ps1)) ('AK ('L '::: qs1))
- AdjCup :: forall {j :: AB} (ps1 :: Path ABK 'B j) (qs1 :: ADJK 'B j). Adj ('AK ps1) qs1 -> Adj ('AK ('R '::: ('L '::: ps1))) qs1
- AdjCap :: forall {j :: AB} (ps1 :: ADJK 'A j) (qs1 :: Path ABK 'A j). Adj ps1 ('AK qs1) -> Adj ps1 ('AK ('L '::: ('R '::: qs1)))
data SAdj (p :: Path ABK i j) where
- SNil :: forall {i :: AB}. SAdj ('Nil :: Path ABK i i)
- SL :: forall {j :: AB} (ps :: Path ABK 'B j). IsLRPath ps => SAdj ('L '::: ps)
- SR :: forall {j :: AB} (ps :: Path ABK 'A j). IsLRPath ps => SAdj ('R '::: ps)
class ((ps +++ ('Nil :: Path ABK k k)) ~ ps, forall (i :: AB) (h :: AB) (qs :: Path ABK k h) (rs :: Path ABK h i). Assoc ps qs rs) => IsLRPath (ps :: Path ABK j k) where
- singPath :: SAdj ps
- withIsPath2 :: forall {k1 :: AB} (qs :: Path ABK k k1) r. IsLRPath qs => (IsLRPath (ps +++ qs) => r) -> r
type family RepLR (n :: Nat) :: Path ABK 'A 'A where ...
fromSimplex :: forall (a :: Nat) (b :: Nat). Simplex a b -> Adj ('AK (RepLR a)) ('AK (RepLR b))
type family CountLR (ps :: Path ABK 'A 'A) :: Nat where ...
type family CountLR' (ps :: Path ABK 'B 'A) :: Nat where ...
toSimplex :: forall (a :: Path ABK 'A 'A) (b :: Path ABK 'A 'A). Adj ('AK a) ('AK b) -> Simplex (CountLR a) (CountLR b)
type family RepRL (n :: Nat) :: Path ABK 'B 'B where ...
fromSimplexOp :: forall (b :: Nat) (a :: Nat). Simplex b a -> Adj ('AK (RepRL a)) ('AK (RepRL b))
type family CountRL (ps :: Path ABK 'B 'B) :: Nat where ...
type family CountRL' (ps :: Path ABK 'A 'B) :: Nat where ...
toSimplexOp :: forall (a :: Path ABK 'B 'B) (b :: Path ABK 'B 'B). Adj ('AK a) ('AK b) -> Simplex (CountRL b) (CountRL a)
data SNilOrL (p :: Path ABK i j) where
- SNilL :: forall {i :: AB}. SNilOrL ('Nil :: Path ABK i i)
- SLL :: SNilOrL ('L '::: ('Nil :: Path ABK 'B 'B))
data SNilOrR (p :: Path ABK i j) where
- SNilR :: forall {i :: AB}. SNilOrR ('Nil :: Path ABK i i)
- SRR :: SNilOrR ('R '::: ('Nil :: Path ABK 'A 'A))
class (IsLRPath ps, IsCotight (CotightAdj ps), Adjunction_ ('AK ps) ('AK (CotightAdj ps))) => IsTight (ps :: Path ABK i j) where
- type CotightAdj (ps :: Path ABK i j) :: Path ABK j i
- isNilOrL :: SNilOrL ps
class (IsLRPath ps, IsTight (TightAdj ps), Adjunction_ ('AK (TightAdj ps)) ('AK ps)) => IsCotight (ps :: Path ABK i j) where
- type TightAdj (ps :: Path ABK i j) :: Path ABK j i
- isNilOrR :: SNilOrR ps

Documentation

data AB Source Comments #

Constructors

A
B

Instances

Instances details

Bicategory ADJK Source Comments #

The walking adjunction

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Associated Types

type Ob0 ADJK (j :: k)
Instance details Defined in Proarrow.Category.Bicategory.Adj type Ob0 ADJK (j :: k) = ()
type I
Instance details Defined in Proarrow.Category.Bicategory.Adj type I = 'AK ('Nil :: Path ABK i i)
type O (ps :: ADJK i1 j) (qs :: ADJK i2 i1)
Instance details Defined in Proarrow.Category.Bicategory.Adj type O (ps :: ADJK i1 j) (qs :: ADJK i2 i1) = 'AK (UN ('AK :: Path ABK i2 i1 -> ADJK i2 i1) qs +++ UN ('AK :: Path ABK i1 j -> ADJK i1 j) ps)

Methods

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

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

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

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

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

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

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

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

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

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

Equipment ADJK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Methods

withCotightAdjoint :: forall {j :: AB} {k1 :: AB} (f :: ADJK j k1) r. IsTight f => ((Adjunction_ f (CotightAdjoint f), IsCotight (CotightAdjoint f)) => r) -> r Source Comments #

withTightAdjoint :: forall {j :: AB} {k1 :: AB} (f :: ADJK j k1) r. IsCotight f => ((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r) -> r Source Comments #

WithObO2 Cotight ADJK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Methods

withObO2 :: forall {i :: AB} {j :: AB} {k :: AB} (a :: ADJK j k) (b :: ADJK i j) r. (Ob a, Ob b, IsOb Cotight a, IsOb Cotight b) => ((IsOb Cotight (O a b), Ob (O a b)) => r) -> r Source Comments #

WithObO2 Tight ADJK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Methods

withObO2 :: forall {i :: AB} {j :: AB} {k :: AB} (a :: ADJK j k) (b :: ADJK i j) r. (Ob a, Ob b, IsOb Tight a, IsOb Tight b) => ((IsOb Tight (O a b), Ob (O a b)) => r) -> r Source Comments #

Adjunction_ ('AK ('L '::: ('R '::: ('L '::: ('Nil :: Path ABK 'B 'B))))) ('AK ('R '::: ('L '::: ('R '::: ('Nil :: Path ABK 'A 'A))))) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Methods

adj :: Adj ('AK ('L '::: ('R '::: ('L '::: ('Nil :: Path ABK 'B 'B))))) ('AK ('R '::: ('L '::: ('R '::: ('Nil :: Path ABK 'A 'A))))) Source Comments #

Adjunction_ ('AK ('L '::: ('Nil :: Path ABK 'B 'B))) ('AK ('R '::: ('Nil :: Path ABK 'A 'A))) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Methods

adj :: Adj ('AK ('L '::: ('Nil :: Path ABK 'B 'B))) ('AK ('R '::: ('Nil :: Path ABK 'A 'A))) Source Comments #

Adjunction_ ('AK ('Nil :: Path ABK c c) :: ADJK c c) ('AK ('Nil :: Path ABK c c) :: ADJK c c) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Methods

adj :: Adj ('AK ('Nil :: Path ABK c c)) ('AK ('Nil :: Path ABK c c)) Source Comments #

Comonad ('AK ('R '::: ('L '::: ('Nil :: Path ABK 'B 'B)))) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Methods

epsilon :: 'AK ('R '::: ('L '::: ('Nil :: Path ABK 'B 'B))) ~> (I :: ADJK 'B 'B) Source Comments #

delta :: 'AK ('R '::: ('L '::: ('Nil :: Path ABK 'B 'B))) ~> O ('AK ('R '::: ('L '::: ('Nil :: Path ABK 'B 'B)))) ('AK ('R '::: ('L '::: ('Nil :: Path ABK 'B 'B)))) Source Comments #

Monad ('AK ('L '::: ('R '::: ('Nil :: Path ABK 'A 'A)))) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Methods

eta :: (I :: ADJK 'A 'A) ~> 'AK ('L '::: ('R '::: ('Nil :: Path ABK 'A 'A))) Source Comments #

mu :: O ('AK ('L '::: ('R '::: ('Nil :: Path ABK 'A 'A)))) ('AK ('L '::: ('R '::: ('Nil :: Path ABK 'A 'A)))) ~> 'AK ('L '::: ('R '::: ('Nil :: Path ABK 'A 'A))) Source Comments #

IsCotight ('Nil :: Path ABK j j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Associated Types

type TightAdj ('Nil :: Path ABK j j)
Instance details Defined in Proarrow.Category.Bicategory.Adj type TightAdj ('Nil :: Path ABK j j) = 'Nil :: Path ABK j j

Methods

isNilOrR :: SNilOrR ('Nil :: Path ABK j j) Source Comments #

IsLRPath ('Nil :: Path ABK k k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Methods

singPath :: SAdj ('Nil :: Path ABK k k) Source Comments #

withIsPath2 :: forall {k1 :: AB} (qs :: Path ABK k k1) r. IsLRPath qs => (IsLRPath (('Nil :: Path ABK k k) +++ qs) => r) -> r Source Comments #

IsTight ('Nil :: Path ABK j j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Associated Types

type CotightAdj ('Nil :: Path ABK j j)
Instance details Defined in Proarrow.Category.Bicategory.Adj type CotightAdj ('Nil :: Path ABK j j) = 'Nil :: Path ABK j j

Methods

isNilOrL :: SNilOrL ('Nil :: Path ABK j j) Source Comments #

IsCotight ('R '::: ('Nil :: Path ABK 'A 'A)) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Associated Types

type TightAdj ('R '::: ('Nil :: Path ABK 'A 'A))
Instance details Defined in Proarrow.Category.Bicategory.Adj type TightAdj ('R '::: ('Nil :: Path ABK 'A 'A)) = 'L '::: ('Nil :: Path ABK 'B 'B)

Methods

isNilOrR :: SNilOrR ('R '::: ('Nil :: Path ABK 'A 'A)) Source Comments #

IsLRPath ps => IsLRPath ('L '::: ps :: Path ABK 'A k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Methods

singPath :: SAdj ('L '::: ps) Source Comments #

withIsPath2 :: forall {k1 :: AB} (qs :: Path ABK k k1) r. IsLRPath qs => (IsLRPath (('L '::: ps) +++ qs) => r) -> r Source Comments #

IsLRPath ps => IsLRPath ('R '::: ps :: Path ABK 'B k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Methods

singPath :: SAdj ('R '::: ps) Source Comments #

withIsPath2 :: forall {k1 :: AB} (qs :: Path ABK k k1) r. IsLRPath qs => (IsLRPath (('R '::: ps) +++ qs) => r) -> r Source Comments #

IsTight ('L '::: ('Nil :: Path ABK 'B 'B)) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Associated Types

type CotightAdj ('L '::: ('Nil :: Path ABK 'B 'B))
Instance details Defined in Proarrow.Category.Bicategory.Adj type CotightAdj ('L '::: ('Nil :: Path ABK 'B 'B)) = 'R '::: ('Nil :: Path ABK 'A 'A)

Methods

isNilOrL :: SNilOrL ('L '::: ('Nil :: Path ABK 'B 'B)) Source Comments #

type I Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

type I = 'AK ('Nil :: Path ABK i i)

type Ob0 ADJK (j :: k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

type Ob0 ADJK (j :: k) = ()

type O (ps :: ADJK i1 j) (qs :: ADJK i2 i1) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

type O (ps :: ADJK i1 j) (qs :: ADJK i2 i1) = 'AK (UN ('AK :: Path ABK i2 i1 -> ADJK i2 i1) qs +++ UN ('AK :: Path ABK i1 j -> ADJK i1 j) ps)

type IsOb Cotight ('AK ps :: ADJK i j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

type IsOb Cotight ('AK ps :: ADJK i j) = IsCotight ps

type IsOb Tight ('AK ps :: ADJK i j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

type IsOb Tight ('AK ps :: ADJK i j) = IsTight ps

type CotightAdjoint ('AK ps :: ADJK j i) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

type CotightAdjoint ('AK ps :: ADJK j i) = 'AK (CotightAdj ps)

type TightAdjoint ('AK ps :: ADJK j i) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

type TightAdjoint ('AK ps :: ADJK j i) = 'AK (TightAdj ps)

type CotightAdj ('Nil :: Path ABK j j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

type CotightAdj ('Nil :: Path ABK j j) = 'Nil :: Path ABK j j

type TightAdj ('Nil :: Path ABK j j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

type TightAdj ('Nil :: Path ABK j j) = 'Nil :: Path ABK j j

type CotightAdj ('L '::: ('Nil :: Path ABK 'B 'B)) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

type CotightAdj ('L '::: ('Nil :: Path ABK 'B 'B)) = 'R '::: ('Nil :: Path ABK 'A 'A)

type TightAdj ('R '::: ('Nil :: Path ABK 'A 'A)) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

type TightAdj ('R '::: ('Nil :: Path ABK 'A 'A)) = 'L '::: ('Nil :: Path ABK 'B 'B)

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

data ABK (a :: AB) (b :: AB) where Source Comments #

Constructors

L :: ABK 'A 'B
R :: ABK 'B 'A

Instances

Instances details

Adjunction_ ('AK ('L '::: ('R '::: ('L '::: ('Nil :: Path ABK 'B 'B))))) ('AK ('R '::: ('L '::: ('R '::: ('Nil :: Path ABK 'A 'A))))) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Methods

adj :: Adj ('AK ('L '::: ('R '::: ('L '::: ('Nil :: Path ABK 'B 'B))))) ('AK ('R '::: ('L '::: ('R '::: ('Nil :: Path ABK 'A 'A))))) Source Comments #

Adjunction_ ('AK ('L '::: ('Nil :: Path ABK 'B 'B))) ('AK ('R '::: ('Nil :: Path ABK 'A 'A))) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Methods

adj :: Adj ('AK ('L '::: ('Nil :: Path ABK 'B 'B))) ('AK ('R '::: ('Nil :: Path ABK 'A 'A))) Source Comments #

Adjunction_ ('AK ('Nil :: Path ABK c c) :: ADJK c c) ('AK ('Nil :: Path ABK c c) :: ADJK c c) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Methods

adj :: Adj ('AK ('Nil :: Path ABK c c)) ('AK ('Nil :: Path ABK c c)) Source Comments #

Comonad ('AK ('R '::: ('L '::: ('Nil :: Path ABK 'B 'B)))) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Methods

epsilon :: 'AK ('R '::: ('L '::: ('Nil :: Path ABK 'B 'B))) ~> (I :: ADJK 'B 'B) Source Comments #

delta :: 'AK ('R '::: ('L '::: ('Nil :: Path ABK 'B 'B))) ~> O ('AK ('R '::: ('L '::: ('Nil :: Path ABK 'B 'B)))) ('AK ('R '::: ('L '::: ('Nil :: Path ABK 'B 'B)))) Source Comments #

Monad ('AK ('L '::: ('R '::: ('Nil :: Path ABK 'A 'A)))) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Methods

eta :: (I :: ADJK 'A 'A) ~> 'AK ('L '::: ('R '::: ('Nil :: Path ABK 'A 'A))) Source Comments #

mu :: O ('AK ('L '::: ('R '::: ('Nil :: Path ABK 'A 'A)))) ('AK ('L '::: ('R '::: ('Nil :: Path ABK 'A 'A)))) ~> 'AK ('L '::: ('R '::: ('Nil :: Path ABK 'A 'A))) Source Comments #

IsCotight ('Nil :: Path ABK j j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Associated Types

type TightAdj ('Nil :: Path ABK j j)
Instance details Defined in Proarrow.Category.Bicategory.Adj type TightAdj ('Nil :: Path ABK j j) = 'Nil :: Path ABK j j

Methods

isNilOrR :: SNilOrR ('Nil :: Path ABK j j) Source Comments #

IsLRPath ('Nil :: Path ABK k k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Methods

singPath :: SAdj ('Nil :: Path ABK k k) Source Comments #

withIsPath2 :: forall {k1 :: AB} (qs :: Path ABK k k1) r. IsLRPath qs => (IsLRPath (('Nil :: Path ABK k k) +++ qs) => r) -> r Source Comments #

IsTight ('Nil :: Path ABK j j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Associated Types

type CotightAdj ('Nil :: Path ABK j j)
Instance details Defined in Proarrow.Category.Bicategory.Adj type CotightAdj ('Nil :: Path ABK j j) = 'Nil :: Path ABK j j

Methods

isNilOrL :: SNilOrL ('Nil :: Path ABK j j) Source Comments #

IsCotight ('R '::: ('Nil :: Path ABK 'A 'A)) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Associated Types

type TightAdj ('R '::: ('Nil :: Path ABK 'A 'A))
Instance details Defined in Proarrow.Category.Bicategory.Adj type TightAdj ('R '::: ('Nil :: Path ABK 'A 'A)) = 'L '::: ('Nil :: Path ABK 'B 'B)

Methods

isNilOrR :: SNilOrR ('R '::: ('Nil :: Path ABK 'A 'A)) Source Comments #

IsLRPath ps => IsLRPath ('L '::: ps :: Path ABK 'A k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Methods

singPath :: SAdj ('L '::: ps) Source Comments #

withIsPath2 :: forall {k1 :: AB} (qs :: Path ABK k k1) r. IsLRPath qs => (IsLRPath (('L '::: ps) +++ qs) => r) -> r Source Comments #

IsLRPath ps => IsLRPath ('R '::: ps :: Path ABK 'B k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Methods

singPath :: SAdj ('R '::: ps) Source Comments #

withIsPath2 :: forall {k1 :: AB} (qs :: Path ABK k k1) r. IsLRPath qs => (IsLRPath (('R '::: ps) +++ qs) => r) -> r Source Comments #

IsTight ('L '::: ('Nil :: Path ABK 'B 'B)) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Associated Types

type CotightAdj ('L '::: ('Nil :: Path ABK 'B 'B))
Instance details Defined in Proarrow.Category.Bicategory.Adj type CotightAdj ('L '::: ('Nil :: Path ABK 'B 'B)) = 'R '::: ('Nil :: Path ABK 'A 'A)

Methods

isNilOrL :: SNilOrL ('L '::: ('Nil :: Path ABK 'B 'B)) Source Comments #

type CotightAdj ('Nil :: Path ABK j j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

type CotightAdj ('Nil :: Path ABK j j) = 'Nil :: Path ABK j j

type TightAdj ('Nil :: Path ABK j j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

type TightAdj ('Nil :: Path ABK j j) = 'Nil :: Path ABK j j

type CotightAdj ('L '::: ('Nil :: Path ABK 'B 'B)) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

type CotightAdj ('L '::: ('Nil :: Path ABK 'B 'B)) = 'R '::: ('Nil :: Path ABK 'A 'A)

type TightAdj ('R '::: ('Nil :: Path ABK 'A 'A)) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

type TightAdj ('R '::: ('Nil :: Path ABK 'A 'A)) = 'L '::: ('Nil :: Path ABK 'B 'B)

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

data ADJK (i :: AB) (j :: AB) Source Comments #

Constructors

AK (Path ABK i j)

Instances

Instances details

Bicategory ADJK Source Comments #

The walking adjunction

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Associated Types

type Ob0 ADJK (j :: k)
Instance details Defined in Proarrow.Category.Bicategory.Adj type Ob0 ADJK (j :: k) = ()
type I
Instance details Defined in Proarrow.Category.Bicategory.Adj type I = 'AK ('Nil :: Path ABK i i)
type O (ps :: ADJK i1 j) (qs :: ADJK i2 i1)
Instance details Defined in Proarrow.Category.Bicategory.Adj type O (ps :: ADJK i1 j) (qs :: ADJK i2 i1) = 'AK (UN ('AK :: Path ABK i2 i1 -> ADJK i2 i1) qs +++ UN ('AK :: Path ABK i1 j -> ADJK i1 j) ps)

Methods

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

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

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

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

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

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

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

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

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

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

Equipment ADJK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Methods

withCotightAdjoint :: forall {j :: AB} {k1 :: AB} (f :: ADJK j k1) r. IsTight f => ((Adjunction_ f (CotightAdjoint f), IsCotight (CotightAdjoint f)) => r) -> r Source Comments #

withTightAdjoint :: forall {j :: AB} {k1 :: AB} (f :: ADJK j k1) r. IsCotight f => ((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r) -> r Source Comments #

WithObO2 Cotight ADJK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Methods

withObO2 :: forall {i :: AB} {j :: AB} {k :: AB} (a :: ADJK j k) (b :: ADJK i j) r. (Ob a, Ob b, IsOb Cotight a, IsOb Cotight b) => ((IsOb Cotight (O a b), Ob (O a b)) => r) -> r Source Comments #

WithObO2 Tight ADJK Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Methods

withObO2 :: forall {i :: AB} {j :: AB} {k :: AB} (a :: ADJK j k) (b :: ADJK i j) r. (Ob a, Ob b, IsOb Tight a, IsOb Tight b) => ((IsOb Tight (O a b), Ob (O a b)) => r) -> r Source Comments #

Adjunction_ ('AK ('L '::: ('R '::: ('L '::: ('Nil :: Path ABK 'B 'B))))) ('AK ('R '::: ('L '::: ('R '::: ('Nil :: Path ABK 'A 'A))))) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Methods

adj :: Adj ('AK ('L '::: ('R '::: ('L '::: ('Nil :: Path ABK 'B 'B))))) ('AK ('R '::: ('L '::: ('R '::: ('Nil :: Path ABK 'A 'A))))) Source Comments #

Adjunction_ ('AK ('L '::: ('Nil :: Path ABK 'B 'B))) ('AK ('R '::: ('Nil :: Path ABK 'A 'A))) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Methods

adj :: Adj ('AK ('L '::: ('Nil :: Path ABK 'B 'B))) ('AK ('R '::: ('Nil :: Path ABK 'A 'A))) Source Comments #

Adjunction_ ('AK ('Nil :: Path ABK c c) :: ADJK c c) ('AK ('Nil :: Path ABK c c) :: ADJK c c) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Methods

adj :: Adj ('AK ('Nil :: Path ABK c c)) ('AK ('Nil :: Path ABK c c)) Source Comments #

Comonad ('AK ('R '::: ('L '::: ('Nil :: Path ABK 'B 'B)))) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Methods

epsilon :: 'AK ('R '::: ('L '::: ('Nil :: Path ABK 'B 'B))) ~> (I :: ADJK 'B 'B) Source Comments #

delta :: 'AK ('R '::: ('L '::: ('Nil :: Path ABK 'B 'B))) ~> O ('AK ('R '::: ('L '::: ('Nil :: Path ABK 'B 'B)))) ('AK ('R '::: ('L '::: ('Nil :: Path ABK 'B 'B)))) Source Comments #

Monad ('AK ('L '::: ('R '::: ('Nil :: Path ABK 'A 'A)))) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Methods

eta :: (I :: ADJK 'A 'A) ~> 'AK ('L '::: ('R '::: ('Nil :: Path ABK 'A 'A))) Source Comments #

mu :: O ('AK ('L '::: ('R '::: ('Nil :: Path ABK 'A 'A)))) ('AK ('L '::: ('R '::: ('Nil :: Path ABK 'A 'A)))) ~> 'AK ('L '::: ('R '::: ('Nil :: Path ABK 'A 'A))) Source Comments #

CategoryOf (ADJK a b) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Bicategory.Adj type (~>) = Adj :: ADJK a b -> ADJK a b -> Type

Promonad (Adj :: ADJK a b -> ADJK a b -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Methods

id :: forall (a0 :: ADJK a b). Ob a0 => Adj a0 a0 Source Comments #

(.) :: forall (b0 :: ADJK a b) (c :: ADJK a b) (a0 :: ADJK a b). Adj b0 c -> Adj a0 b0 -> Adj a0 c Source Comments #

Profunctor (Adj :: ADJK a b -> ADJK a b -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Methods

dimap :: forall (c :: ADJK a b) (a0 :: ADJK a b) (b0 :: ADJK a b) (d :: ADJK a b). (c ~> a0) -> (b0 ~> d) -> Adj a0 b0 -> Adj c d Source Comments #

(\\) :: forall (a0 :: ADJK a b) (b0 :: ADJK a b) r. ((Ob a0, Ob b0) => r) -> Adj a0 b0 -> r Source Comments #

type I Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

type I = 'AK ('Nil :: Path ABK i i)

type Ob0 ADJK (j :: k) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

type Ob0 ADJK (j :: k) = ()

type O (ps :: ADJK i1 j) (qs :: ADJK i2 i1) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

type O (ps :: ADJK i1 j) (qs :: ADJK i2 i1) = 'AK (UN ('AK :: Path ABK i2 i1 -> ADJK i2 i1) qs +++ UN ('AK :: Path ABK i1 j -> ADJK i1 j) ps)

type IsOb Cotight ('AK ps :: ADJK i j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

type IsOb Cotight ('AK ps :: ADJK i j) = IsCotight ps

type IsOb Tight ('AK ps :: ADJK i j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

type IsOb Tight ('AK ps :: ADJK i j) = IsTight ps

type CotightAdjoint ('AK ps :: ADJK j i) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

type CotightAdjoint ('AK ps :: ADJK j i) = 'AK (CotightAdj ps)

type TightAdjoint ('AK ps :: ADJK j i) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

type TightAdjoint ('AK ps :: ADJK j i) = 'AK (TightAdj ps)

type (~>) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

type (~>) = Adj :: ADJK a b -> ADJK a b -> Type

type Ob (ps :: ADJK a b) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

type Ob (ps :: ADJK a b) = (Is ('AK :: Path ABK a b -> ADJK a b) ps, IsLRPath (UN ('AK :: Path ABK a b -> ADJK a b) ps))

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

data Adj (ps :: ADJK i j) (qs :: ADJK i j) where Source Comments #

Constructors

AdjNil :: forall {i :: AB}. Adj ('AK ('Nil :: Path ABK i i)) ('AK ('Nil :: Path ABK i i))
AdjR :: forall {j :: AB} (ps1 :: Path ABK 'A j) (qs1 :: Path ABK 'A j). Adj ('AK ps1) ('AK qs1) -> Adj ('AK ('R '::: ps1)) ('AK ('R '::: qs1))
AdjL :: forall {j :: AB} (ps1 :: Path ABK 'B j) (qs1 :: Path ABK 'B j). Adj ('AK ps1) ('AK qs1) -> Adj ('AK ('L '::: ps1)) ('AK ('L '::: qs1))
AdjCup :: forall {j :: AB} (ps1 :: Path ABK 'B j) (qs1 :: ADJK 'B j). Adj ('AK ps1) qs1 -> Adj ('AK ('R '::: ('L '::: ps1))) qs1
AdjCap :: forall {j :: AB} (ps1 :: ADJK 'A j) (qs1 :: Path ABK 'A j). Adj ps1 ('AK qs1) -> Adj ps1 ('AK ('L '::: ('R '::: qs1)))

Instances

Instances details

Promonad (Adj :: ADJK a b -> ADJK a b -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Adj Methods id :: forall (a0 :: ADJK a b). Ob a0 => Adj a0 a0 Source Comments # (.) :: forall (b0 :: ADJK a b) (c :: ADJK a b) (a0 :: ADJK a b). Adj b0 c -> Adj a0 b0 -> Adj a0 c Source Comments #
Profunctor (Adj :: ADJK a b -> ADJK a b -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Adj Methods dimap :: forall (c :: ADJK a b) (a0 :: ADJK a b) (b0 :: ADJK a b) (d :: ADJK a b). (c ~> a0) -> (b0 ~> d) -> Adj a0 b0 -> Adj c d Source Comments # (\\) :: forall (a0 :: ADJK a b) (b0 :: ADJK a b) r. ((Ob a0, Ob b0) => r) -> Adj a0 b0 -> r Source Comments #

data SAdj (p :: Path ABK i j) where Source Comments #

Constructors

SNil :: forall {i :: AB}. SAdj ('Nil :: Path ABK i i)
SL :: forall {j :: AB} (ps :: Path ABK 'B j). IsLRPath ps => SAdj ('L '::: ps)
SR :: forall {j :: AB} (ps :: Path ABK 'A j). IsLRPath ps => SAdj ('R '::: ps)

class ((ps +++ ('Nil :: Path ABK k k)) ~ ps, forall (i :: AB) (h :: AB) (qs :: Path ABK k h) (rs :: Path ABK h i). Assoc ps qs rs) => IsLRPath (ps :: Path ABK j k) where Source Comments #

Methods

singPath :: SAdj ps Source Comments #

withIsPath2 :: forall {k1 :: AB} (qs :: Path ABK k k1) r. IsLRPath qs => (IsLRPath (ps +++ qs) => r) -> r Source Comments #

Instances

Instances details

IsLRPath ('Nil :: Path ABK k k) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Adj Methods singPath :: SAdj ('Nil :: Path ABK k k) Source Comments # withIsPath2 :: forall {k1 :: AB} (qs :: Path ABK k k1) r. IsLRPath qs => (IsLRPath (('Nil :: Path ABK k k) +++ qs) => r) -> r Source Comments #
IsLRPath ps => IsLRPath ('L '::: ps :: Path ABK 'A k) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Adj Methods singPath :: SAdj ('L '::: ps) Source Comments # withIsPath2 :: forall {k1 :: AB} (qs :: Path ABK k k1) r. IsLRPath qs => (IsLRPath (('L '::: ps) +++ qs) => r) -> r Source Comments #
IsLRPath ps => IsLRPath ('R '::: ps :: Path ABK 'B k) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Adj Methods singPath :: SAdj ('R '::: ps) Source Comments # withIsPath2 :: forall {k1 :: AB} (qs :: Path ABK k k1) r. IsLRPath qs => (IsLRPath (('R '::: ps) +++ qs) => r) -> r Source Comments #

type family RepLR (n :: Nat) :: Path ABK 'A 'A where ... Source Comments #

Equations

RepLR 'Z = 'Nil :: Path ABK 'A 'A
RepLR ('S n) = 'L '::: ('R '::: RepLR n)

fromSimplex :: forall (a :: Nat) (b :: Nat). Simplex a b -> Adj ('AK (RepLR a)) ('AK (RepLR b)) Source Comments #

Adj(A, A) is the walking monoid

type family CountLR (ps :: Path ABK 'A 'A) :: Nat where ... Source Comments #

Equations

CountLR ('Nil :: Path ABK 'A 'A) = 'Z
CountLR ('L '::: ps) = 'S (CountLR' ps)

type family CountLR' (ps :: Path ABK 'B 'A) :: Nat where ... Source Comments #

Equations

CountLR' ('R '::: n) = CountLR n

toSimplex :: forall (a :: Path ABK 'A 'A) (b :: Path ABK 'A 'A). Adj ('AK a) ('AK b) -> Simplex (CountLR a) (CountLR b) Source Comments #

type family RepRL (n :: Nat) :: Path ABK 'B 'B where ... Source Comments #

Equations

RepRL 'Z = 'Nil :: Path ABK 'B 'B
RepRL ('S n) = 'R '::: ('L '::: RepRL n)

fromSimplexOp :: forall (b :: Nat) (a :: Nat). Simplex b a -> Adj ('AK (RepRL a)) ('AK (RepRL b)) Source Comments #

Adj(B, B) is the walking comonoid

type family CountRL (ps :: Path ABK 'B 'B) :: Nat where ... Source Comments #

Equations

CountRL ('Nil :: Path ABK 'B 'B) = 'Z
CountRL ('R '::: ps) = 'S (CountRL' ps)

type family CountRL' (ps :: Path ABK 'A 'B) :: Nat where ... Source Comments #

Equations

CountRL' ('L '::: n) = CountRL n

toSimplexOp :: forall (a :: Path ABK 'B 'B) (b :: Path ABK 'B 'B). Adj ('AK a) ('AK b) -> Simplex (CountRL b) (CountRL a) Source Comments #

data SNilOrL (p :: Path ABK i j) where Source Comments #

Constructors

SNilL :: forall {i :: AB}. SNilOrL ('Nil :: Path ABK i i)
SLL :: SNilOrL ('L '::: ('Nil :: Path ABK 'B 'B))

data SNilOrR (p :: Path ABK i j) where Source Comments #

Constructors

SNilR :: forall {i :: AB}. SNilOrR ('Nil :: Path ABK i i)
SRR :: SNilOrR ('R '::: ('Nil :: Path ABK 'A 'A))

class (IsLRPath ps, IsCotight (CotightAdj ps), Adjunction_ ('AK ps) ('AK (CotightAdj ps))) => IsTight (ps :: Path ABK i j) where Source Comments #

Associated Types

type CotightAdj (ps :: Path ABK i j) :: Path ABK j i Source Comments #

Methods

isNilOrL :: SNilOrL ps Source Comments #

Instances

Instances details

IsTight ('Nil :: Path ABK j j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Associated Types

type CotightAdj ('Nil :: Path ABK j j)
Instance details Defined in Proarrow.Category.Bicategory.Adj type CotightAdj ('Nil :: Path ABK j j) = 'Nil :: Path ABK j j

Methods

isNilOrL :: SNilOrL ('Nil :: Path ABK j j) Source Comments #

IsTight ('L '::: ('Nil :: Path ABK 'B 'B)) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Associated Types

type CotightAdj ('L '::: ('Nil :: Path ABK 'B 'B))
Instance details Defined in Proarrow.Category.Bicategory.Adj type CotightAdj ('L '::: ('Nil :: Path ABK 'B 'B)) = 'R '::: ('Nil :: Path ABK 'A 'A)

Methods

isNilOrL :: SNilOrL ('L '::: ('Nil :: Path ABK 'B 'B)) Source Comments #

class (IsLRPath ps, IsTight (TightAdj ps), Adjunction_ ('AK (TightAdj ps)) ('AK ps)) => IsCotight (ps :: Path ABK i j) where Source Comments #

Associated Types

type TightAdj (ps :: Path ABK i j) :: Path ABK j i Source Comments #

Methods

isNilOrR :: SNilOrR ps Source Comments #

Instances

Instances details

IsCotight ('Nil :: Path ABK j j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Associated Types

type TightAdj ('Nil :: Path ABK j j)
Instance details Defined in Proarrow.Category.Bicategory.Adj type TightAdj ('Nil :: Path ABK j j) = 'Nil :: Path ABK j j

Methods

isNilOrR :: SNilOrR ('Nil :: Path ABK j j) Source Comments #

IsCotight ('R '::: ('Nil :: Path ABK 'A 'A)) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Adj

Associated Types

type TightAdj ('R '::: ('Nil :: Path ABK 'A 'A))
Instance details Defined in Proarrow.Category.Bicategory.Adj type TightAdj ('R '::: ('Nil :: Path ABK 'A 'A)) = 'L '::: ('Nil :: Path ABK 'B 'B)

Methods

isNilOrR :: SNilOrR ('R '::: ('Nil :: Path ABK 'A 'A)) Source Comments #