Hello, World

Bedrock's minimal literate module: reflexivity gives a path from any point to itself, checked by the same toolchain this site is built with.

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

open import Cubical.Foundations.Prelude

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