Creating own Prop universe

Stream: general

[Brandon Brown]

So Prop as Sort 0 is special because of some axioms applied especially in that universe, particularly the fact that if P : Prop and a : P and b : P then definitionally a = b. Could you pick a random non-Prop universe, say Sort 23, and define these same axioms to apply just to Sort 23 and have another Prop universe? I ask because if so, I wonder if this could allow modeling other logics in Lean by just selecting a different type universe to work in as Prop and using a different set of axioms.

[Kevin Buzzard]

I would imagine that this axiom would be inconsistent because I can make bool in Sort 23

[Patrick Johnson]

It would allow you to prove false

import tactic

axiom ax (P : Sort 23) (a b : P) : a = b

example : false :=
by cases ax (ulift nat) 0 1

[Chris Bailey]

You would have to modify the kernel to play around with proof irrelevance and impredicativity as well. You can try mm0 if you want a system that does the pluggable axioms thing.

[Chris Bailey]

The inductive module also has some sort 0 behavior hard-coded for the large vs small elimination stuff.

[Junyan Xu]

I read that to do HoTT in Lean3/4 people need to disable large elimination from Prop (they don't modify the kernel, they just check separately that large elimination isn't used). I wonder what if we just define the identity type to lie in Type instead of Prop? Maybe that isn't enough, but what about just don't use Prop at all and make Type effectively the lowest universe?

[Brandon Brown]

@Patrick Johnson what if I re-defined equality to not be Prop-valued but Sort 23 valued?

[Eric Wieser]

Then I could still define old_eq as the current definition and prove false

[Floris van Doorn]

@Junyan Xu: that is what happens in practice (at least in the Lean 3 HoTT library). The fact that you disable large elimination just means you cannot do anything useful with Prop, and so it is not used.

[Junyan Xu]

@Floris van Doorn Yes it looks like that you somehow override the built-in = notation and your equality types lie in Type instead of Prop. However I can't find the definition of your custom equality type in the repo. Reading the repo is quite confusing, as Type* and Prop have different meaning than in contemporary Lean 3. I hope Type still means the same thing!

However, once you define a custom equality type that lies in Type and state the univalence axiom in terms of it, it seems that you can't derive a contradiction even if large elimination is allowed. At least this proof of false won't work because it depends on ua bswap = ua (iso.refl bool) which you get from proof irrelevance because they're both proofs of bool = bool : Prop; however if bool = bool : Type then bool = bool isn't necessarily a subsingleton so you can't seem to prove ua bswap = ua (iso.refl bool). So why is there a need to disable large elimination? Is it possible to derive a contradiction from the following?

universe u

inductive Id {α : Sort u} (a : α) : α → Type
| refl [] : Id a

infix ` ≡ `:50 := Id

structure is_iso {α β} (f : α → β) :=
(inv_fun : β → α)
(left_inv : Π a, inv_fun (f a) ≡ a)
(right_inv : Π b, f (inv_fun b) ≡ b)

structure iso (α β : Sort*) :=
(to_fun : α → β)
(is_iso : is_iso to_fun)

infix ` ≅ `:25 := iso

def iso.refl (α) : α ≅ α := ⟨id, id, Id.refl, Id.refl⟩
def transport {X Y} (h : X ≡ Y) : X ≅ Y := Id.rec (iso.refl X) h
constant ua {X Y} : is_iso (@transport X Y)

[Junyan Xu]

By the way, I have trouble getting the hott3 repo to work; when I do lean --make src/hott it seems to correctly download Lean 3.7.0 as specified in the leanpkg.toml, as confirmed by running lean --version. However errors like the following immediately appear:

/Users/xuj18/Desktop/hott3/src/hott/types/pi.lean:1:0: error: file 'hott/arity' not found in the LEAN_PATH
/Users/xuj18/Desktop/hott3/src/hott/types/pi.lean:1:0: error: file 'hott/cubical/square' not found in the LEAN_PATH

If I open the repo in VSCode I immediately get "Server has stopped with error code 1", and I guess that's due to incompatibiliy with latest VSCode Lean extension.

[Gabriel Ebner]

You need to run leanpkg configure first.

[Junyan Xu]

Thanks that works (for compilation)! But the VSCode problem isn't related to that right? I saw that leanpkg configure was run the first time I open a file in VSCode.

[Gabriel Ebner]

It works for me. What platform are you on?

[Floris van Doorn]

The definition of equality is here: https://github.com/gebner/hott3/blob/7ead7a8a2503049eacd45cbff6587802bae2add2/src/hott/init/path0.lean#L18

