module Uxx where

open import Relation.Binary.PropositionalEquality
open import Data.Nat

_,_⊢_≡_ : {A : Set}(B : A → Set){a a' : A} → a ≡ a' → B a → B a' → Set
B , refl ⊢ a ≡ a' = a ≡ a'

dcong : {A : Set}(B : A → Set)(f : (a : A) → B a)
  {a a' : A}(p : a ≡ a') → B , p ⊢ f a ≡ f a'
dcong B f refl = refl 

data U : Set 
El : U → Set

data U where
  nat : U
  π : (a : U)(b : El a → U) → U

postulate 
  eqUx : ∀ {a b} → El a ≡ El b → a ≡ b

El nat = ℕ
El (π a b) = (x : El a) → El (b x)

RecU : (X : Set)
     → X
     → ((a : U) → X → (b : El a → U) → ((El a) → X) → X)
     → (∀ {a b}(p : El a ≡ El b)(x y : X) → x ≡ y)
     → U → X
RecU X n p q nat = n
RecU X n p q (π a b) = p a (RecU X n p q a) b (λ x → RecU X n p q (b x))

ElimU : (X : U → Set) 
       → (X nat)
       → ((a : U) → X a → (b : El a → U) → ((x : El a) → X (b x)) → X (π a b))
       → (∀ {a b}(p : El a ≡ El b)(x : X a)(y : X b) → X , eqUx p ⊢ x ≡ y)
       → (a : U) → X a
ElimU X n p q nat = n
ElimU X n p q (π a b) = p a (ElimU X n p q a) b (λ x → ElimU X n p q (b x))

postulate 
  ElimU' : (X : U → Set) 
       → (n : X nat)
       → (p : (a : U) → X a → (b : El a → U) → ((x : El a) → X (b x)) → X (π a b))
       → (q : ∀ {a b}(p : El a ≡ El b)(x : X a)(y : X b) → X , eqUx p ⊢ x ≡ y)
       → ∀ {a b}(α : El a ≡ El b) → dcong X (ElimU X n p q) 
              (eqUx α) ≡ q α (ElimU X n p q a) (ElimU X n p q b)

  El' : ∀ {a b}(α : El a ≡ El b) → cong El (eqUx α) ≡ α