module Univ where

open import Data.Nat hiding (fold)
open import Data.Product
open import Data.Unit
open import Data.Empty
open import Data.Bool hiding (T)
open ≤-Reasoning


module Dummy (n : ℕ)(U : ∀ {m} -> .(m < n) -> Set) where
  mutual
    data `U : Set where 
      `u : ∀ m -> .(m < n) -> `U
      `pi : (A : `U) -> (B : `El A -> `U) -> `U
        
    `El : `U -> Set
    `El (`u _ m<n) = U m<n
    `El (`pi A B) = (a : `El A) -> `El (B a)

open Dummy


data Acc {A : Set} (_<_ : A → A → Set) : A → Set where 
  acc : ∀ {x} → (∀ y → .(y < x) → Acc _<_ y) → Acc _<_ x

wf-< : ∀ x -> (∀ y → .(y < x) → Acc _<_ y)
wf-< zero _ ()
wf-< (suc n) y lt = 
     acc λ z z<y -> wf-< n z (lemma z z<y lt)
  where 
    lemma : ∀ z -> (z < y) -> y < (suc n) -> z < n
    lemma z z<y (s≤s y≤n) = (begin 
                               suc z ≤⟨ z<y ⟩ 
                               y     ≤⟨ y≤n ⟩ 
                               n     ∎)
∀Acc : ∀ x -> Acc _<_ x
∀Acc n = acc (wf-< n)
mutual
  U' : (n : ℕ) -> Acc _<_ n -> Set
  U' n (acc f) = `U n λ {m} m<n → U' m (f _ m<n)
  T' : (n : ℕ) -> (a : Acc _<_ n) -> U' n a -> Set
  T' n (acc f) u = `El n (λ {m} m<n → U' m (f _ m<n)) u
  U : (n : ℕ) -> Set
  U n = U' n (∀Acc n)  
  T : (n : ℕ) -> U n -> Set
  T n u = T' n (∀Acc n) u

inc : ∀ {m n} -> m < n -> m < suc n
inc (s≤s z≤n) = s≤s z≤n
inc (s≤s (s≤s m≤n)) = s≤s (inc (s≤s m≤n))

open import Relation.Binary.PropositionalEquality

postulate
  exte : ∀ {A : Set} {B : A → Set} → {f g : (a : A) → B a} → (∀ a → f a ≡ g a) → f ≡ g
  exti1 : ∀ {A : Set} {C : A → Set1} → {f g : {a : A}→ C a} → (∀ a  → f {a} ≡ g {a}) → _≡_ {A = {a : A} → C a} f g
  exte1 : ∀ {A : Set} {B : Set1} → {f g : .A → B} → (∀ a → f a ≡ g a) → f ≡ g

equalU : ∀ {n} (a b : Acc _<_ n) -> U' n a ≡ U' n b
equalU (acc rs) (acc rs') = cong (`U _) (exti1 (λ a → exte1 (λ a' → equalU _ _)))

subst-id : ∀ {A B : Set} (eq1 : A ≡ B) (eq2 : B ≡ A) -> ∀ {x} -> subst (\ x -> x) eq1 (subst (\ x -> x) eq2 x) ≡ x
subst-id refl refl = refl

mutual 
  up : ∀ {n} -> U n -> U (suc n)
  up {zero} (`u _ ())
  up {zero} (`pi A B) = `pi (up A) (λ x → up (B (out A x)))
  up {suc n} (`u m m<n) = `u m (inc m<n)
  up {suc n} (`pi A B) = `pi (up A) (λ x → up (B (out A x)))
  
  out : ∀ {n} (A : U n) -> T (suc n) (up A) -> T n A
  out {zero} (`u _ ()) x
  out {zero} (`pi A B) x = λ a →
                               out {zero} (B a)
                               (subst (λ x' → `El _ _ (up (B x'))) (iso1 {zero} A a) (x (inn {zero} A a)))
  out {suc n} (`u m m<n) x = subst (λ x' → x') (equalU (wf-< (suc (suc n)) m (inc m<n)) (wf-< (suc n) m m<n)) x
  out {suc n} (`pi A B) x = λ a → out {suc n} (B a) 
                                  (subst (λ x' → `El _ _ (up (B x'))) (iso1 {suc n} A a) (x (inn {suc n} A a)))

  inn : ∀ {n} (A : U n)  -> T n A -> T (suc n) (up A)
  inn {zero} (`u _ ()) x
  inn {zero} (`pi A B) x = λ a → inn {zero} (B (out {zero} A a)) (x (out {zero} A a))
  inn {suc n} (`u m m<n) x = subst (λ x' → x') (equalU (wf-< (suc n) m m<n) (wf-< (suc (suc n)) m (inc m<n))) x
  inn {suc n} (`pi A B) x = λ a → inn {suc n} (B (out {suc n} A a)) (x (out {suc n} A a))

  iso1 : ∀ {n} (A : U n) (a : T n A) -> out A (inn A a) ≡ a
  iso1 {zero} (`u _ ()) a
  iso1 {zero} (`pi A B) a = exte lemma where
    lemma : (a' : `El _ _ A) →
      out (B a')
      (subst
       (λ x' → `El _ _ (up (B x')))
       (iso1 A a') (inn (B (out A (inn A a'))) (a (out A (inn A a')))))
      ≡ a a'
    lemma a' rewrite iso1 A a' = iso1 (B a') (a a')
  iso1 {suc n} (`u m m<n) a = subst-id (equalU (wf-< (suc (suc n)) m (inc m<n)) (wf-< (suc n) m m<n)) 
                                         (equalU (wf-< (suc n) m m<n) (wf-< (suc (suc n)) m (inc m<n)))
  iso1 {suc n} (`pi A B) a = exte lemma where
    lemma : (a' : `El _ _ A) →
      out (B a')
      (subst
       (λ x' → `El _ _ (up (B x')))
       (iso1 A a') (inn (B (out A (inn A a'))) (a (out A (inn A a')))))
      ≡ a a'
    lemma a' rewrite iso1 A a' = iso1 (B a') (a a')


upn : ∀ n {m} -> U m -> U (n + m)
upn zero x = x
upn (suc n) x = up (upn n x)

syntax upn n x = x ↑ n

idt : U 1
idt = `pi (`u 0 (s≤s z≤n)) λ x → `pi (x ↑ 1) λ _ → x ↑ 1