https://twitter.com/agdakx/status/1577952310243872769?s=20&t=UJrepWvNkFpXFRNY8yoWDA agda2hs blog post jasper

Martin Escardo Introduction to Univalent Foundations of Mathematics with Agda

agda wiki

Agda manual

Programming Language Foundations in Agda

apt-get install agda agda-mode agda-stdlib
echo 'module hello-world where

open import Agda.Builtin.IO using (IO)
open import Agda.Builtin.Unit using (⊤)
open import Agda.Builtin.String using (String)

postulate putStrLn : String → IO ⊤
{-# FOREIGN GHC import qualified Data.Text as T #-}
{-# COMPILE GHC putStrLn = putStrLn . T.unpack #-}

main : IO ⊤
main = putStrLn "Hello world!"

' > /tmp/hello-world.agda
cd /tmp # Why do I have to do this? Me dunno.
agda --compile /tmp/hello-world.agda
./hello-world

The hott game Cubical Agda: a cold Introduction