Skip to content

Instantly share code, notes, and snippets.



View GitHub Profile
View Cantor.agda
{-# OPTIONS --without-K #-}
open import Data.Bool
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Data.Empty
open import Function
surj : {A B : Set} (A B) Set
surj f = b λ a f a ≡ b
AndrasKovacs / cont-cwf.agda
Created Jun 18, 2020 — forked from bobatkey/cont-cwf.agda
Construction of the Containers / Polynomials CwF in Agda, showing that function extensionality is refuted
View cont-cwf.agda
{-# OPTIONS --rewriting #-}
module cont-cwf where
open import Agda.Builtin.Sigma
open import Agda.Builtin.Unit
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Data.Empty
open import Relation.Binary.PropositionalEquality public using (_≡_; refl; trans; subst; cong)
AndrasKovacs / GluedEval.hs
Last active Aug 31, 2020
Non-deterministic normalization-by-evaluation in Olle Fredriksson's flavor.
View GluedEval.hs
{-# language Strict, LambdaCase, BlockArguments #-}
{-# options_ghc -Wincomplete-patterns #-}
Minimal demo of "glued" evaluation in the style of Olle Fredriksson:
The main idea is that during elaboration, we need different evaluation
AndrasKovacs / FixNf.hs
Last active Oct 13, 2020
Minimal environment machine normalization with a fixpoint operator
View FixNf.hs
{-# language Strict, BangPatterns #-}
data Tm = Var Int | App Tm Tm | Lam Tm | Fix Tm deriving (Show, Eq)
data Val = VVar Int | VApp Val Val | VLam [Val] Tm | VFix [Val] Tm
isCanonical :: Val -> Bool
isCanonical VLam{} = True
isCanonical _ = False
eval :: [Val] -> Tm -> Val
View CCCNbE.agda
open import Data.Unit
open import Data.Product
infixr 4 _⇒_ _*_ ⟨_,_⟩ _∘_
data Obj : Set where
: Obj
base : Obj
_*_ : Obj Obj Obj
View CellularUnrolled.hs
{-# language Strict, TypeApplications, ScopedTypeVariables,
PartialTypeSignatures, ViewPatterns #-}
{-# options_ghc -Wno-partial-type-signatures #-}
import qualified Data.Primitive.PrimArray as A
import GHC.Exts (IsList(..))
import Data.Bits
import Data.Word
import Control.Monad.ST.Strict
AndrasKovacs / Cellular.hs
Last active Apr 10, 2020
Cellular automata
View Cellular.hs
{-# language Strict #-}
import qualified Data.Primitive.PrimArray as A
import GHC.Exts (IsList(..))
import Data.Bits
import Data.Word
type Rule = A.PrimArray Word8
mkRule :: Word8 -> Rule
AndrasKovacs / Ordinals.agda
Last active Sep 25, 2020
Large countable ordinals and numbers in Agda
View Ordinals.agda
{-# OPTIONS --postfix-projections --without-K --safe #-}
Large countable ordinals in Agda. For examples, see the bottom of this file.
Checked with Agda
Countable ordinals are useful in "big number" contests, because they
can be directly converted into fast-growing ℕ → ℕ functions via the
fast-growing hierarchy:
AndrasKovacs / IITfromNat.agda
Last active May 14, 2020
Constructing finitary inductive types from natural numbers
View IITfromNat.agda
{-# OPTIONS --without-K #-}
Claim: finitary inductive types are constructible from Π,Σ,Uᵢ,_≡_ and ℕ, without
quotients. Sketch in two parts.
1. First, construction of finitary inductive types from Π, Σ, Uᵢ, _≡_ and binary trees.
Here I only show this for really simple, single-sorted closed inductive types,
but it should work for indexed inductive types as well.
AndrasKovacs / CumulativeIRUniv.agda
Last active Oct 6, 2020
Transfinite, cumulative, Russell-style, inductive-recursive universes in Agda.
View CumulativeIRUniv.agda
Inductive-recursive universes, indexed by levels which are below an arbitrary type-theoretic ordinal number (see HoTT book 10.3). This includes all kinds of transfinite levels as well.
Checked with: Agda 2.6.1, stdlib 1.3
My original motivation was to give inductive-recursive (or equivalently: large inductive)
semantics to to Jon Sterling's cumulative algebraic TT paper:
You can’t perform that action at this time.