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

open import Agda.Builtin.Equality

module Inductive.Constructors.▹-types
  {A : Set}
  (I : A → Set)
  (C : (a : A) → I a → A → Set)
  (V : A → Set)
  where

data ▹ : A → Set where
  rf : (a : A) → V a → ▹ a
  tr : (a : A) (i : I a) → ((b : A) → C a i b → ▹ b) → ▹ a

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

El-▹ : (M : (a : A) → ▹ a → Set)
      (q₁ : (a : A) (r : V a) → M a (rf a r))
      (q₂ : (a : A)
            (i : I a)
            (k : (b : A) → C a i b → ▹ b)
            (f : (b : A) → (p : C a i b) → M b ((k b) p))
            → M a (tr a i k))
      → (a : A) (w : ▹ a)
      → M a w

El-▹ M q₁ q₂ a (rf a r) = q₁ a r
El-▹ M q₁ q₂ a (tr a i k) = q₂ a i k (λ b p → El-▹ M q₁ q₂ b (k b p))

C₁-El-▹ : (M : (a : A) → ▹ a → Set)
      (q₁ : (a : A) (r : V a) → M a (rf a r))
      (q₂ : (a : A)
            (i : I a)
            (k : (b : A) → C a i b → ▹ b)
            (f : (b : A) → (p : C a i b) → M b ((k b) p))
            → M a (tr a i k))
      → (a : A) (r : V a)
      → El-▹ M q₁ q₂ a (rf a r) ≡ q₁ a r

C₁-El-▹ M q₁ q₂ a r = refl

C₂-El-▹ : (M : (a : A) → ▹ a → Set)
      (q₁ : (a : A) (r : V a) → M a (rf a r))
      (q₂ : (a : A)
            (i : I a)
            (k : (b : A) → C a i b → ▹ b)
            (f : (b : A) → (p : C a i b) → M b ((k b) p))
            → M a (tr a i k))
      → (a : A) (i : I a) (r : (b : A) → C a i b → ▹ b)
      → El-▹ M q₁ q₂ a (tr a i r) ≡ q₂ a i r λ b p → El-▹ M q₁ q₂ b (r b p)

C₂-El-▹ M q₁ q₂ a i r = refl

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

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 (rf a r) = q₁ a r
Rec-▹ M q₁ q₂ a (tr a i k) = q₂ a i (λ b p → Rec-▹ M q₁ q₂ b (k b p))

C₁-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) (r : V a)
      → Rec-▹ M q₁ q₂ a (rf a r) ≡ q₁ a r

C₁-Rec-▹ M q₁ q₂ a r = refl

C₂-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) (i : I a) (r : (b : A) → C a i b → ▹ b)
      → Rec-▹ M q₁ q₂ a (tr a i r) ≡ q₂ a i λ b p → Rec-▹ M q₁ q₂ b (r b p)

C₂-Rec-▹ M q₁ q₂ a i r = refl