This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(** 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). |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- empty type | |
data 𝟘 : Set where | |
absurd : {A : Set} → 𝟘 → A | |
absurd () | |
-- booleans | |
data 𝟚 : Set where | |
false true : 𝟚 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* 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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- 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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* 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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* Content-type: application/vnd.wolfram.mathematica *) | |
(*** Wolfram Notebook File ***) | |
(* http://www.wolfram.com/nb *) | |
(* CreatedBy='Mathematica 11.2' *) | |
(*CacheID: 234*) | |
(* Internal cache information: | |
NotebookFileLineBreakTest |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(** * 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". *) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(** 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 |