| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Proarrow.Squares.Limit
Synopsis
- limit :: forall {k1} {hk :: k1 -> k1 -> Type} {vk :: k1 -> k1 -> Type} {a :: k1} {i :: k1} {k2 :: k1} (j :: hk i a) (d :: vk i k2). (Ob0 vk i, HasLimits vk j k2, Ob d) => Sq '(j '::: ('Nil :: Path hk a a), Limit j d '::: ('Nil :: Path vk k2 k2)) '('Nil :: Path hk k2 k2, d '::: ('Nil :: Path vk k2 k2))
- limitUniv :: forall {k1} {hk :: k1 -> k1 -> Type} {vk :: k1 -> k1 -> Type} {a :: k1} {i :: k1} {k2 :: k1} (j :: hk i a) (d :: vk i k2) (p :: vk a k2). (Ob0 vk i, HasLimits vk j k2, Ob d, Ob p) => Sq '(j '::: ('Nil :: Path hk a a), p '::: ('Nil :: Path vk k2 k2)) '('Nil :: Path hk k2 k2, d '::: ('Nil :: Path vk k2 k2)) -> Sq '('Nil :: Path hk a a, p '::: ('Nil :: Path vk k2 k2)) '('Nil :: Path hk k2 k2, Limit j d '::: ('Nil :: Path vk k2 k2))
- rightAdjointPreservesLimits :: forall {k1} {hk :: k1 -> k1 -> Type} {vk :: k1 -> k1 -> Type} {k2 :: k1} {k' :: k1} {i :: k1} {a :: k1} (f :: vk k' k2) (g :: vk k2 k') (d :: vk i k2) (j :: hk i a). (Adjunction f g, HasCompanions hk vk, Ob d, Ob f, Ob g, HasLimits vk j k2, HasLimits vk j k', Ob0 vk i, Ob0 vk k2, Ob0 vk k', Ob0 vk a) => Sq '('Nil :: Path hk a a, Limit j (O g d) '::: ('Nil :: Path vk k' k')) '('Nil :: Path hk k' k', Limit j d '::: (g '::: ('Nil :: Path vk k' k')))
- rightAdjointPreservesLimitsInv :: forall {k1} {hk :: k1 -> k1 -> Type} {vk :: k1 -> k1 -> Type} {k2 :: k1} {k' :: k1} {i :: k1} {a :: k1} (g :: vk k2 k') (d :: vk i k2) (j :: hk i a). (HasCompanions hk vk, Ob d, Ob g, HasLimits vk j k2, HasLimits vk j k', Ob0 vk i, Ob0 vk k2, Ob0 vk k', Ob0 vk a) => Sq '('Nil :: Path hk a a, Limit j d '::: (g '::: ('Nil :: Path vk k' k'))) '('Nil :: Path hk k' k', Limit j (O g d) '::: ('Nil :: Path vk k' k'))
- colimit :: forall {k1} {hk :: k1 -> k1 -> Type} {vk :: k1 -> k1 -> Type} {a :: k1} {i :: k1} {k2 :: k1} (j :: hk a i) (d :: vk i k2). (Ob0 vk i, HasColimits vk j k2, Ob d) => Sq '(j '::: ('Nil :: Path hk i i), d '::: ('Nil :: Path vk k2 k2)) '('Nil :: Path hk k2 k2, Colimit j d '::: ('Nil :: Path vk k2 k2))
- colimitUniv :: forall {k1} {hk :: k1 -> k1 -> Type} {vk :: k1 -> k1 -> Type} {a :: k1} {i :: k1} {k2 :: k1} (j :: hk a i) (d :: vk i k2) (p :: vk a k2). (Ob0 vk i, HasColimits vk j k2, Ob d, Ob p) => Sq '(j '::: ('Nil :: Path hk i i), d '::: ('Nil :: Path vk k2 k2)) '('Nil :: Path hk k2 k2, p '::: ('Nil :: Path vk k2 k2)) -> Sq '('Nil :: Path hk a a, Colimit j d '::: ('Nil :: Path vk k2 k2)) '('Nil :: Path hk k2 k2, p '::: ('Nil :: Path vk k2 k2))
- leftAdjointPreservesColimits :: forall {k1} {hk :: k1 -> k1 -> Type} {vk :: k1 -> k1 -> Type} {k2 :: k1} {k' :: k1} {i :: k1} {a :: k1} (f :: vk k2 k') (g :: vk k' k2) (d :: vk i k2) (j :: hk a i). (Adjunction f g, HasCompanions hk vk, Ob d, Ob f, Ob g, HasColimits vk j k2, HasColimits vk j k', Ob0 vk i, Ob0 vk k2, Ob0 vk k', Ob0 vk a) => Sq '('Nil :: Path hk a a, Colimit j d '::: (f '::: ('Nil :: Path vk k' k'))) '('Nil :: Path hk k' k', Colimit j (O f d) '::: ('Nil :: Path vk k' k'))
- leftAdjointPreservesColimitsInv :: forall {k1} {hk :: k1 -> k1 -> Type} {vk :: k1 -> k1 -> Type} {k2 :: k1} {k' :: k1} {i :: k1} {a :: k1} (f :: vk k2 k') (d :: vk i k2) (j :: hk a i). (HasCompanions hk vk, Ob d, Ob f, HasColimits vk j k2, HasColimits vk j k', Ob0 vk i, Ob0 vk k2, Ob0 vk k', Ob0 vk a) => Sq '('Nil :: Path hk a a, Colimit j (O f d) '::: ('Nil :: Path vk k' k')) '('Nil :: Path hk k' k', Colimit j d '::: (f '::: ('Nil :: Path vk k' k')))
- unit :: forall {k1} {hk :: CAT k1} {vk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1} (f :: vk j k2) (g :: vk k2 j). (Adjunction f g, HasCompanions hk vk, Ob f, Ob g, Ob0 vk j, Ob0 vk k2) => Sq '('Nil :: Path hk j j, 'Nil :: Path vk j j) '('Nil :: Path hk j j, f '::: (g '::: ('Nil :: Path vk j j)))
- counit :: forall {k1} {hk :: CAT k1} {vk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1} (f :: vk j k2) (g :: vk k2 j). (Adjunction f g, HasCompanions hk vk, Ob f, Ob g, Ob0 vk j, Ob0 vk k2) => Sq '('Nil :: Path hk k2 k2, g '::: (f '::: ('Nil :: Path vk k2 k2))) '('Nil :: Path hk k2 k2, 'Nil :: Path vk k2 k2)
Documentation
limit :: forall {k1} {hk :: k1 -> k1 -> Type} {vk :: k1 -> k1 -> Type} {a :: k1} {i :: k1} {k2 :: k1} (j :: hk i a) (d :: vk i k2). (Ob0 vk i, HasLimits vk j k2, Ob d) => Sq '(j '::: ('Nil :: Path hk a a), Limit j d '::: ('Nil :: Path vk k2 k2)) '('Nil :: Path hk k2 k2, d '::: ('Nil :: Path vk k2 k2)) Source Comments #
The projection out of the j-weighted limit l of d.
A--l--K | v | j--@ | | v | I--d--K
limitUniv :: forall {k1} {hk :: k1 -> k1 -> Type} {vk :: k1 -> k1 -> Type} {a :: k1} {i :: k1} {k2 :: k1} (j :: hk i a) (d :: vk i k2) (p :: vk a k2). (Ob0 vk i, HasLimits vk j k2, Ob d, Ob p) => Sq '(j '::: ('Nil :: Path hk a a), p '::: ('Nil :: Path vk k2 k2)) '('Nil :: Path hk k2 k2, d '::: ('Nil :: Path vk k2 k2)) -> Sq '('Nil :: Path hk a a, p '::: ('Nil :: Path vk k2 k2)) '('Nil :: Path hk k2 k2, Limit j d '::: ('Nil :: Path vk k2 k2)) Source Comments #
The universal property of the limit.
The dotted inner square is the input square, the outer square is the output square.
A-+--p--+-K | : v : | | j--@ : | | : v : | | I..d..K | A----l----K
rightAdjointPreservesLimits :: forall {k1} {hk :: k1 -> k1 -> Type} {vk :: k1 -> k1 -> Type} {k2 :: k1} {k' :: k1} {i :: k1} {a :: k1} (f :: vk k' k2) (g :: vk k2 k') (d :: vk i k2) (j :: hk i a). (Adjunction f g, HasCompanions hk vk, Ob d, Ob f, Ob g, HasLimits vk j k2, HasLimits vk j k', Ob0 vk i, Ob0 vk k2, Ob0 vk k', Ob0 vk a) => Sq '('Nil :: Path hk a a, Limit j (O g d) '::: ('Nil :: Path vk k' k')) '('Nil :: Path hk k' k', Limit j d '::: (g '::: ('Nil :: Path vk k' k'))) Source Comments #
Preservation of limits by right adjoints
Let l be the j-weighted limit of d and l' be the j-weighted limit of g ∘ d.
Then we provide the following square:
A--l'-K' | v | | @ | | / \ | | v v | A-l-g-K'
With this implementation:
+-----l'--+---------+ | v | /@\ | | | | v v | +-+---l'--+-f-+-+-g-+ | : v | v : | v | | j---@ | | : | | | | : / \ | | : | | | | : v v | v : | | | | +-d-+-g-+-f-+ | | | | : | | v v : | | | | : v | \@/ : | | | | +.d.+.......+ | v | +-------l-------+-g-+
rightAdjointPreservesLimitsInv :: forall {k1} {hk :: k1 -> k1 -> Type} {vk :: k1 -> k1 -> Type} {k2 :: k1} {k' :: k1} {i :: k1} {a :: k1} (g :: vk k2 k') (d :: vk i k2) (j :: hk i a). (HasCompanions hk vk, Ob d, Ob g, HasLimits vk j k2, HasLimits vk j k', Ob0 vk i, Ob0 vk k2, Ob0 vk k', Ob0 vk a) => Sq '('Nil :: Path hk a a, Limit j d '::: (g '::: ('Nil :: Path vk k' k'))) '('Nil :: Path hk k' k', Limit j (O g d) '::: ('Nil :: Path vk k' k')) Source Comments #
The inverse works for any arrow:
The required square
A-l-g-K' | v v | | \@/ | | | | A--l'-K'
is implemented as
A-+-l-+-g-+-K' | : v | v : | | j-@ | | : | | : v | v : | | +.d.+.g.+ | A-----l'----K'
colimit :: forall {k1} {hk :: k1 -> k1 -> Type} {vk :: k1 -> k1 -> Type} {a :: k1} {i :: k1} {k2 :: k1} (j :: hk a i) (d :: vk i k2). (Ob0 vk i, HasColimits vk j k2, Ob d) => Sq '(j '::: ('Nil :: Path hk i i), d '::: ('Nil :: Path vk k2 k2)) '('Nil :: Path hk k2 k2, Colimit j d '::: ('Nil :: Path vk k2 k2)) Source Comments #
The projection into the j-weighted colimit c of d.
I--d--K | v | j--@ | | v | A--l--K
colimitUniv :: forall {k1} {hk :: k1 -> k1 -> Type} {vk :: k1 -> k1 -> Type} {a :: k1} {i :: k1} {k2 :: k1} (j :: hk a i) (d :: vk i k2) (p :: vk a k2). (Ob0 vk i, HasColimits vk j k2, Ob d, Ob p) => Sq '(j '::: ('Nil :: Path hk i i), d '::: ('Nil :: Path vk k2 k2)) '('Nil :: Path hk k2 k2, p '::: ('Nil :: Path vk k2 k2)) -> Sq '('Nil :: Path hk a a, Colimit j d '::: ('Nil :: Path vk k2 k2)) '('Nil :: Path hk k2 k2, p '::: ('Nil :: Path vk k2 k2)) Source Comments #
The universal property of the colimit.
The dotted inner square is the input square, the outer square is the output square.
A----c----K | I..d..K | | : v : | | j--@ : | | : v : | A-+--p--+-K
leftAdjointPreservesColimits :: forall {k1} {hk :: k1 -> k1 -> Type} {vk :: k1 -> k1 -> Type} {k2 :: k1} {k' :: k1} {i :: k1} {a :: k1} (f :: vk k2 k') (g :: vk k' k2) (d :: vk i k2) (j :: hk a i). (Adjunction f g, HasCompanions hk vk, Ob d, Ob f, Ob g, HasColimits vk j k2, HasColimits vk j k', Ob0 vk i, Ob0 vk k2, Ob0 vk k', Ob0 vk a) => Sq '('Nil :: Path hk a a, Colimit j d '::: (f '::: ('Nil :: Path vk k' k'))) '('Nil :: Path hk k' k', Colimit j (O f d) '::: ('Nil :: Path vk k' k')) Source Comments #
Preservation of colimits by left adjoints
Let c be the j-weighted colimit of d and c' be the j-weighted colimit of g ∘ d.
Then we provide the following square:
A-c-f-K' | v v | | \ / | | @ | | v | A--c'-K'
With this implementation:
+-------c-------+-f-+ | +.d.+.......+ | v | | : v | /@\ : | | | | : | | v v : | | | | +-d-+-f-+-g-+ | | | | : v v | v : | | | | : \ / | | : | | | | j---@ | | : | | | | : v | v : | v | +-+---c'--+-g-+-+-f-+ | | | v v | | v | \@/ | +-----c'--+---------+
leftAdjointPreservesColimitsInv :: forall {k1} {hk :: k1 -> k1 -> Type} {vk :: k1 -> k1 -> Type} {k2 :: k1} {k' :: k1} {i :: k1} {a :: k1} (f :: vk k2 k') (d :: vk i k2) (j :: hk a i). (HasCompanions hk vk, Ob d, Ob f, HasColimits vk j k2, HasColimits vk j k', Ob0 vk i, Ob0 vk k2, Ob0 vk k', Ob0 vk a) => Sq '('Nil :: Path hk a a, Colimit j (O f d) '::: ('Nil :: Path vk k' k')) '('Nil :: Path hk k' k', Colimit j d '::: (f '::: ('Nil :: Path vk k' k'))) Source Comments #
The inverse works for any arrow:
The required square
A--c'-K' | | | | /@\ | | v v | A-c-g-K'
is implemented as
A-----c'----K' | +.d.+.f.+ | | : v | v : | | j-@ | | : | | : v | v : | A-+-c-+-f-+-K'
unit :: forall {k1} {hk :: CAT k1} {vk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1} (f :: vk j k2) (g :: vk k2 j). (Adjunction f g, HasCompanions hk vk, Ob f, Ob g, Ob0 vk j, Ob0 vk k2) => Sq '('Nil :: Path hk j j, 'Nil :: Path vk j j) '('Nil :: Path hk j j, f '::: (g '::: ('Nil :: Path vk j j))) Source Comments #
counit :: forall {k1} {hk :: CAT k1} {vk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1} (f :: vk j k2) (g :: vk k2 j). (Adjunction f g, HasCompanions hk vk, Ob f, Ob g, Ob0 vk j, Ob0 vk k2) => Sq '('Nil :: Path hk k2 k2, g '::: (f '::: ('Nil :: Path vk k2 k2))) '('Nil :: Path hk k2 k2, 'Nil :: Path vk k2 k2) Source Comments #