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

open import Data.Product

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

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

open import Endofunctors
open With-rule-set I C

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

  open SmallestFixedPoint S

  Ind : A → Set
  Ind = P
  
  ind : (a : A)
        (i : I a)
        (f : (b : A) → C a i b → Ind b)
        → Ind a
  ind a i f = closed (i , f)

  Rec-Ind : (M : (a : A) → Set)
            (c : (a : A)
                (i : I a)
                (h : (j : A) (r : C a i j) → M j)
                → M a)
            → (a : A) (w : Ind a) → M a

  Rec-Ind M c a = smallest {M} λ { (i , f) → c _ i f }

module Ind-give-SmallestFixedPoint where

  open import Inductive.Constructors.Ind-types I C

  Ind-is-smallest : SmallestFixedPoint Der
  Ind-is-smallest = record {
    P = Ind ;
    closed = λ { (i , f) → ind _ i f } ;
    smallest = λ {Q} c w
      → Rec-Ind Q (λ a i h → c (i , h)) _ w
    }