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

open import Agda.Builtin.Equality

module Inductive.Constructors.Ind-types
  {A : Set}
  (I : A → Set)
  (C : (a : A) → I a → A → Set)
  where
  
data Ind : A → Set where
  ind : (a : A)
        (i : I a)
        (f : (b : A) → C a i b → Ind b)
        → Ind a

-- Elimination towards types depending on Ind
-- as in Martin-Löf's type theory

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 a (ind a i f) = c a i f λ j r → El-Ind M c j (f j r)

C-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) (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-El-Ind M c a i f = refl

-- Elimination towards types not depending on Ind
-- as in the Minimalist Foundation / the Calculus of Constructions

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 (ind a i f) = c a i λ b r → Rec-Ind M c b (f b r)

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 λ b r → Rec-Ind M c b (f b r)

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