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 https://leanpub.com/certainty-by-construction sandy maguire book

https://dl.acm.org/doi/abs/10.1145/3437992.3439922 Formalizing category theory in Agda

https://link.springer.com/chapter/10.1007/978-3-030-33636-3_10
System F in Agda, for Fun and Profit

https://yangzhixuan.github.io/pdf/free.pdf Algebraic Effects Meet Hoare Logic in Cubical Agda - Kidney, Yang, Wu

https://dl.acm.org/doi/abs/10.1145/3607861 Timely Computation Conal Elliot

https://cris.vub.be/ws/portalfiles/portal/66013205/TyDeAbstract.pdf Shallowly Embedding Type Theories as Presheaf Models in Agda

https://arxiv.org/abs/2306.15375 Frex: dependently-typed algebraic simplification

https://github.com/JacquesCarette/PureBaggery

https://github.com/pigworker/CS410-17 cs 410 mcbride

Well Typed Syntax

https://dl.acm.org/doi/pdf/10.1145/3498715 Formal Metatheory of Second-Order Abstract Syntax

https://arxiv.org/abs/1804.00119 Generic Description of Well-Scoped, Well-Typed Syntaxes Erdi

https://link.springer.com/article/10.1007/s10817-011-9219-0 2012 benton et al Strongly Typed Term Representations in Coq

Altenkirch and Reus [1999] Monadic presentations of lambda terms using generalized inductive types https://link.springer.com/chapter/10.1007/3-540-48168-0_32

Richard S. Bird and Ross Paterson. 1999. de Bruijn notation as a nested datatype

Allais, Atkey, Chapman, McBride, and McKinna [2021] https://www.cambridge.org/core/journals/journal-of-functional-programming/article/type-and-scopesafe-universe-of-syntaxes-with-binding-their-semantics-and-proofs/8A0865F34313BA65F4FE46D4522B4568 https://dl.acm.org/doi/10.1145/3236785 A type and scope safe universe of syntaxes with binding: their semantics and proofs

http://strictlypositive.org/ren-sub.pdf 2005 mcbride Type-Preserving Renaming and Substitution

https://www.youtube.com/watch?v=imz9UkdQBdI&ab_channel=LFCSSeminar horsten Altenkirch: How to define type theories?

mcbride thinning and substitution https://www.youtube.com/watch?v=ahwCXcYHkXQ&t=1853s&ab_channel=ConorMcBride

https://docs.idris-lang.org/en/latest/tutorial/interp.html well typed interpeter example idris

https://lean-lang.org/lean4/doc/examples/interp.lean.html well typed interpreter lean

https://richarde.dev/papers/2018/stitch/stitch.pdf Stitch: The Sound Type-Indexed Type Checker (Functional Pearl) - eisenberg

https://bentnib.org/posts/2015-04-19-algebraic-approach-typechecking-and-elaboration.html An algerbaic approahc to typchecking and elaboration - bob atkey

Idris

Eh, they’re similar enough. Wow. Idris. Takes me back

Idris 2: Quantitative Type Theory in Practice

idris

Zanzi https://zanzix.github.io/posts/bcc.html Lambda Calculus And Bicartesian Closed Categories https://gist.github.com/zanzix Second Order Algebraic Theories https://gist.github.com/zanzix/df5eb62079d4bc3a56306a1de4f276cd “two theories” kappa and zeta calculus https://gist.github.com/zanzix/0e113d5aef1c7e0a985328fac35fa032

Typed Syntax. Thinnings telescope

Relative monads https://stringdiagram.com/2023/05/28/relative-monads/

Quantitative type theory 0 1 omega algebraic paths optics open games

https://github.com/Jademaster/TheCategoryMachine/tree/main

https://gist.github.com/Jademaster/755ec0d389c41e8a681f8bdd27be8e76 Grothendieckconstruction.idr

https://gist.github.com/Jademaster/df24f8d2640c066ddbe427e98547d35e freesemiring.idr

https://www.cis.upenn.edu/~sweirich/papers/yorgey-thesis.pdf brent yorgey theis COMBINATORIAL SPECIES AND LABELLED STRUCTURES

https://blog.functorial.com/posts/2017-06-18-Stack-Safe-Traversals-via-Dissection.html phil freeman. Stack safe traversal via dissections https://github.com/PureFunctor/purescript-ssrs

https://github.com/adamgundry/type-inference/blob/master/src/Milner/Zipper.lhs zipperized algorithm W https://types.pl/@pigworker/111375156578265560 more n phd thesis

https://www.researchgate.net/profile/Peter-Dybjer/publication/226035566_Inductive_families/links/0f317532159fcea814000000/Inductive-families.pdf dybjer inductive families