andrejbauer

open import Level
open import Relation.Binary
open import Data.Product
open import Data.Unit
open import Agda.Builtin.Sigma
open import Relation.Binary.PropositionalEquality renaming (refl to ≡-refl; trans to ≡-trans; sym to ≡-sym; cong to ≡-cong)
open import Relation.Binary.PropositionalEquality.Properties
open import Function.Equality hiding (setoid)

module Epimorphism where

andrejbauer

open import Data.Nat
open import Data.Maybe
open import Data.Product

-- An implementation of infinite queues fashioned after the von Neuman ordinals

module Queue where

   infixl 5 _⊕_

andrejbauer

open import Data.Nat
open import Data.Fin as Fin

module Primrec where

  -- The datatype of primitive recursive function
  data PR : ∀ (k : ℕ) → Set where
    pr-zero : PR 0 -- zero
    pr-succ : PR 1 -- successor
    pr-proj : ∀ {k} (i : Fin k) → PR k -- projection

andrejbauer

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

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

-- empty type
data 𝟘 : Set where

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

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

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

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

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