Hello, World

Bedrock 的最小文学化模块：自反性给出从任意一点到其自身的道路，由构建本站点的同一套工具链检查。

{-# OPTIONS --cubical --safe --guardedness #-}
module HelloWorld where

open import Cubical.Foundations.Prelude

hello : {ℓ : Level} {A : Type ℓ} (x : A) → x ≡ x
hello x = refl