NathanielB123’s gists

NathanielB123 / IO.agda

Last active April 25, 2026 18:59

	{-# OPTIONS --guardedness #-}

	open import Agda.Primitive
	open import Agda.Builtin.Unit
	import Agda.Builtin.IO as Prim

	-- IO from https://agda.github.io/agda-stdlib/master/IO.Base.html
	-- but using coinductive records instead of musical coinduction
	module IO where

NathanielB123 / QuotDec.agda

Last active March 27, 2026 12:34

Decision procedure for quotients

	{-# OPTIONS --prop --show-irrelevant --rewriting #-}

	open import Agda.Builtin.Equality
	open import Agda.Builtin.Equality.Rewrite
	open import Agda.Builtin.Bool

	-- Inspired by https://types.pl/deck/@mevenlennonbertrand@lipn.info/116300216566705883
	-- Challenge: define the decision procedure for quotients with only the
	-- non-dependent and strict-propositional eliminators
	module QuotDec where

NathanielB123 / EqPuzzle.agda

Last active March 2, 2026 19:33

	{-# OPTIONS --cubical -WnoUnsupportedIndexedMatch #-}

	open import Agda.Primitive.Cubical
	open import Agda.Builtin.Cubical.Path

	module EqPuzzle where

	data Eqs : Set
	data Var : Set
	data Tm : Eqs → Set

NathanielB123 / SubstRew.agda

Created February 11, 2026 13:57

Substitution using local rewrite rules

	{-# OPTIONS --rewriting #-}

	open import Agda.Builtin.Equality
	open import Agda.Builtin.Equality.Rewrite
	open import Agda.Builtin.Nat

	module LocalRewriteSubst where

	module Utils where
	infixr 4 _∙_

NathanielB123 / KFromSmartWith.agda

Last active April 11, 2026 14:42

Possible counter-example to "smart with without K" observed by @jespercockx

	{-# OPTIONS --without-K #-}

	open import Agda.Builtin.Equality

	-- Example due to Jesper Cockx
	module KFromSmartWith where

	data Unit : Set where ⟨⟩ : Unit

	variable

NathanielB123 / Sound.agda

Last active January 21, 2026 08:09

	{-# OPTIONS --rewriting #-}

	open import Agda.Builtin.Equality
	open import Agda.Builtin.Equality.Rewrite
	open import Agda.Builtin.Sigma renaming (_,_ to _Σ,_)
	open import Agda.Builtin.Unit renaming (⊤ to 𝟙; tt to ⟨⟩)
	open import Agda.Primitive

	-- Sketch for how to prove soundness (specifically, consistency relative to
	-- Agda) of a type theory by constructing the standard model

NathanielB123 / Lego.agda

Last active January 19, 2026 16:41

	open import Agda.Builtin.Equality
	open import Agda.Builtin.Nat renaming (zero to ze; suc to su)
	open import Agda.Builtin.Sigma

	module Lego where

	infixr 6 _,-_

	variable
	n m l : Nat

NathanielB123 / Div.agda

Last active January 7, 2026 22:35

Division by repeated subtraction

	open import Agda.Primitive
	open import Agda.Builtin.Equality

	-- Adapted from https://types.pl/deck/@jeanas@mathstodon.xyz/115855070991058388
	-- See also https://github.com/agda/agda/issues/8312

	-- Quite unfortunate that with-abstraction actually works here...
	-- I want examples where it fails!
	module Div where

NathanielB123 / StreamFinal.agda

Created December 21, 2025 13:34

Bisimulation from finality

	open import Agda.Primitive
	open import Agda.Builtin.Equality
	open import Agda.Builtin.Sigma

	module StreamFinal where

	-- Utils
	variable
	ℓ ℓ₁ ℓ₂ : Level
	A B : Set _

NathanielB123 / BoolInit.agda

Last active December 20, 2025 12:58

Induction from initiality

	open import Agda.Primitive
	open import Agda.Builtin.Equality
	open import Agda.Builtin.Sigma

	module BoolInit where

	variable
	ℓ : Level
	A B : Set _
	x y z : A

Nathaniel Burke NathanielB123