[Floris van Doorn]

Yes, that version of ua is inconsistent with large elimination. With large elimination you are able to prove that Id a b \equiv (a = b) (and Id a b \iso (a = b)) (just apply path induction / eq.rec for both functions and both proofs), so Id a b is a subsingleton.

[Junyan Xu]

@Gabriel Ebner I'm on Mac, the following is the output:

cannot parse: Miscellaneous:
cannot parse:   --help -h          display this message
cannot parse:   --version -v       display version number
cannot parse:   --githash          display the git commit hash number used to build this binary
cannot parse:   --run              executes the 'main' definition
cannot parse:   --doc=file -r      generate module documentation based on module doc strings
cannot parse:   --make             create olean files
cannot parse:   --recursive        recursively find *.lean files in directory arguments
cannot parse:   --trust=num -t     trust level (default: max) 0 means do not trust any macro,
cannot parse:                      and type check all imported modules
cannot parse:   --quiet -q         do not print verbose messages
cannot parse:   --memory=num -M    maximum amount of memory that should be used by Lean
cannot parse:                      (in megabytes)
cannot parse:   --timeout=num -T   maximum number of memory allocations per task
cannot parse:                      this is a deterministic way of interrupting long running tasks
cannot parse:   --threads=num -j   number of threads used to process lean files
cannot parse:   --tstack=num -s    thread stack size in Kb
cannot parse:   --deps             just print dependencies of a Lean input
cannot parse:   --path             display the path used for finding Lean libraries and extensions
cannot parse:   --json             print JSON-formatted structured error messages
cannot parse:   --server           start lean in server mode
cannot parse:   --server=file      start lean in server mode, redirecting standard input from the specified file (for debugging)
cannot parse:   --profile          display elaboration/type checking time for each definition/theorem
cannot parse:   -D name=value      set a configuration option (see set_option command)
cannot parse: Exporting data:
cannot parse:   --export=file -E   export final environment as textual low-level file
cannot parse:   --only-export=decl_name   only export the specified declaration (+ dependencies)
cannot parse:   --test-suite       capture output and status code from each input file $f in $f.produced and $f.status, respectively
lean: unrecognized option `--old'
Unknown command line option
Lean (version 3.7.0, commit 401f4b723054, Release)

[Junyan Xu]

maybe I need to remove the --old from command line options ...

[Junyan Xu]

Indeed it works now. Thanks!

[Junyan Xu]

Floris van Doorn said:

Yes, that version of ua is inconsistent with large elimination. With large elimination you are able to prove that Id a b \equiv (a = b) (and Id a b \iso (a = b)) (just apply path induction / eq.rec for both functions and both proofs), so Id a b is a subsingleton.

Thanks for the hint! I confirm that I can derive a contradiction from my ua, and now I agree that large elimination needs to be disabled. It suffices to show that Id_of_eq is a left inverse of eq_of_Id, and it's also easy to show that they form an equiv/iso:

def Id_of_eq {α} {a b : α} (h : a = b) : a ≡ b := eq.rec (Id.refl a) h
def eq_of_Id {α} {a b : α} (h : a ≡ b) : a = b := Id.rec rfl h

lemma inv_Id_of_eq {α} {a b : α} :
  function.left_inverse (@Id_of_eq α a b) (@eq_of_Id α a b) :=
λ h, by { apply Id.rec_on h, refl }

lemma subsingleton_of_injective {α β} {f : α → β} (hf : function.injective f) [subsingleton β] :
  subsingleton α := ⟨λ a a', hf $ subsingleton.elim _ _⟩

def bnot_bnot' (b : bool) : bnot (bnot b) ≡ b := Id_of_eq (bnot_bnot b)
def bswap : bool ≅ bool := ⟨bnot, bnot, bnot_bnot', bnot_bnot'⟩
example : false :=
begin
  have h1 : transport (ua.inv_fun bswap) tt = ff :=
    congr_arg (λ e : bool ≅ bool, e tt) (eq_of_Id $ ua.right_inv bswap),
  haveI : subsingleton (bool ≡ bool) := subsingleton_of_injective inv_Id_of_eq.injective,
  have h2 : ua.inv_fun bswap = ua.inv_fun (iso.refl _) := subsingleton.elim _ _,
  rw [h2, eq_of_Id (ua.right_inv _)] at h1, cases h1,
end

def Id_iso_eq {α} {a b : α} : (a ≡ b) ≅ (a = b) :=
⟨eq_of_Id, ⟨Id_of_eq, λ h, by { apply Id.rec_on h, apply Id.refl }, Id.refl⟩⟩