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

-- Part (iv) of Proposition 5.2
-- A Topological Counterpart of Well-founded Trees
-- in Dependent Type Theory

open import Agda.Builtin.Equality

module Inductive.Equivalences.Ind-give-W
  (A : Set) (B : A → Set)
  where

open import Data.Unit
open import Inductive.Constructors.Ind-types {⊤} (λ _ → A) (λ _ a _ → B a)

W : Set
W = Ind tt

sup : (a : A) (f : B a → W) → W
sup a f = ind tt a λ _ b → f b

El-W : (M : W → Set)
        (d : (a : A)
             (f : B a → W)
             (h : (b : B a) → M (f b))
             → M (sup a f))
        → (w : W) → M w

El-W M d = El-Ind (λ { tt w → M w }) (λ { tt a f h → d a (f tt) (h tt) }) tt

C-W : (M : W → Set)
      (d : (a : A)
           (f : B a → W)
           (h : (b : B a) → M (f b))
           → M (sup a f))
      → (a : A) (f : B a → W)
      → El-W M d (sup a f) ≡ d a f λ b → El-W M d (f b)

C-W M d a f = refl