{-# OPTIONS --rewriting #-}

module WF  where

open import Equality
open import Fibration
open import FunExt
open import Interval
open import Level
open import Path
open import Product
open import WellFoundedTree

----------------------------------------------------------------------
-- W types
----------------------------------------------------------------------
Wf :
  {ℓ ℓ' ℓ'' : Level}
  {Γ : Set ℓ}
  (A : Γ → Set ℓ')
  (B : Σ Γ A  → Set ℓ'')
  → -------------------
  Γ → Set (ℓ' ⊔ ℓ'')
Wf A B x = W (A x) (λ a → B (x , a))

WfAct :
  {ℓ ℓ' ℓ'' : Level}
  {Γ : Set ℓ}
  (A : Γ → Set ℓ')
  {{_ : isFib A}}
  (B : Σ Γ A → Set ℓ'')
  {{_ : isFib B}}
  (x y : Γ)
  (p : x ~ y)
   → -----------------
   Wf A B x → Wf A B y
WfAct A B _ _ p (sup a f) =
  sup (p ∗ a) (λ b → WfAct A B _ _ p (f ((~symm (~lift p a)) ∗ b)))
  
WfActId :
  {ℓ ℓ' ℓ'' : Level}
  {Γ : Set ℓ}
  (A : Γ → Set ℓ')
  {{_ : isFib A}}
  (B : Σ Γ A → Set ℓ'')
  {{_ : isFib B}}
  (x  : Γ)
  (t : Wf A B x)
  → ---------------------------
  t ~ WfAct A B x x (~refl x) t
WfActId A {{α}} B {{β}} x (sup a f) =
  path:
    sup a f
  ~[ ~cong (sup a) (~funext (λ b →
     ~cong (λ b → WfAct A B x x (~refl x) (f b))
       (~substrefl β b) ∙ WfActId A B _ (f b))) ]
    sup a (λ b → WfAct A B x x (~refl x)
    (f (~subst β (~refl (x , a)) b)))
  ~[ ⟨ i ⟩(sup (~substrefl α a at i) (λ b → WfAct A B x x (~refl x)
     (f (~subst β (~symm (~cong (x ,_)
     ((~substrefl α a) upto i))) b)))) ]
    sup (~subst α (~refl x) a) (λ b → WfAct A B x x (~refl x)
    (f (~subst β (~symm (~cong (x ,_) (~substrefl α a))) b)))
  ~[ ~cong (λ p → sup (~subst α (~refl x) a)
     (λ b → WfAct A B x x (~refl x)
     (f (~subst β (~symm p) b)))) (~symm (~liftrefl x a)) ]
    sup (~subst α (~refl x) a) (λ b → WfAct A B x x (~refl x)
    (f (~subst β (~symm (~lift (~refl x) a)) b)))
  endp

isFibWf :
  {ℓ ℓ' ℓ'' : Level}
  {Γ : Set ℓ}
  (A : Γ → Set ℓ')
  {{_ : isFib A}}
  (B : Σ Γ A → Set ℓ'')
  {{_ : isFib B}}
  → -------------------
  isFib (Wf A B)
isFibWf A B = (WfAct A B , WfActId A B)