{-# 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)