Stefan pushed to branch master at Stefan / Typer
Commits: 749381e0 by Stefan Monnier at 2018-11-23T22:51:34Z * samples/hurkens.typer: Add a few comments.
- - - - -
1 changed file:
- samples/hurkens.typer
Changes:
===================================== samples/hurkens.typer ===================================== @@ -21,13 +21,25 @@ * = Type; \square = Type1;
-%% p (S) = (S -> *); FIXME: internal error! +%% 𝓅 is the "powerset". +%% 𝓅 S = (S -> *); FIXME: internal error! 𝓅 : \square -> \square; 𝓅 (S : \square) = (S -> Type); 𝓅𝓅 S = 𝓅 (𝓅 S);
+%%%% A "powerful" universe (U, σ, τ). +%% We need that ∀ C : 𝓅𝓅 U +%% +%% σ(τ C) = {X | {y|τ(σ y) ∈ X} ∈ C} +%% +%% i.o.w +%% +%% (σ ∘ τ) = (τ ∘ σ)** +%% +%% where * is ... + U : \square; -U = (X : \square) ≡> (𝓅𝓅 X -> X) -> 𝓅𝓅 X; +U = (X : \square) ≡> (𝓅𝓅 X -> X) -> 𝓅𝓅 X; % Uses the (▵,□,□) rule!
τ : 𝓅𝓅 U -> U; τ t = lambda (X : \square) @@ -38,29 +50,41 @@ U = (X : \square) ≡> (𝓅𝓅 X -> X) -> 𝓅𝓅 X; σ : U -> 𝓅𝓅 U; σ (s : U) = (s (X := U) (lambda (t : 𝓅𝓅 U) -> τ t));
+τσ y = τ (σ y); +%% στ x = σ (τ x); + Δ : 𝓅 U; -Δ = lambda (y : U) -> ¬((p : 𝓅 U) ≡> σ y p -> p (τ (σ y))); +Δ = lambda (y : U) -> ¬((p : 𝓅 U) ≡> σ y p -> p (τσ y));
+%% Ω = τ {X | X is inductive} Ω : U; Ω = τ (lambda (p : 𝓅 U) -> ((y : U) ≡> σ y p -> p y));
-boom1 : ((p : 𝓅 U) ≡> ((y : U) ≡> σ y p -> p y) -> p Ω) -> ⊥; +%%%% Proof that Ω is both well-founded and not + +%% FIXME: Not sure if this means well-founded or the opposite! +well-founded = ((p : 𝓅 U) ≡> ((y : U) ≡> σ y p -> p y) -> p Ω); + +boom1 : ¬ well-founded; boom1 = lambda (v0 : (p : 𝓅 U) ≡> ((y : U) ≡> σ y p -> p y) -> p Ω) -> v0 (p := Δ) (lambda (y : U) ≡> lambda (v2 : σ y Δ) -> - lambda (v3 : (p : 𝓅 U) ≡> σ y p -> p (τ (σ y))) + lambda (v3 : (p : 𝓅 U) ≡> σ y p -> p (τσ y)) -> v3 (p := Δ) v2 (lambda (p : 𝓅 U) - ≡> v3 (p := lambda (y : U) -> p (τ (σ y))))) - (lambda (p : 𝓅 U) ≡> v0 (p := lambda (y : U) -> p (τ (σ y)))); + ≡> v3 (p := lambda (y : U) -> p (τσ y)))) + (lambda (p : 𝓅 U) ≡> v0 (p := lambda (y : U) -> p (τσ y)));
-boom2 : (p : 𝓅 U) ≡> ((y : U) ≡> σ y p -> p y) -> p Ω; +boom2 : well-founded; boom2 = lambda (p : 𝓅 U) ≡> lambda (v1 : (y : U) ≡> σ y p -> p y) -> v1 (y := Ω) - (lambda (y : U) ≡> v1 (y := τ (σ y))); + %% FIXME: (lambda (x : U) ≡> v1 (y := τσ x)) + %% signals a spurious "DeBruijn index 1 refers to wrong name. + %% Expected: `y` got `x`". + (lambda (y : U) ≡> v1 (y := τσ y));
%% FIXME: Defining `boom` as below inf-loops, which I believe is a bug %% (call it an accidental feature)!
View it on GitLab: https://gitlab.com/monnier/typer/commit/749381e080170dc733ee71b977f14a6b3f24...