Skip to content

Instantly share code, notes, and snippets.

@marklemay
Forked from favonia/BuraliFortiParadox.agda
Last active July 5, 2018 20:20
Show Gist options
  • Save marklemay/c8c644b733fd79ca1e5910cf379d5df2 to your computer and use it in GitHub Desktop.
Save marklemay/c8c644b733fd79ca1e5910cf379d5df2 to your computer and use it in GitHub Desktop.
{-# 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