Skip to content

Instantly share code, notes, and snippets.

View andrejbauer's full-sized avatar

Andrej Bauer andrejbauer

View GitHub Profile
@andrejbauer
andrejbauer / Corey.agda
Created June 1, 2021 22:46
The type of bit streams is uncountable.
open import Data.Bool
open import Data.Empty
open import Agda.Builtin.Nat
open import Agda.Builtin.Sigma
open import Relation.Binary.PropositionalEquality
module Corey where
-- streams of bits
record Stream : Set where
@andrejbauer
andrejbauer / finite.v
Created February 5, 2021 21:14
The finite truth values are precisely the decidable truth values.
(** Prop is a complete lattice. We can ask which propositions are finite. *)
Definition directed (D : Prop -> Prop) :=
(exists p , D p) /\ forall p q, D p -> D q -> exists r, D r /\ (p -> r) /\ (q -> r).
(** A proposition p is finite when it has the following property:
for any directed D, if p ≤ sup D then there is q ∈ D such that p ≤ q. *)
Definition finite (p : Prop) :=
forall D, directed D ->
(p -> exists q, D q /\ q) -> exists q, D q /\ (p -> q).
@andrejbauer
andrejbauer / doubleNegationInitialAlgebra.agda
Created January 4, 2021 23:53
The initial algebra for the functor X ↦ (X → ∅) → ∅ is ∅.
-- empty type
data 𝟘 : Set where
absurd : {A : Set} 𝟘 A
absurd ()
-- booleans
data 𝟚 : Set where
false true : 𝟚
@andrejbauer
andrejbauer / finite_subsets_and_LEM.v
Created November 15, 2020 08:41
The proof that excluded middle follows if all subsets of a singleton set are finite.
(* If all subsets of a singleton set are finite, then excluded middle holds.*)
Require Import List.
(* We present the subsets of X as characteristic maps S : X -> Prop.
Thus to say that x : X is an element of S : Powerset X we write S x. *)
Definition Powerset X := X -> Prop.
(* Auxiliary relation "l lists the elements of S". *)
Definition lists {X} (l : list X) (S : Powerset X) :=
forall x, S x <-> In x l.
@andrejbauer
andrejbauer / UniverseInjection.agda
Last active February 28, 2021 10:27
Formalization of the fact that a dependent type theory with excluded middle cannot have a universe Set such that Set → Set injects into Set.
-- Counterexample by Chung Kil Hur, improved by Andrej Bauer
-- We show that it is inconsistent to have an injection I : (Set → Set) → Set and excluded middle.
-- Indeed, excluded middle and I together give a surjection J : Set → (Set → Set),
-- which by Lawvere's fixed point theorem begets a fixed point operator on Set.
-- However, negation does not have a fixed point.
module cantor where
-- generalities
@andrejbauer
andrejbauer / algebraic.v
Last active January 15, 2020 22:21
Unions of algebraic sets are algebraic
(* A Coq formalization of the theorem that the the union of algebraic sets are algebraic.
The file is self-contained, so we start with some general definitions
and facts from logic and sets, and basic algebraic definitions.
It should be straight-forward to translate it to any setting that has
a decent library of basic facts of logic, set theory and algebra.
*)
(* We formalize the following "paper" proof.
@andrejbauer
andrejbauer / ConstructibleNumbers.nb
Last active September 25, 2020 10:51
Generation of constructible numbers in Mathematica
(* Content-type: application/vnd.wolfram.mathematica *)
(*** Wolfram Notebook File ***)
(* http://www.wolfram.com/nb *)
(* CreatedBy='Mathematica 11.2' *)
(*CacheID: 234*)
(* Internal cache information:
NotebookFileLineBreakTest
@andrejbauer
andrejbauer / algebraic.py
Created August 14, 2019 12:47
Pictures of algebraic numbers
#!/usr/local/bin/python3
# Compute algebraic numbers in the complex plane and draw a nice picture
import numpy
import sys
import argparse
import math
import cairo
import pickle
@andrejbauer
andrejbauer / localization.ml
Last active May 2, 2018 09:23
Experiments in using multicore OCaml effects to simulate dynamically created local effects.
(** * General support for creation of dynamic effects *)
(** We show how to use the multicore Ocaml effects to dynamically generate local
effects. Such effects are akin to the Eff resources, and they can be used to
implement ML references.
The code is based on "Eff directly in OCaml" by Oleg Kiselyov and KC
Sivaramakrishnan (http://kcsrk.info/papers/caml-eff17.pdf). It was written by
Andrej Bauer, Oleg Kiselyov, and Stephen Dolan at the Dagstuhl seminar
"Algebraic Effect Handlers go Mainstream". *)
@andrejbauer
andrejbauer / functional2tree.eff
Created April 19, 2018 16:05
Use of effects and handlers to compute the tree representation of a functional.
(** This code is compatible with Eff 5.0, see http://www.eff-lang.org *)
(** We show that with algebraic effects and handlers a total functional
[(int -> bool) -> bool] has a tree representation. *)
(* A tree representation of a functional. *)
type tree =
| Answer of bool
| Question of int * tree * tree