cubical type theory with UIP

[Michael Shulman]

I am wondering about versions of cubical type theory with UIP. The
motivation would be to have a type theory with canonicity for
1-categorical semantics that can prove both function extensionality
and propositional univalence. (I am aware of Observational Type
Theory, which I believe has UIP and proves function extensionality,
but I don't think it proves propositional univalence -- although I
would be happy to be wrong about that.)

Presumably we obtain a cubical type theory that's compatible with
axiomatic UIP if in CCHM cubical type theory we postulate only a
single universe of propositions. But I wonder about some possible
refinements, such as:

1. In this case do we still need *all* the Kan composition and gluing
operations? If all types are hsets then it seems like it ought to be
unnecessary to have these operations at all higher dimensions.

2. Can it be enhanced to make UIP provable, such as by adding a
computing K eliminator?

Mike

[Matt Oliveri]

I'm confused. So you want a cubical type theory with only hsets? In what sense would there be cubes, other than just points? I thoght OTT had propositional extensionality. Though maybe that's only for strict props.

[Jon Sterling]

On Fri, Jul 28, 2017, at 06:47 PM, Matt Oliveri wrote:
> I'm confused. So you want a cubical type theory with only hsets? In what
> sense would there be cubes, other than just points? I thoght OTT had
> propositional extensionality. Though maybe that's only for strict props.

I think 'propositional extensionality' in OTT was for objects which were
propositions *by definition*, as opposed to h-props in HoTT (which is
something that you prove about a type, and doesn't merely follow from
the intension of the type).

Best,
Jon

>
> On Sunday, July 23, 2017 at 6:54:39 PM UTC-4, Michael Shulman wrote:
> >
> > I am wondering about versions of cubical type theory with UIP. The
> > motivation would be to have a type theory with canonicity for
> > 1-categorical semantics that can prove both function extensionality
> > and propositional univalence. (I am aware of Observational Type
> > Theory, which I believe has UIP and proves function extensionality,
> > but I don't think it proves propositional univalence -- although I
> > would be happy to be wrong about that.)
> >
> > Presumably we obtain a cubical type theory that's compatible with
> > axiomatic UIP if in CCHM cubical type theory we postulate only a
> > single universe of propositions. But I wonder about some possible
> > refinements, such as:
> >
> > 1. In this case do we still need *all* the Kan composition and gluing
> > operations? If all types are hsets then it seems like it ought to be
> > unnecessary to have these operations at all higher dimensions.
> >
> > 2. Can it be enhanced to make UIP provable, such as by adding a
> > computing K eliminator?
> >
> > Mike
> >
>

> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Michael Shulman]

