From 475c61c4e11ee61d169fce4346d7062357803828 Mon Sep 17 00:00:00 2001 From: Max New <maxsnew@gmail.com> Date: Wed, 24 May 2023 09:21:23 -0400 Subject: [PATCH] lower the universe level of the terms --- formalizations/guarded-cubical/Syntax/Terms.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/formalizations/guarded-cubical/Syntax/Terms.agda b/formalizations/guarded-cubical/Syntax/Terms.agda index 97de49f..f0b7dc4 100644 --- a/formalizations/guarded-cubical/Syntax/Terms.agda +++ b/formalizations/guarded-cubical/Syntax/Terms.agda @@ -30,10 +30,10 @@ private -- Values, Computations and Evaluation contexts, -- quotiented by βη equivalence but *not* by order equivalence (i.e., up/dn laws) -data Subst : (Δ : TypeCtx) (Γ : TypeCtx) → Type (ℓ-suc ℓ-zero) -data Val : (Γ : TypeCtx) (A : SynType) → Type (ℓ-suc ℓ-zero) -data EvCtx : (Γ : TypeCtx) (A : SynType) (B : SynType) → Type (ℓ-suc ℓ-zero) -data Comp : (Γ : TypeCtx) (A : SynType) → Type (ℓ-suc ℓ-zero) +data Subst : (Δ : TypeCtx) (Γ : TypeCtx) → Type +data Val : (Γ : TypeCtx) (A : SynType) → Type +data EvCtx : (Γ : TypeCtx) (A : SynType) (B : SynType) → Type +data Comp : (Γ : TypeCtx) (A : SynType) → Type -- This isn't actually induction-recursion, this is just a hack to get -- around limitations of Agda's mutual recursion for HITs -- GitLab