Erase first index of TySubst

jespercockx · Mar 22, 2024 · 651d2a2 · 651d2a2
1 parent 28504f2
commit 651d2a2
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Agda/Core/Typing.agda b/src/Agda/Core/Typing.agda
@@ -55,7 +55,7 @@ data TyTerm (@0 Γ : Context α) : @0 Term α → @0 Type α → Set
 -- TyElim Γ u e t a means: if  Γ ⊢ u : t  then  Γ ⊢ appE u e : a
 data TyElim  (@0 Γ : Context α) : @0 Term α → @0 Elim α → @0 Type α → @0 Type α → Set
 
-data TySubst (@0 Γ : Context α) : (β ⇒ α) → @0 Telescope α β → Set
+data TySubst (@0 Γ : Context α) : @0 (β ⇒ α) → @0 Telescope α β → Set
 
 data TyBranches (@0 Γ : Context α) (@0 dt : Datatype)
                 (@0 ps : dataParameterScope dt ⇒ α)