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

open import Data.Product
open import Data.Sum

-- Inductive part of Proposition 9 of
-- A topological reading of coinductive
-- predicates in Dependent Type Theory

module Inductive.Equivalences.▹-as-fixedpoint
  {A : Set}
  (I : A → Set)
  (C : (a : A) → I a → A → Set)
  (V : A → Set)
  where

open import Endofunctors
open Topological I C V

module SmallestFixedPoint-give-▹ (S : SmallestFixedPoint Der) where

  open SmallestFixedPoint S

  ▹ : A → Set
  ▹ = P

  rf : (a : A) → V a → ▹ a
  rf a v = closed (inj₁ v)
  
  tr : (a : A) (i : I a) → ((b : A) → C a i b → ▹ b) → ▹ a
  tr a i f = closed (inj₂ (i , f))

  Rec-▹ : (M : A → Set)
      (q₁ : (a : A) (r : V a) → M a)
      (q₂ : (a : A)
            (i : I a)
            (f : (b : A) → (p : C a i b) → M b)
            → M a)
      → (a : A) (w : ▹ a)
      → M a
  Rec-▹ M q₁ q₂ a = smallest {M} λ { (inj₁ v) → q₁ _ v
                                   ; (inj₂ (i , f)) → q₂ _ i f }

module ▹-give-SmallestFixedPoint where

  open import Inductive.Constructors.▹-types I C V

  ▹-is-smallest : SmallestFixedPoint Der
  ▹-is-smallest = record {
    P = ▹ ;
    closed = λ { (inj₁ v) → rf _ v
               ; (inj₂ (i , f)) → tr _ i f } ;
    smallest = λ {Q} c
      → Rec-▹ Q (λ _ r → c (inj₁ r)) (λ a i f → c (inj₂ (i , f))) _
    }