Right: up to homotopy, all cubes would be equivalent to points (hence
my question #1).

[Matt Oliveri]

Only up to homotopy? So you still want the model to be using cubical sets? Actually, couldn't you interpret OTT into the hsets, internally to HoTT? It'd be a hassle without a real solution to the infinite coherence problem, but it should work, since the h-levels involved are bounded.

[Matt Oliveri]

On Friday, July 28, 2017 at 10:25:44 PM UTC-4, Jonathan Sterling wrote:

On Fri, Jul 28, 2017, at 06:47 PM, Matt Oliveri wrote:
> I'm confused. So you want a cubical type theory with only hsets? In what
> sense would there be cubes, other than just points? I thoght OTT had
> propositional extensionality. Though maybe that's only for strict props.

I think 'propositional extensionality' in OTT was for objects which were
propositions *by definition*, as opposed to h-props in HoTT (which is
something that you prove about a type, and doesn't merely follow from
the intension of the type).

Right, that's what I meant by strict props. If so, it still seems like it should work to redefine equality for types such that hprops are quotiented based on logical equivalence, and equality of other types is left alone.

[Michael Shulman]

As I said,

> The motivation would be to have a type theory with canonicity for
> 1-categorical semantics

So no, I don't want "the model" to be using cubical sets, I want
models in all suitable 1-categories (e.g. Pi-pretopos etc.).

[Matt Oliveri]

Sorry. I got distracted because the type theory you seem to be asking for doesn't sound cubical. Like I said, I suspect OTT could handle hprop extensionality, if it doesn't already. Probably ETT could too.

[Matt Oliveri]

Now I'm having second thoughts. Quotienting together hprops might make type equality computationally relevant. Not something you want with OTT's strict props or ETT's equality. Maybe 2-dimensional type theory would be good for the job. In this case the 2-cells would not be distinguishable by equality, but might still have computational content.

[Michael Shulman]

But it seems to me that cubical type theory could solve these problems
in a nicer way, which is why I asked.

[Matt Oliveri]

On Sun, Jul 30, 2017 at 4:26 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> I am interested in this question.
>
> Univalent type theory gives something we don't have in e.g. the calculus
> of constructions, such as unique choice, or function extensionality or
> propositional extensionality.
>
> A very attractive type theory, before we start to consider higher
> dimensional types that are not sets, is an intensional Martin-Loef type
> theory in with universes of propositions and of sets, with propositional
> truncation, function extensionality, propositional extensionality,
> quotients, Sigma and Exists.
>
> (1) What is this type theory? (Whatever it is, it is a common extension
> of some spartan intensional Martin-Loef type theory and the internal
> language of the free elementary topos.)
>
> (2) What are its models? In particular (as Mike asks), which fragment of
> the cubical model does it correspond to?
>
> Martin

I'm curious what you guys are thinking of doing with this kind of
system, and why extensional equality of strict propositions is not
enough. Is it just that using strict propositions is bad style for
structuralists? Or maybe I just mistakenly assumed strict
propositional extensionality is not enough.

(Any computational content of proofs of strict propositions is not
internalized. So with constructive functions, strict propositions do
not provide unique choice.)

[Matt Oliveri]

Hey what about if you start with intuitionistic set theory. Use the usual encodings of Martin-Löf types. For the universe of propositions, use the subsets of your favorite singleton. You get proposition extensionality. The way functions are defined provides function extensionality and unique choice. Now consider the realizers for this system and somehow clean it up into a type system. If the realizers are sane, you should get canonicity. Does that work? It's quite different from MLTT: you don't reason about computations. (At least not using "propositions".)

[Michael Shulman]

As I've said twice already, what I want to do with this system is use
it as an internal language for 1-toposes. So to me, that is the
answer to Martin's question (2). I'm not quite sure what Martin means
by his question (1), since he's just described a type theory, but the
original question I asked was whether cubical methods can be used to
describe a version of such a type theory with canonicity.

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.

I'm not quite sure what a "strict proposition" is, but if you mean
having a type of propositions that doesn't include all of them, then
the reason that's not enough for me is that frequently in univalent
type theory we encounter types that we *prove* to be propositions even
though they are not "given as such", such as "being contractible" and
"being a proposition", and this is responsible for a significant
amount of the unique flavor and usefulness of univalent type theory.

For semantic reasons I wouldn't want to use intuitionistic set theory,
because it doesn't naturally occur as the internal language of
categories. You can perform contortions to model it therein, but that
involves interpreting it into type theory rather than the other way
around. I don't know what you mean by "somehow clean it up into a
type system", but if you can do that cleaning up and obtain a type
theory (a "formal type theory" in Bob Harper's sense, not a
"computational type theory", i.e. one that is inductively generated by
rules rather than assigning types to untyped terms in an "intended
semantics"), then I'd like to see it.

Mike

[Matt Oliveri]

Can you point me to an example of a not-fully-satisfactory cut elimination theorem for FOL= and say what's wrong with it, so I can better appreciate the problem?

[Neelakantan Krishnaswami]

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

[Michael Shulman]

Yes, I think I've seen something like this before. It may give a good
programming language, but from a semantic category-theoretic
perspective I don't think it's any good. Two syntactically distinct
terms might still turn out to be semantically equal, so you need a
left rule for equality that does more than just syntactically analyze
the terms being equated.

[James Cheney]

Not sure if it's what you're looking for or if it is an example of a "not fully satisfactory" system, but Negri and von Plato's book "Structural Proof Theory" (esp. ch. 6) talks about axiomatic extensions to sequent calculi that preserve cut elimination.  The main idea is to turn axioms of the form

P1 & ... & Pn => Q1 | ...  | Qm

into right-rules of the form

Q1,Gamma => Delta, ... Qm, Gamma => Delta

---------------------------------------------------------------

P1,...,Pn, Gamma => Delta

so that no new principal cuts are introduced.  This can handle equality or other FOL axioms of the form forall X. /\_i Pi ==> \/_i Q_i where P_i and Q_i are atomic.

--James

> email to HomotopyTypeTheory+unsub...@googlegroups.com.

> For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.

To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsub...@googlegroups.com.

[Michael Shulman]

I think I've seen something like that too; it seems to be basically
giving up on eliminating cuts involving equalities by building them
into the primitive rules. I would expect equality to be one of the
*logical* operations, so that we can eliminate its cuts, rather than
being described by axioms as if it were part of the "theory".

>> > email to HomotopyTypeThe...@googlegroups.com.

>> > For more options, visit https://groups.google.com/d/optout.
>>
>> --
>> You received this message because you are subscribed to the Google Groups
>> "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from it, send an

>> email to HomotopyTypeThe...@googlegroups.com.

[Matt Oliveri]

On Monday, July 31, 2017 at 11:51:18 AM UTC-4, Michael Shulman wrote:

I'm not quite sure what a "strict proposition" is, but if you mean
having a type of propositions that doesn't include all of them, then
the reason that's not enough for me is that frequently in univalent
type theory we encounter types that we *prove* to be propositions even
though they are not "given as such", such as "being contractible" and
"being a proposition", and this is responsible for a significant
amount of the unique flavor and usefulness of univalent type theory.

For semantic reasons I wouldn't want to use intuitionistic set theory,
because it doesn't naturally occur as the internal language of
categories.  You can perform contortions to model it therein, but that
involves interpreting it into type theory rather than the other way
around.  I don't know what you mean by "somehow clean it up into a
type system", but if you can do that cleaning up and obtain a type
theory (a "formal type theory" in Bob Harper's sense, not a
"computational type theory", i.e. one that is inductively generated by
rules rather than assigning types to untyped terms in an "intended
semantics"), then I'd like to see it.

I'm thinking it would look a lot like OTT, but with unique choice for strict props. Not all subsingletons are strict props, so they would not be subject to propositional extensionality. So this is apparently not what you want.

However, I'm not very confident about all that. I wouldn't be that surprised if it worked out differently. (In particular, something OTT-like, but with unique choice may not even make sense.) But I don't think it'll be what you want, in any case. I've lost interest in that approach.

[Andrea Vezzosi]

Not really an answer, but one observation about point 2:

> 2. Can it be enhanced to make UIP provable, such as by adding a
> computing K eliminator?

I think we would rather derive K from a computing UIP, because even
the J eliminator is derived by proving that any element of (Sigma (y :
A), x = y) is equal to (x , refl) by using connections (and then using
comp on the obtained path).

I think something along these lines should work: suppose we add a
primitive UIP0 for every type A (restricting to some universe if
needed)

UIP0 A : (x y : A) (p : x = y) -> p = refl

then "UIP0 A a b (\ i. t)" could compute by scrutinizing A: in case A
is a "positive" type it would commute with introductions when a, b and
t are all built with the same one; in case A is a "negative" type it
would commute with the eliminations.

It's quite probable that UIP0 will have to be generalized a bit to
make sense for path types, just like composition generalizes transport
by also having a system.

This might make connections in the interval type redundant, because
they wouldn't be needed for J.


Best,
Andrea