open import Definition.Typed.Restrictions
open import Graded.Modality
module Definition.Conversion.Whnf
{a} {M : Set a}
{đ : Modality M}
(R : Type-restrictions đ)
where
open Type-restrictions R
open import Definition.Untyped M
open import Definition.Untyped.Neutral M type-variant
open import Definition.Conversion R
open import Tools.Nat
open import Tools.Product as ÎŁ
private
variable
n : Nat
Î : Con Term n
mutual
ne~â : â {t u A}
â Π⢠t ~ u â A
â Neutral t Ă Neutral u
ne~â (var-refl xâ xâĄy) = var _ , var _
ne~â (app-cong x xâ) = let _ , q , w = ne~â x
in ââ q , ââ w
ne~â (fst-cong x) =
let _ , pNe , rNe = ne~â x
in fstâ pNe , fstâ rNe
ne~â (snd-cong x) =
let _ , pNe , rNe = ne~â x
in sndâ pNe , sndâ rNe
ne~â (natrec-cong x xâ xâ xâ) = let _ , q , w = ne~â xâ
in natrecâ q , natrecâ w
ne~â (prodrec-cong _ g~h _) =
let _ , gNe , hNe = ne~â g~h
in prodrecâ gNe , prodrecâ hNe
ne~â (emptyrec-cong x xâ) = let _ , q , w = ne~â xâ
in emptyrecâ q , emptyrecâ w
ne~â (unitrec-cong _ k~l _ no-Ρ) =
let _ , kNe , lNe = ne~â k~l
in unitrecâ no-Ρ kNe , unitrecâ no-Ρ lNe
ne~â (J-cong _ _ _ _ _ wâ~wâ _) =
ÎŁ.map Jâ Jâ (ne~â wâ~wâ .projâ)
ne~â (K-cong _ _ _ _ vâ~vâ _ _) =
ÎŁ.map Kâ Kâ (ne~â vâ~vâ .projâ)
ne~â ([]-cong-cong _ _ _ vâ~vâ _ _) =
ÎŁ.map []-congâ []-congâ (ne~â vâ~vâ .projâ)
ne~â : â {t u A}
â Π⢠t ~ u â A
â Whnf A Ă Neutral t Ă Neutral u
ne~â ([~] _ (_ , whnfB) k~l) = whnfB , ne~â k~l
whnfConvâ : â {A B}
â Π⢠A [convâ] B
â Whnf A Ă Whnf B
whnfConvâ (U-refl x) = Uâ , Uâ
whnfConvâ (â-refl x) = ââ , ââ
whnfConvâ (Empty-refl x) = Emptyâ , Emptyâ
whnfConvâ (Unit-refl x _) = Unitâ , Unitâ
whnfConvâ (ne x) = let _ , neA , neB = ne~â x
in ne neA , ne neB
whnfConvâ (Î ÎŁ-cong _ _ _ _) = Î ÎŁâ , Î ÎŁâ
whnfConvâ (Id-cong _ _ _) = Idâ , Idâ
whnfConvâTerm : â {t u A}
â Π⢠t [convâ] u ⡠A
â Whnf A Ă Whnf t Ă Whnf u
whnfConvâTerm (â-ins x) = let _ , neT , neU = ne~â x
in ââ , ne neT , ne neU
whnfConvâTerm (Empty-ins x) = let _ , neT , neU = ne~â x
in Emptyâ , ne neT , ne neU
whnfConvâTerm (Unit-ins x) = let _ , neT , neU = ne~â x
in Unitâ , ne neT , ne neU
whnfConvâTerm (Σʡ-ins x xâ xâ) =
let _ , neT , neU = ne~â xâ
in Î ÎŁâ , ne neT , ne neU
whnfConvâTerm (ne-ins t u x xâ) =
let _ , neT , neU = ne~â xâ
in ne x , ne neT , ne neU
whnfConvâTerm (univ x xâ xâ) = Uâ , whnfConvâ xâ
whnfConvâTerm (zero-refl x) = ââ , zeroâ , zeroâ
whnfConvâTerm (starʡ-refl _ _ _) = Unitâ , starâ , starâ
whnfConvâTerm (suc-cong x) = ââ , sucâ , sucâ
whnfConvâTerm (prod-cong _ _ _ _ _) = Î ÎŁâ , prodâ , prodâ
whnfConvâTerm (Ρ-eq xâ xâ y yâ xâ) = Î ÎŁâ , functionWhnf y , functionWhnf yâ
whnfConvâTerm (ÎŁ-Ρ _ _ pProd rProd _ _) = Î ÎŁâ , productWhnf pProd , productWhnf rProd
whnfConvâTerm (Ρ-unit _ _ tWhnf uWhnf _) = Unitâ , tWhnf , uWhnf
whnfConvâTerm (Id-ins _ vâ~vâ) =
Idâ , ÎŁ.map ne ne (ne~â vâ~vâ .projâ)
whnfConvâTerm (rfl-refl _) =
Idâ , rflâ , rflâ