hunk ./HOAS/SimplyTyped/Value.agda 9
-open import Data.Function
+open import Function
hunk ./SimplyTyped/Semantics.agda 11
+open import Level
hunk ./SimplyTyped/Semantics.agda 18
-data _⇾_ : ∀ {Γ σ} → Rel (Γ ⊢ σ) where
+data _⇾_ : ∀ {Γ σ} → Rel (Γ ⊢ σ) zero where
hunk ./SimplyTyped/Semantics.agda 51
-data _⇛_ : ∀ {Γ σ} → Rel (Γ ⊢ σ) where
+data _⇛_ : ∀ {Γ σ} → Rel (Γ ⊢ σ) zero where
hunk ./SimplyTyped/Semantics.agda 59
-_⇛⋆_ : ∀ {Γ σ} → Rel (Γ ⊢ σ)
+_⇛⋆_ : ∀ {Γ σ} → Rel (Γ ⊢ σ) zero
hunk ./SimplyTyped/Substitution.agda 10
-open import Data.Function
+open import Function
hunk ./SimplyTyped/Value.agda 12
-open import Data.Function
+open import Function