Implement checking for sigmas

jonsterling / TT-Reflection

An experimental type theory with scoped equality reflection, and non-arbitrary proof search. This is basically a pared down version of Andromeda/Brazil, but with untyped reduction and a more Nuprl-like feel. Computational content of proofs is got via a realizability-based extraction. (Note: substitution is unsafe here, not because of a problem with the theory, but because I didn't understand how Bound works sadly.)

12 stars 0 forks source link

Implement checking for sigmas #6

Closed jonsterling closed 10 years ago

jonsterling commented 10 years ago

[x] Type formation
[x] Introduction: Pair
[x] Elimination: Spread
[x] Also, Spread needs a first parameter which is the motive. So the elimination rule needs to look like this:

     Γ !-[Σ;E] p : Σ[x:A]B             
     Γ, x : Σ[x:A]B !-[Σ;E] C : U
     Γ, u:A, v:[u/x]B !-[Σ;E] M : [<u,v>/x]C
-----------------------------------------------------
     Γ !-[Σ;E] spread([x]C; [u,v]M; p) : [p/x]C

Therefore, we have in the syntax:

Spread :: (B.Scope () Tm a) -> (B.Scope Bool Tm a) -> Tm a -> Tm a