open import Graded.Modality
open import Graded.Usage.Restrictions
open import Definition.Typed.Restrictions
module Graded.Erasure.LogicalRelation.Fundamental.Assumptions
{a} {M : Set a}
{š : Modality M}
(TR : Type-restrictions š)
(UR : Usage-restrictions š)
where
open Modality š
open Usage-restrictions UR
open import Definition.Untyped M
open import Definition.Typed TR
open import Definition.Typed.Consequences.Consistency TR
open import Graded.Mode š
open import Graded.Restrictions š
open import Tools.Nat
open import Tools.PropositionalEquality
open import Tools.Sum
private variable
k : Nat
record Fundamental-assumptionsā» (Ī : Con Term k) : Set a where
no-eta-equality
field
consistent : Emptyrec-allowed šįµ š ā Consistent Ī
closed-or-no-erased-matches : No-erased-matches TR UR ā k ā” 0
record Fundamental-assumptions (Ī : Con Term k) : Set a where
no-eta-equality
field
well-formed : ā¢ Ī
other-assumptions : Fundamental-assumptionsā» Ī
open Fundamental-assumptionsā» other-assumptions public
fundamental-assumptionsā»ā : Fundamental-assumptionsā» Īµ
fundamental-assumptionsā»ā = record
{ consistent = Ī» _ ā
inhabited-consistent
(_ā¢Ė¢_ā·_.id {Ļ = idSubst})
; closed-or-no-erased-matches = injā refl
}
fundamental-assumptionsā : Fundamental-assumptions Īµ
fundamental-assumptionsā = record
{ well-formed = Īµ
; other-assumptions = fundamental-assumptionsā»ā
}