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

open import Agda.Builtin.Equality

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

open import Data.Empty
open import Data.Sum

I+V : A → Set
I+V a = I a ⊎ V a

C+V : (a : A) → I+V a → A → Set
C+V a (inj₁ i) = C a i
C+V a (inj₂ r) = λ _ → ⊥

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

module WithDependentElimination where

  open import Data.Product
  open import Inductive.Constructors.Ind-types I+V C+V 

  absurd : (a : A) → ⊥ → Ind a
  absurd a ()
  
  Canonical : {a : A} → Ind a → Set
  Canonical (ind _ (inj₁ i) f) = ∀ b r → Canonical (f b r)
  Canonical (ind _ (inj₂ r) f) = f ≡ absurd

  ▹ : A → Set
  ▹ a = Σ (Ind a) Canonical

  rf : (a : A) → V a → ▹ a
  rf a r = ind a (inj₂ r) absurd , refl

  tr : (a : A) (i : I a) → ((b : A) → C a i b → ▹ b) → ▹ a
  tr a i f = (ind a (inj₁ i) (λ j r → proj₁ (f j r))) ,
              λ b r → proj₂ (f b r)

  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) (m : ▹ a)
            → M a m

  El-▹ M q₁ q₂ a (ind a (inj₂ r) absurd , refl) =
    q₁ a r

  El-▹ M q₁ q₂ a (ind a (inj₁ i) f , c) =
    q₂ a i
    (λ b r → (f b r) , (c b r))
    λ b r → El-▹ M q₁ q₂ b ((f b r) , (c b r))

  C₁-▹ : (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₁-▹ M q₁ q₂ a r = refl

  C₂-▹ : (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₂-▹ M q₁ q₂ a i r = refl


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

module WithoutDependentElimination where

  open import Inductive.Constructors.Ind-types I+V C+V

  ▹ : A → Set
  ▹ = Ind

  rf : (a : A) → V a → ▹ a
  rf a r = ind a (inj₂ r) λ _ ()

  tr : (a : A) (i : I a) → ((b : A) → C a i b → ▹ b) → ▹ a
  tr a i = ind a (inj₁ i)

  Rec-▹ : (M : (a : 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₂ = Rec-Ind M λ { a (inj₁ i)   → q₂ a i
                              ; a (inj₂ v) _ → q₁ a v }

  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