{-# OPTIONS --without-K --exact-split #-}

open import Data.Product

-- Endofunctors used to semantically define coinductive types
-- as in Section 4 of
-- "A topological reading of coinductive
--  predicates in Dependent Type Theory"

module Endofunctors where

_⇒_ : ∀ {A : Set} → (A → Set) → (A → Set) → Set
_⇒_ {A} P Q = {a : A} → P a → Q a

module With-rule-set
  {A : Set}
  (I : A → Set)
  (C : (a : A) → I a → A → Set)
  where

  Der : (A → Set) → (A → Set)
  Der P a = Σ (I a) λ i → ∀ b → C a i b → P b

  Der⇒ : ∀ {P Q} → P ⇒ Q → Der P ⇒ Der Q
  Der⇒ p (i , f) = i , λ b c → p (f b c)

  Conf : (A → Set) → (A → Set)
  Conf P a = ∀ i → Σ A λ b → C a i b × P b

  Conf⇒ : ∀ {P Q} → P ⇒ Q → Conf P ⇒ Conf Q
  Conf⇒ p q i with q i
  ... | b , c , r = b , c , p r

-- Topological operators
module Topological
  {A : Set}
  (I : A → Set)
  (C : (a : A) → I a → A → Set)
  (V : A → Set)
  where

  open import Data.Sum

  Der : (A → Set) → A → Set
  Der P a = V a ⊎ Σ (I a) λ i → ∀ b → C a i b → P b

  Der⇒ : ∀ {P Q} → P ⇒ Q → Der P ⇒ Der Q
  Der⇒ p (inj₁ r) = inj₁ r
  Der⇒ p (inj₂ (i , f)) = inj₂ (i , λ b c → p (f b c))

  Conf : (A → Set) → A → Set
  Conf P a = V a × ∀ i → Σ A λ b → C a i b × P b

  Conf⇒ : ∀ {P Q} → P ⇒ Q → Conf P ⇒ Conf Q
  Conf⇒ p (v , f) =
    v , λ i → proj₁ (f i) , proj₁ (proj₂ (f i)) , p (proj₂ (proj₂ (f i)))

module With-indexed-container
  {A : Set}
  (I : A → Set)
  (Br : (a : A) → I a → Set)
  (ar : (a : A) (i : I a) → Br a i → A)
  where

  Der : (A → Set) → (A → Set)
  Der P a = Σ (I a) λ i → ∀ b → P (ar a i b)

  Der⇒ : ∀ {P Q} → P ⇒ Q → Der P ⇒ Der Q
  Der⇒ p (i , f) = i , λ b → p (f b)

  Conf : (A → Set) → (A → Set)
  Conf P a = ∀ i → Σ (Br a i) λ b → P (ar a i b)

  Conf⇒ : ∀ {P Q} → P ⇒ Q → Conf P ⇒ Conf Q
  Conf⇒ p f i with f i
  ... | b , q = b , p q

module _ {A : Set} (F : (A → Set) → (A → Set)) where

  record SmallestFixedPoint : Set₁ where
    field
      P        : A → Set
      closed   : F P ⇒ P
      smallest : ∀ {Q} → F Q ⇒ Q → P ⇒ Q

  record GreatestFixedPoint : Set₁ where
    field
      P        : A → Set
      correct  : P ⇒ F P
      greatest : ∀ {Q} → Q ⇒ F Q → Q ⇒ P