| Safe Haskell | None |
|---|---|
| Language | GHC2024 |
Proarrow.Squares.Limit
Synopsis
- limit :: forall {k1} {kk :: k1 -> k1 -> Type} {a :: k1} {i :: k1} {k2 :: k1} (j :: kk i a) (d :: kk i k2). (HasLimits j k2, IsTight d) => Sq (j '::: (Limit j d '::: ('Nil :: Path kk k2 k2))) (d '::: ('Nil :: Path kk k2 k2)) ('Nil :: Path kk k2 k2) ('Nil :: Path kk i i)
- limitUniv :: forall {k1} {kk :: k1 -> k1 -> Type} {a :: k1} {i :: k1} {k2 :: k1} (j :: kk i a) (d :: kk i k2) (p :: kk a k2). (HasLimits j k2, IsTight d, Ob p) => Sq (j '::: (p '::: ('Nil :: Path kk k2 k2))) (d '::: ('Nil :: Path kk k2 k2)) ('Nil :: Path kk k2 k2) ('Nil :: Path kk i i) -> Sq (p '::: ('Nil :: Path kk k2 k2)) (Limit j d '::: ('Nil :: Path kk k2 k2)) ('Nil :: Path kk k2 k2) ('Nil :: Path kk a a)
- limitUniv' :: forall {k1} {kk :: k1 -> k1 -> Type} {a :: k1} {i :: k1} {k2 :: k1} (j :: kk i a) (d :: kk i k2) (p :: kk a k2). (HasLimits j k2, IsTight d, IsTight p) => Sq (j '::: ('Nil :: Path kk a a)) ('Nil :: Path kk k2 k2) (p '::: ('Nil :: Path kk k2 k2)) (d '::: ('Nil :: Path kk k2 k2)) -> Sq ('Nil :: Path kk a a) ('Nil :: Path kk k2 k2) (p '::: ('Nil :: Path kk k2 k2)) (Limit j d '::: ('Nil :: Path kk k2 k2))
- rightAdjointPreservesLimits :: forall {k1} {kk :: k1 -> k1 -> Type} {k2 :: k1} {k' :: k1} {i :: k1} {a :: k1} (f :: kk k' k2) (g :: kk k2 k') (d :: kk i k2) (j :: kk i a). (Adjunction f g, Equipment kk, IsTight d, IsTight f, IsTight g, HasLimits j k2, HasLimits j k') => Sq (Limit j (O g d) '::: ('Nil :: Path kk k' k')) (Limit j d '::: (g '::: ('Nil :: Path kk k' k'))) ('Nil :: Path kk k' k') ('Nil :: Path kk a a)
- rightAdjointPreservesLimitsInv :: forall {k1} {kk :: k1 -> k1 -> Type} {k2 :: k1} {k' :: k1} {i :: k1} {a :: k1} (f :: kk k' k2) (g :: kk k2 k') (d :: kk i k2) (j :: kk i a). (Adjunction f g, Equipment kk, IsTight d, IsTight f, IsTight g, HasLimits j k2, HasLimits j k') => Sq (Limit j d '::: (g '::: ('Nil :: Path kk k' k'))) (Limit j (O g d) '::: ('Nil :: Path kk k' k')) ('Nil :: Path kk k' k') ('Nil :: Path kk a a)
- colimit :: forall {k1} {kk :: k1 -> k1 -> Type} {a :: k1} {i :: k1} {k2 :: k1} (j :: kk a i) (d :: kk k2 i). (HasColimits j k2, IsCotight d) => Sq (Colimit j d '::: (j '::: ('Nil :: Path kk i i))) (d '::: ('Nil :: Path kk i i)) ('Nil :: Path kk i i) ('Nil :: Path kk k2 k2)
- colimitUniv :: forall {k1} {kk :: k1 -> k1 -> Type} {a :: k1} {i :: k1} {k2 :: k1} (j :: kk a i) (d :: kk k2 i) (p :: kk k2 a). (HasColimits j k2, IsCotight d, Ob p) => Sq (p '::: (j '::: ('Nil :: Path kk i i))) (d '::: ('Nil :: Path kk i i)) ('Nil :: Path kk i i) ('Nil :: Path kk k2 k2) -> Sq (p '::: ('Nil :: Path kk a a)) (Colimit j d '::: ('Nil :: Path kk a a)) ('Nil :: Path kk a a) ('Nil :: Path kk k2 k2)
- unit :: forall {k1} {kk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1} (f :: kk j k2) (g :: kk k2 j). (Adjunction f g, Equipment kk) => Sq ('Nil :: Path kk j j) (f '::: (g '::: ('Nil :: Path kk j j))) ('Nil :: Path kk j j) ('Nil :: Path kk j j)
- counit :: forall {k1} {kk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1} (f :: kk j k2) (g :: kk k2 j). (Adjunction f g, Equipment kk) => Sq (g '::: (f '::: ('Nil :: Path kk k2 k2))) ('Nil :: Path kk k2 k2) ('Nil :: Path kk k2 k2) ('Nil :: Path kk k2 k2)
Documentation
limit :: forall {k1} {kk :: k1 -> k1 -> Type} {a :: k1} {i :: k1} {k2 :: k1} (j :: kk i a) (d :: kk i k2). (HasLimits j k2, IsTight d) => Sq (j '::: (Limit j d '::: ('Nil :: Path kk k2 k2))) (d '::: ('Nil :: Path kk k2 k2)) ('Nil :: Path kk k2 k2) ('Nil :: Path kk i i) Source Comments #
The projection out of the j-weighted limit l of d.
K-----K l>\ | | @->d j-/ | I-----I
limitUniv :: forall {k1} {kk :: k1 -> k1 -> Type} {a :: k1} {i :: k1} {k2 :: k1} (j :: kk i a) (d :: kk i k2) (p :: kk a k2). (HasLimits j k2, IsTight d, Ob p) => Sq (j '::: (p '::: ('Nil :: Path kk k2 k2))) (d '::: ('Nil :: Path kk k2 k2)) ('Nil :: Path kk k2 k2) ('Nil :: Path kk i i) -> Sq (p '::: ('Nil :: Path kk k2 k2)) (Limit j d '::: ('Nil :: Path kk k2 k2)) ('Nil :: Path kk k2 k2) ('Nil :: Path kk a a) Source Comments #
The universal property of the limit.
The dotted inner square is the input square, the outer square is the output square.
A---------K | K.....K | p---\ : | | : @->d l | j-/ : | | I.....I | A---------A
limitUniv' :: forall {k1} {kk :: k1 -> k1 -> Type} {a :: k1} {i :: k1} {k2 :: k1} (j :: kk i a) (d :: kk i k2) (p :: kk a k2). (HasLimits j k2, IsTight d, IsTight p) => Sq (j '::: ('Nil :: Path kk a a)) ('Nil :: Path kk k2 k2) (p '::: ('Nil :: Path kk k2 k2)) (d '::: ('Nil :: Path kk k2 k2)) -> Sq ('Nil :: Path kk a a) ('Nil :: Path kk k2 k2) (p '::: ('Nil :: Path kk k2 k2)) (Limit j d '::: ('Nil :: Path kk k2 k2)) Source Comments #
A-+--p--+-K | : v : | | j--@ : | | : v : | | I..d..K | A----l----K
rightAdjointPreservesLimits :: forall {k1} {kk :: k1 -> k1 -> Type} {k2 :: k1} {k' :: k1} {i :: k1} {a :: k1} (f :: kk k' k2) (g :: kk k2 k') (d :: kk i k2) (j :: kk i a). (Adjunction f g, Equipment kk, IsTight d, IsTight f, IsTight g, HasLimits j k2, HasLimits j k') => Sq (Limit j (O g d) '::: ('Nil :: Path kk k' k')) (Limit j d '::: (g '::: ('Nil :: Path kk k' k'))) ('Nil :: Path kk k' k') ('Nil :: Path kk a a) 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} {kk :: k1 -> k1 -> Type} {k2 :: k1} {k' :: k1} {i :: k1} {a :: k1} (f :: kk k' k2) (g :: kk k2 k') (d :: kk i k2) (j :: kk i a). (Adjunction f g, Equipment kk, IsTight d, IsTight f, IsTight g, HasLimits j k2, HasLimits j k') => Sq (Limit j d '::: (g '::: ('Nil :: Path kk k' k'))) (Limit j (O g d) '::: ('Nil :: Path kk k' k')) ('Nil :: Path kk k' k') ('Nil :: Path kk a a) 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} {kk :: k1 -> k1 -> Type} {a :: k1} {i :: k1} {k2 :: k1} (j :: kk a i) (d :: kk k2 i). (HasColimits j k2, IsCotight d) => Sq (Colimit j d '::: (j '::: ('Nil :: Path kk i i))) (d '::: ('Nil :: Path kk i i)) ('Nil :: Path kk i i) ('Nil :: Path kk k2 k2) Source Comments #
The projection into the j-weighted colimit c of d.
I-----I j-\ | | @-<d c</ | K-----K
colimitUniv :: forall {k1} {kk :: k1 -> k1 -> Type} {a :: k1} {i :: k1} {k2 :: k1} (j :: kk a i) (d :: kk k2 i) (p :: kk k2 a). (HasColimits j k2, IsCotight d, Ob p) => Sq (p '::: (j '::: ('Nil :: Path kk i i))) (d '::: ('Nil :: Path kk i i)) ('Nil :: Path kk i i) ('Nil :: Path kk k2 k2) -> Sq (p '::: ('Nil :: Path kk a a)) (Colimit j d '::: ('Nil :: Path kk a a)) ('Nil :: Path kk a a) ('Nil :: Path kk 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---------A | I.....I | | j-\ : | | : @-<d c p---/ : | | K.....K | K---------K