{-# OPTIONS --without-K --safe #-}
module Categories.Functor.Limits where

open import Level

open import Categories.Category
open import Categories.Functor
open import Categories.Functor.Properties
open import Categories.Object.Terminal
open import Categories.Object.Initial

open import Categories.Diagram.Limit
open import Categories.Diagram.Colimit
open import Categories.Diagram.Cone.Properties
open import Categories.Diagram.Cocone.Properties

open import Categories.Category.Construction.Cones
open import Categories.Category.Construction.Cocones

private
  variable
    o β„“ e : Level
    π’ž π’Ÿ ℐ : Category o β„“ e

module _ (F : Functor π’ž π’Ÿ) {J : Functor ℐ π’ž} where

  PreservesLimit : (L : Limit J) β†’ Set _
  PreservesLimit L = IsTerminal (Cones (F ∘F J)) (F-map-Coneˑ F limit)
    where open Limit L

  PreservesColimit : (L : Colimit J) β†’ Set _
  PreservesColimit L = IsInitial (Cocones (F ∘F J)) (F-map-Coconeˑ F colimit)
    where open Colimit L

  ReflectsLimits : Set _
  ReflectsLimits = βˆ€ (K : Cone J) β†’ IsTerminal (Cones (F ∘F J)) (F-map-ConeΛ‘ F K) β†’ IsTerminal (Cones J) K

  ReflectsColimits : Set _
  ReflectsColimits = βˆ€ (K : Cocone J) β†’ IsInitial (Cocones (F ∘F J)) (F-map-CoconeΛ‘ F K) β†’ IsInitial (Cocones J) K

--   record CreatesLimits : Set (o βŠ” β„“ βŠ” e βŠ” oβ€² βŠ” β„“β€² βŠ” eβ€² βŠ” oβ€³ βŠ” β„“β€³) where
--     field
--       preserves-limits : PreservesLimit
--       reflects-limits  : ReflectsLimits

--   record CreatesColimits : Set (o βŠ” β„“ βŠ” e βŠ” oβ€² βŠ” β„“β€² βŠ” eβ€² βŠ” oβ€³ βŠ” β„“β€³) where
--     field
--       preserves-colimits : PreservesColimit
--       reflects-colimits  : ReflectsColimits

Continuous : βˆ€ o β„“ e β†’ (F : Functor π’ž π’Ÿ) β†’ Set _
Continuous {π’ž = π’ž} o β„“ e F = βˆ€ {π’₯ : Category o β„“ e} {J : Functor π’₯ π’ž} (L : Limit J) β†’ PreservesLimit F L

Cocontinuous : βˆ€ o β„“ e β†’ (F : Functor π’ž π’Ÿ) β†’ Set _
Cocontinuous {π’ž = π’ž} o β„“ e F = βˆ€ {π’₯ : Category o β„“ e} {J : Functor π’₯ π’ž} (L : Colimit J) β†’ PreservesColimit F L