andrejbauer

    Variable A : Type.
    Variable P : A -> Type.
    Variable Q : forall x, P x -> Type.

    Lemma transport_funext (f g : forall x, P x) (n : forall x, Q x (f x)) (E : forall x, f x = g x) (x : A) :
      (transport (fun h => forall x, Q x (h x)) (funext E) n) x = transport (Q x) (E x) (n x).

andrejbauer

% Testing how lookup in an associative list works.

% We consider associative lists with keys of type key and values
% of type value.
%
% Ideally, we want key to be any type with decidable
% equality and value to be any type. However, we use natural numbers
% as keys so that we can convince Twelf that key has decidable equality.
% Is there a way to tell Twelf "assume key has decidable equality"?
%

andrejbauer

(* The Mandelbrot set.

   Compile with:

   ocamlbuild mandelbrot.native

   Example usage:
   
   ./mandelbrot.native --xmin 0.27085 --xmax 0.27100 --ymin 0.004640 --ymax 0.004810 --xres 1000 --maxiter 1024 --file pic.ppm

andrejbauer

Official Zermelo-Fraenkel set theory only has the elementhood relation symbol ∈, and nothing else. Other constants, such as ∅, ⊆, ∩, ∪, f[x], etc. can be mechanically eliminated. The result of the elimination is a formula which is logically equivalent to the original, but is more complicated.

This program eliminates constants and function symbols, and generates LaTeX showing the formula before and after the elimination.

andrejbauer

(** 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

andrejbauer

(** * 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

(* 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

(* 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

(* 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

-- empty type
data 𝟘 : Set where

absurd : {A : Set} → 𝟘 → A
absurd ()

-- booleans
data 𝟚 : Set where
  false true : 𝟚