Last active
October 28, 2023 11:44
-
-
Save favonia/cc7a504839c5fbb3ebc6 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 #-} | |
-- 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. | |
-- Σ-types | |
record Σ (A : Set) (B : A → Set) : Set where | |
constructor _,_ | |
field | |
fst : A | |
snd : B fst | |
open Σ | |
infixr 4 _,_ | |
-- Non-dependent version | |
_×_ : Set → Set → Set | |
A × B = Σ A λ _ → B | |
-- Empty type | |
data ⊥ : Set where | |
-- Composition | |
_∘_ : ∀ {A : Set} {B : A → Set} {C : (a : A) → (B a → Set)} | |
→ (g : {a : A} → (b : B a) → C a b) → (f : (a : A) → B a) → (a : A) → (C a (f a)) | |
g ∘ f = λ x → g (f x) | |
-- Identity | |
id : ∀ {A : Set} → A → A | |
id x = x | |
------------------------------------------------------------------------------ | |
-- Binary relation | |
rel : Set → Set | |
rel A = A → A → Set | |
-- Is it transitive? | |
is-trans : (A : Set) → rel A → Set | |
is-trans A ordA = ∀ c b a → ordA c b → ordA b a → ordA c a | |
-- Does the induction principle hold? | |
-- | |
-- Note: [has-rec] is the official definition of "well-founded", but I decide to | |
-- consider only _transitive_ relations in [is-well-founded] for convenience. | |
-- One can always consider the transitive closure of a well-founded relation. | |
has-rec : (A : Set) → rel A → Set | |
has-rec A ordA = (P : A → Set) → (∀ a → (∀ b → ordA b a → P b) → P a) → ∀ a → P a | |
-- Is it a well-founded type? | |
-- That is, a type with a transitive, well-founded relation. | |
-- (This is DIFFERENT from "well-founded sets".) | |
is-well-founded : (A : Set) → rel A → Set | |
is-well-founded A ordA = is-trans A ordA × has-rec A ordA | |
-- The type of all well-founded types. | |
well-founded : Set | |
well-founded = Σ Set λ A → Σ (rel A) (is-well-founded A) | |
-- Convenient projection. | |
#set : well-founded → Set | |
#set = fst | |
#ord : ∀ A → rel (#set A) | |
#ord A = fst (snd A) | |
#trans : ∀ A → is-trans (#set A) (#ord A) | |
#trans A = fst (snd (snd A)) | |
#rec : ∀ A → has-rec (#set A) (#ord A) | |
#rec A = snd (snd (snd A)) | |
-- The induction principle rejects reflexivity. | |
rec-irr : ∀ A → ∀ a → #ord A a a → ⊥ | |
rec-irr A = #rec A (λ a → #ord A a a → ⊥) (λ a ih refl → ih a refl refl) | |
-- [embed-up-to A B b] means that [A] can be embedded into [B] | |
-- with the strict upper bound [b]. | |
embed-up-to : well-founded → (B : well-founded) → #set B → Set | |
embed-up-to A B b = | |
Σ (#set A → #set B) λ f -- the function | |
→ (∀ a → #ord B (f a) b) -- the proof that it's a upper bound | |
× (∀ {a₁ a₂} → #ord A a₁ a₂ → #ord B (f a₁) (f a₂)) -- the proof that it preserves orders | |
-- [embed A B] means [A] can be embedded into [B] with some upper bound | |
embed : well-founded → well-founded → Set | |
embed A B = Σ (#set B) (embed-up-to A B) | |
-- [embed] is a transitive relation on [well-founded]. | |
embed-trans : is-trans well-founded embed | |
embed-trans _ _ _ (b↑ , g , g-bound , g-mono) (_ , f , _ , f-mono) | |
= f b↑ , f ∘ g , f-mono ∘ g-bound , f-mono ∘ g-mono | |
-- [embed] admits an induction principle too! | |
embed-rec : has-rec well-founded embed | |
embed-rec P ind A = ind A lemma | |
where | |
lemma : ∀ B → embed B A → P B | |
lemma B (a↑ , embed-up-to-a↑) = #rec A P′ lemmaA a↑ B embed-up-to-a↑ | |
where | |
P′ : #set A → Set | |
P′ a↑ = ∀ B → embed-up-to B A a↑ → P B | |
lemmaA : ∀ a↑ → (∀ a↑′ → #ord A a↑′ a↑ → P′ a↑′) → P′ a↑ | |
lemmaA a↑ ih B (f , f-bound , f-mono) = ind B lemmaCB | |
where | |
lemmaCB : ∀ C → embed C B → P C | |
lemmaCB C (b↑ , g , g-bound , g-mono) = | |
ih (f b↑) (f-bound b↑) C (f ∘ g , f-mono ∘ g-bound , f-mono ∘ g-mono) | |
-- As a result, [embed] is a well-founded! | |
embed-is-well-founded : is-well-founded well-founded embed | |
embed-is-well-founded = embed-trans , embed-rec | |
-- So all the well-founded types form a well-founded | |
well-founded-well-founded : well-founded | |
well-founded-well-founded = well-founded , embed , embed-is-well-founded | |
-- Initial segment. | |
init : ∀ A → #set A → Set | |
init A a = Σ (#set A) λ b → #ord A b a | |
-- Induced order. | |
init-order : ∀ A a → rel (init A a) | |
init-order A a a+₁ a+₂ = #ord A (fst a+₁) (fst a+₂) | |
-- Induced order is still a well-founded. | |
init-is-well-founded : ∀ A a → is-well-founded (init A a) (init-order A a) | |
init-is-well-founded (A , ordA , transA , recA) a = (λ _ _ _ → transA _ _ _) , λ P indA+ b+ → | |
recA (λ b → ∀ b<a → P (b , b<a)) (λ b ih b<a → indA+ (b , b<a) (λ c+ c<b → ih (fst c+) c<b (snd c+))) (fst b+) (snd b+) | |
-- Therefore the initial segment of a well-founded type is a well-founded type. | |
init-well-founded : (A : well-founded) → #set A → well-founded | |
init-well-founded A a = init A a , init-order A a , init-is-well-founded A a | |
-- Every initial segment can be embedded back to the original well-founded type. | |
embed-init-self : ∀ A a → embed (init-well-founded A a) A | |
embed-init-self A a = a , fst , snd , λ < → < | |
-- And smaller initial segments can be embedded into the larger ones. | |
embed-init-mono : ∀ A {b a} → #ord A b a → embed (init-well-founded A b) (init-well-founded A a) | |
embed-init-mono A {b} {a} b<a = | |
(b , b<a) , | |
(λ b+ → fst b+ , #trans A _ _ _ (snd b+) b<a) , | |
snd , | |
id | |
-- Therefore, every well-founded type can be embedded into the type of all well-founded types, | |
-- where the upper bound is the well-founded type in question. | |
well-founded-is-max : ∀ A → embed A well-founded-well-founded | |
well-founded-is-max A = A , init-well-founded A , embed-init-self A , embed-init-mono A | |
-- It means that we can embed well-founded into well-founded itself. | |
absurd : ⊥ | |
absurd = rec-irr well-founded-well-founded well-founded-well-founded (well-founded-is-max well-founded-well-founded) |
Hello, I like it a lot too!
This development is very similar to Martin-Löf's presentation of Girard Paradox in his 1972 presentation of MLTT. However, he used nat-indexed sequences to define well-founded orderings.
I just translated this development to Dedukti and I remarked that the lemma init-is-tree-order
uses twice the eta rule for sigma-types implicitely: the term ih (fst c+) c<b (snd c+)
proves P (fst c+ , snd c+)
instead of P c+
and similarly, the whole recA
term proves P (fst b+ , snd b+)
instead of P b+
. Dedukti has no eta rule by default so I inserted the propositional eta rule ∀ (A : Set) (B : A → Set) (P : Σ A B → Set) (a : Σ A B) → P (fst a , snd a) → P a
.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
This is really great! Defining well ordering from an induction principle is really elegant. I didn't see that in any of the papers you cited, did you come up with it?