andrejbauer

(* We want to implement a trusted kernel which is the only module that can
   produce values of some abstract type jdg, but at the same time we want to be
   able to expose the values of type jdg so they can be inspected, tested, etc.

   In some cases OCaml private types will do the job, but not always. Here is a
   solution that uses OCaml modules. The idea is as follows:

   1. Implement an untrusted transparent kernel which makes everything visible.
   2. Using signatures, create a trusted opaque version of the transparent kernel
      with an additional expose function that maps opaque values to non-opaque values.

andrejbauer

module Ackermann where

  open import Data.Nat
  open import Relation.Binary.PropositionalEquality

  -- Primitive recursion a la System T, for defining maps ℕ → τ for any type τ.
  primrec : ∀ {τ : Set} → τ → (ℕ → τ → τ) → ℕ → τ
  primrec x f zero = x
  primrec x f (suc m) = f m (primrec x f m)

andrejbauer

-- In type theory we can show that ℕ and Bool are not equal as follows

module N≠Bool where

open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Bool
open import Data.Sum
open import Data.Empty

andrejbauer

(* The basic theory of Lawvere-Tierney operators and sheafification in logical form.

   This formalization is based on:

   Barbara Veit: A proof of the associated sheaf theorem by means of categorical logic,
   The Journal of Symbolic Logic , Volume 46 , Issue 1 , March 1981 , pp. 45–55
   DOI: https://doi.org/10.2307/2273255
*)

Require Import Utf8.

andrejbauer

module Myhill where

import Data.List (find)

type N = Integer

-- given injective maps `f, g : N → N` that witness 1-1 reductions `A ≤₁ B` and `B ≤₁ A`, respectively,
-- `myhill f g` computes the graph of a bijection `h : N → N` that witnesses `A ≡ B`, see
-- https://en.wikipedia.org/wiki/Myhill_isomorphism_theorem
myhill :: (N -> N) -> (N -> N) -> [(N,N)]

andrejbauer

(* A proof that there is a least closure operator which forces a given
   predicate to be true. The construction can be found in, e.g.,
   Martin Hyland's “Effective topos” paper, Proposition 16.3. *)

(* A closure operator on [Prop] is an idempotent, monotone, inflationary enodmap.

   One often requires additionally that the operator preserves conjunctions,
   in which case these are also called j-operators and Lawvere-Tierney topologies.
   We eschew the condition to obtain a slighly more general result, but we
   also show that the closure operator of interst happens to preserve conjunctions.

andrejbauer

(* A formalization of a classical propositional calculus a la user4035,
   see https://proofassistants.stackexchange.com/q/4443/169 and
   https://proofassistants.stackexchange.com/q/4468/169 ,
   with the following modifications:

   1) We use a set of assumptions rather than a list of assumptions.
   2) We use derivation trees to represent proofs instead of lists of formulas.

   Proofs-as-lists are used in Hilbert-style systems, whereas
   derivation trees are more common in natural-deduction style rules.

andrejbauer

-- A predicative version of Tarski's fixed-point theorem

open import Level
open import Data.Product

module Tarski where

  -- a complete preorder with carrier at level a, the preorder is at level b,
  -- and suprema indexed by sets from level c
  record CompletePreorder a b c : Setω where

andrejbauer

Experiments involving Miquel's theorem. Joint work with Finn Klein.

andrejbauer

# 
METHOD: TABLE
ENCODE: Unicode
PROMPT: LaTeX
VERSION: 1.0
DELIMITER: ,
VALIDINPUTKEY: ^,.?!:;"'/\()[]{}<>$%&@*01234567890123456789ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz
TERMINPUTKEY: 
BEGINCHARACTER
alpha	α