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