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

open import Agda.Builtin.Equality

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

open import Data.Empty
open import Inductive.Constructors.▹-types I C (λ _ → ⊥)

Ind : A → Set
Ind = ▹ 

ind : (a : A) (i : I a) (f : (b : A) → C a i b → Ind b) → Ind a
ind = tr

-- Part of Proposition 5.1 of
-- A Topological Counterpart of Well-founded Trees in Dependent Type Theory

module WithDependentElimination where

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

  El-Ind M c = El-▹ M (λ { a () }) c
    
  C-Ind : (M : (a : A) → Ind a → Set)
          (c : (a : A)
                (i : I a)
                (f : (j : A) → C a i j → Ind j)
                (h : (j : A) (r : C a i j) → M j (f j r))
                → M a (ind a i f))
          → (a : A) (i : I a) (f : (b : A) → C a i b → Ind b)
          → El-Ind M c a (ind a i f) ≡ c a i f λ j r → El-Ind M c j (f j r)

  C-Ind M c a i f = refl


-- Part of Theorem 10 of
-- A topological reading of coinductive predicates in dependent type theory

module WithoutDependentElimination where

  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 = Rec-▹ M (λ { a () }) c

  C-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) (i : I a) (f : (b : A) → C a i b → Ind b)
          → Rec-Ind M c a (ind a i f) ≡ c a i λ j r → Rec-Ind M c j (f j r)

  C-Rec-Ind M c a i f = refl