BuraliFortiParadox.agda

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

-- ...