Re: [HoTT] Re: cubical type theory with UIP

[Neelakantan Krishnaswami <n.krish...@cs.bham.ac.uk>]

[-- Attachment #1.1: Type: text/plain, Size: 2632 bytes --]

On Monday, July 31, 2017 at 4:51:18 PM UTC+1, Michael Shulman wrote:
>
> Another motivation is that as far as I know, there is not a really 
> satisfactory version of sequent calculus for first-order logic with 
> equality (e.g. not having a fully satisfactory cut-elimination 
> theorem).  If cubical methods are a good way to treat equality 
> "computationally", I wonder whether a "cubical sequent calculus" would 
> be able to deal with equality better. 
>

Actually, there *are* good versions of sequent calculus with 
equality. Jean-Yves Girard and Peter Schroeder-Heister have both given
the appropriate rules. So, given a language of terms with some 
equational theory, the right and left rules are:


    —————————— =R 
    Γ ⊢ t = t


    ∀θ ∈ csu(s,t). θ(Γ) ⊢ Θ(C)
    —————————————————————————— =L
    Γ, s = t ⊢ C

The premise of the left rule quantifies over a *complete set of
unifiers* for s and t. For terms freely generated by some signature,
there is a single most general unifier (if one exists), and so the
left rule has at most one premise. Once you add equations then 
there can be more than one most general unifier -- possibly  even
infinite (eg, if terms are lambda-terms modulo beta/eta, as in 
higher-order unification). 

The Girard/Schroeder-Heister equality is not the same as the Martin-Lof
identity type, but it gives rise to a nicer programming language than raw J 
does, since the left rule is invertible. Invertible left rules are what 
give rise to
pattern matching syntax, and so languages like Agda choose a fragment 
where the G/SH rule and J coincide to implement pattern matching. 

Agda restricts pattern matching so that an identity type 
argument can only have a refl pattern when the two terms being equated
are generated from variables and constructors. So an identity proof 
p : (cons x y) = (cons a b)) can be matched as refl, but an identity 
proof q : (append x y) = (append a b)) can't be. 

This restriction ensures that first-order unification suffices for the
G/SH elim, and therefore to implement pattern matching.

If you are very interested in this topic, Joshua Dunfield and I have a draft
paper where we work out the Curry-Howard story for pattern matching 
with the G/SH equality (what are called GADTs by PL theorists) in gory 
detail:

*  Sound and Complete Bidirectional Typechecking for Higher-Rank 
Polymorphism and Indexed Types*
  <http://www.cl.cam.ac.uk/~nk480/gadt.pdf>

-- 
Neel Krishnaswami
nk...@cl.cam.ac.uk 

[-- Attachment #1.2: Type: text/html, Size: 2955 bytes --]