Stefan pushed to branch master at Stefan / Typer

Commits: c081c586 by Stefan Monnier at 2020-03-20T11:28:31-04:00 -

- - - - -

1 changed file:

- samples/hott.typer

Changes:

===================================== samples/hott.typer ===================================== @@ -47,8 +47,8 @@ %% We additionally need some kind of elimination on paths like: %% %% Eq_call : Eq(_ := ?t) ?x ?y ≡> I ≡> ?t; -%% Eq_call _ i₀ ↝ ?x -%% Eq_call _ i₁ ↝ ?y +%% Eq_call (_ : Eq x y) i₀ ↝ x +%% Eq_call (_ : Eq x y) i₁ ↝ y %% %% Heterogenous equality could look like: %% @@ -81,7 +81,7 @@ Equiv_function f (g : (x : ?A) -> ?B) = ((x : ?A) -> Eq (f x) (g x)); %% %% It'd be great to support univalence without losing `Eq_cast`, but %% it's not at all clear how: -%% - One way is to make it a non-axiom and replace it with a system that +%% - One way is to make it a non-axiom and implement it as a system that %% proves it directly on a case-by-case basis, as in the paper %% "Equivalence for Free!". %% - Another is to make `Eq_cast` take a proof of `isSet T`, @@ -95,6 +95,17 @@ Equiv_function f (g : (x : ?A) -> ?B) = ((x : ?A) -> Eq (f x) (g x)); %% %% but that begs the question: how could we prevent "promoting" %% a non-erasable proof to an erasable one? +%% - Another is to distinguish univalent universes, as done in the paper +%% "Extending Homotopy Type Theory with Strict Equality". +%% E.g. Our sorts `Type ℓ` would be refined to `Type k ℓ` where `k` +%% would be a boolean indicating if the universe admits univalence or not, +%% and then the J (aka "cast") rule would be restricted so that a proof +%% about equality between univalent types can only be used to coerce +%% between univalent types. +%% This is reminiscent of the confinement of Prop in Coq, so we could +%% similarly restrict the univalent universes so they're always erased +%% before runtime (so we don't need to have the non-nop form of "cast" +%% at run-time).

%%%% Propositions, resizing, etc...

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/c081c5869f90f7f00b87a1ac179557bb1c...