-
-
Save marklemay/c8c644b733fd79ca1e5910cf379d5df2 to your computer and use it in GitHub Desktop.
This file contains hidden or 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
{-# OPTIONS --type-in-type #-} | |
-- TODO: turn this off and see what happens! | |
-- Burali-Forti's paradox in MLTT-ish without W-types | |
-- I was following Coquand's paper "An Analysis of Girard's Paradox" | |
-- and Hurkens's paper "A Simplification of Girard's Paradox". | |
-- Code is released under CC0. | |
module BuraliFortiParadox where | |
-- Σ-types | |
-- record Σ (A : Set) (B : A → Set) : Set where | |
-- constructor _,_ | |
-- field | |
-- fst : A | |
-- snd : B fst | |
--open Σ | |
--infixr 4 _,_ | |
-- this gets used a lot, and "Set" has too many conotations | |
• : Set | |
• = Set | |
Σ : (X : •) → (P : X → •) → • | |
Σ X P = { C : • } -> ( (x : X )-> P x -> C) -> C | |
Σ-intro : {X : •} {P : X → •} → (x : X ) → (proof : P x) → Σ X P | |
Σ-intro x proof = λ ih → ih x proof | |
-- Non-dependent version | |
_×_ : • → • → • | |
A × B = Σ A λ _ → B | |
-- Empty type | |
--data ⊥ : Set where | |
⊥ : • | |
⊥ = (T : •) → T | |
-- Composition | |
_∘_ : ∀ {A : •} {B : A → •} {C : (a : A) → (B a → •)} → | |
(g : {a : A} → (b : B a) → C a b) → (f : (a : A) → B a) → (a : A) → (C a (f a)) | |
g ∘ f = λ a → g (f a ) | |
-- Identity, need type in type for that | |
id : ∀ {A} → A → A | |
id x = x | |
------------------------------------------------------------------------------ | |
Rel : • → • | |
Rel A = A → A → • | |
-- pretty syntax | |
_[_<_] : {A : • } → (rel : Rel A) → (a a' : A) → • | |
rel [ a < a' ] = rel a a' | |
isTrans : {A : •} → (rel : Rel A) → • | |
isTrans rel = ∀ x y z → rel [ x < y ] → rel [ y < z ] → rel [ x < z ] | |
isInd : (A : • ) → (rel : Rel A) → • | |
isInd A rel = (P : A → • ) → ( ∀ bound → ( ( a : A ) → rel [ a < bound ] → P a ) → P bound) → (a : A) → P a | |
-- examples | |
data _≡_ {A : Set} (x : A) : A → Set where | |
refl : x ≡ x | |
data Bool : • where | |
tt : Bool | |
ff : Bool | |
data _<B_ : Bool -> Bool -> • where | |
only : ff <B tt | |
ltBoolTrans : isTrans _<B_ | |
ltBoolTrans tt _ _ () _ | |
ltBoolTrans ff tt _ _ () | |
ltBoolTrans ff ff _ () _ | |
--not big enough to not be tranisitive | |
lemma : (f : Bool) -> f <B tt -> f ≡ ff | |
lemma .ff only = refl | |
lemma2 : (P : Bool → • ) -> (f : Bool) -> f ≡ ff -> ( ih : (bound : Bool) → ((a : Bool) → _<B_ [ a < bound ] → P a) → P bound) -> P f | |
lemma2 P .ff refl ih = ih ff (λ a → λ ()) | |
ltBoolisInd : isInd Bool _<B_ | |
ltBoolisInd P ih ff = ih ff (λ a → λ ()) | |
ltBoolisInd P ih tt = ih tt (λ f f<tt → lemma2 P f (lemma f f<tt) ih) | |
data Nat : • where | |
zero : Nat | |
succ : Nat -> Nat | |
data _<N_ : Nat -> Nat -> • where | |
base : ∀ n -> zero <N (succ n) | |
step : ∀ n m -> n <N m -> n <N (succ m) | |
ltNisTrans : isTrans _<N_ | |
ltNisTrans .zero .(succ n) .(succ m) (base n) (step .(succ n) m y<z) = base m | |
ltNisTrans x .(succ m) .(succ m₁) (step .x m x<y) (step .(succ m) m₁ y<z) = step x m₁ (ltNisTrans x (succ m) m₁ (step x m x<y) y<z) | |
--ltNisInd : isInd Nat _<N_ | |
--ltNisInd P ih zero = ih zero (λ a → λ ()) | |
--ltNisInd P ih (succ n) = ih (succ n) | |
-- (λ a → | |
-- ltNisInd (λ z → (x : a <N succ n) → P z) | |
-- (λ bound z x → ih bound (λ a₁ z₁ → z a₁ z₁ x)) a) -- ih n {!!} {!!} {!!} | |
--n <N m = | |
--_<_ : (A : • ) → (rel : Rel A) → • | |
-- _<_ : ∀ {A : Set} {ord: Rel A}→ (a : A ) → (a' : A) → Set | |
-- a < a' = Ord a a' | |
-- _<_ : rel A | |
-- a < a' = rel A | |
-- ... |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment