Repository navigation
A variant of Cubical Agda that is consistent with UIP #3750
Description
Activity
XTT is relevant, but it also goes all the way to definitional UIP (which we might want, but we might not need to start there).
For consistency of UIP you need to:
- Restrict to only set-truncated HITs
- Disable
Glue
You would then have hcomp in the universe as a new canonical type former when \phi is not i1. This type former would have introduction and elimination rules once we implement the change proposed in #3599 (comment).
This doesn't sound so bad:
- Disable
Glue
Easy.
- Restrict to only set-truncated HITs
I suppose one way to do this would be to check that at least one constructor of every higher inductive type family D has the type ∀ {Δ} → Is-set (D Γ Δ) (or something like that).
This type former would have introduction and elimination rules once we implement the change proposed in #3599 (comment).
OK, once that change has been implemented I suggest that we also implement "--cubical-with-uip".
- Restrict to only set-truncated HITs
Is this restriction really needed? At least in book HoTT, it is perfectly consistent to consider the circle HIT together with UIP, it just happens that the circle will be contractible. You need univalence to prove that the circle is not contractible, so there is no contradiction.
I am very much in favour of a version of cubical with UIP. Ideally we could also make UIP hold definitionally.
OK, once that change has been implemented I suggest that we also implement "
--cubical-with-uip".
That is a bad name choice, I want something that is consistent with both UIP and univalence. Let me provisionally call the flag --cubical-without-glue. I'd like this flag to imply --without-K, and I want it to be compatible with --cubical. If possible I'd also like it to be compatible with --with-K, but perhaps the combination of HITs and the K rule requires more thought.
@guillaumebrunerie I suppose the circle might be fine, but the HIT formed by two disjoint lines wouldn't be. Because you could map the two lines respectively to (\ i -> true) and (\ i -> false) and derive a contradiction from the proof that the lines are equal.
The circle doesn't seem to allow for such a proof, maybe there's a better property than set-truncation to consider?
the HIT formed by two disjoint lines
@Saizan What do you mean exactly by that? If the lines have disjoint endpoints, then they are not equal even with UIP.
@guillaumebrunerie Oh, you are right of course. I forgot about that.
In fact it seems that a model where everything is set-truncated (either weakly or strictly) would be able to support the same eliminators by using the truncatedness of the codomain.
Ok, so we just need to restrict Glue, much better.
8 remaining items
I'm joining this discussion late -- it was pointed out to me by Jesper when he closed my #4379.
As #4379 says, I am currently happily abusing Cubical Agda by combining parts of it --with-K. I would be very happy if there were was an option that brings in a subset of --cubical that excludes the primitives and builtins in Agda.Builtin.Cubical.Glue (actually I don't think one needs Agda.Builtin.Cubical.Sub or Agda.Builtin.Cubical.Id either).
Why not call the option --interval, since it provides a form of interval type theory.
About definitional UIP: I don't see that as an issue -- I am already using "abused Cubical" with option --prop as well as --with-K and the definitional UIP in Prop seems sufficient (combined with postulating unique choice).
About effective quotients: I agree that propositional extensionality seems needed to prove it, but there are lots of interesting applications of mere quotients (coequalizers) that don't need them to be effective.
I'm joining this discussion late -- it was pointed out to me by Jesper when he closed my #4379.
As #4379 says, I am currently happily abusing Cubical Agda by combining parts of it --with-K. I would be very happy if there were was an option that brings in a subset of --cubical that excludes the primitives and builtins in Agda.Builtin.Cubical.Glue (actually I don't think one needs Agda.Builtin.Cubical.Sub or Agda.Builtin.Cubical.Id either).
Why not call the option --interval, since it provides a form of interval type theory.
To clarify, you would still want transp and hcomp for every type in Set l, right?
To me --interval would suggest that we don't assume "types" have composition.
About definitional UIP: I don't see that as an issue -- I am already using "abused Cubical" with option --prop as well as --with-K and the definitional UIP in Prop seems sufficient (combined with postulating unique choice).
That's unique choice for strictly propositional types right?
I was surprised today by the fact that I was able to import Agda.Primitive.Cubical without enabling --cubical or --erased-cubical, i.e. the following file is valid Agda:
UIP : {A : Set} (x y : A) (p q : x ≡ y) → p ≡ q
UIP x y refl refl = refl
funext : {A B : Set} (f g : A → B) → (∀ x → PathP (λ _ → B) (f x) (g x)) → PathP (λ _ → A → B) f g
funext f g p i x = p x iHowever, one still needs --cubical or --erased-cubical to prove that the two notions of equality are equivalent, so one doesn't get both UIP and funext for the same identity type. Still, it's surprising how far things already seem to work.
I just want to bump this issue. Agda cubical without Glue would have a number of advantages over plain Agda:
- Provable function (and, if I'm not mistaken, codata type) extensionality,
- Quotient inductive types,
- You could soundly postulate UIP, although I guess it would lack computational content.
Such a system would allow a project like Sikkel to escape from setoid and even groupoid hell without having to go through complicated inductive universe constructions. @JorisCeulemans
Required changes w.r.t. --cubical:
- Disable Glue.
Requirements that seem to be already satisfied by --cubical:
- Without Glue,
hcompfor the universe would have to be a constructor. However, I believe it already is. @antoinevanmuylder
Changes that have been suggested above but are not necessary:
- Check that every HIT has an
isSetconstructor: As mentioned by @guillaumebrunerie, you need univalence to prove that any HIT without such constructor is not an hSet.
Definitional UIP or propositional UIP with computational behaviour would definitely be fun, but if it's unknown how to, or significantly more involved to implement such things, then I think they should not be in the way of providing the more basic feature.
Likewise, compatibility with other flags is also something that can be sorted out later if it's currently not well-understood. One could initially choose to take a conservative (or, as Agda tends to do, lenient) position and converge to a more logically sound situation.
Quick test: In the following code, AD does not normalize to a Glue type (nor to anything else).
{-# OPTIONS --cubical #-}
open import Cubical.Foundations.Prelude
postulate
A B C D : Set
AB : A ≡ B
BC : B ≡ C
CD : C ≡ D
AD : A ≡ D
AD i = hcomp {φ = i ∨ ~ i}
(λ where
j (i = i0) → AB (~ j)
j (i = i1) → CD j
)
(BC i)@antoinevanmuylder confirms that universe hcomps do not reduce to Glue.
Quoting @Saizan , after concerns voiced in email by @nad :
@nad Yes, I think we can handle both concerns positively, but the model construction is not fully done yet.
To prove consistency of Agda --cubical-without-glue with postulated UIP, I think there is trivially the Set model, where:
- the interval is modelled as a singleton,
- path types are modelled as strict identity types (subsingletons inhabited iff both hands are equal),
- hcomp and transp are modelled essentially as identity functions.
Alternatively, I guess translation to XTT proves soundness as well.
The model construction referred to would apparently show that (postulated?) propositional extensionality and the K rule are fine (I'm not sure if that means just "consistent", or also "normalising", or something else). Has anyone worked this out in detail now?
Not that I'm aware of; disabling Glue would however amount to a system consistent with
postulate uip : forall {i} (X : Type i) -> isSet XI would say the other points you mention are an (a priori strictly) stronger request that can be considered in a further step.
I have a development where I use extensionality and the propositional truncation, some parts of the code use instances of univalence (introduced as assumptions), and some parts use instances of UIP (also introduced as assumptions). I think it would be nice if there was a variant of Cubical Agda that was consistent with UIP. What would this take? I imagine that it does not suffice to have a flag that disables the primitives and builtins related to univalence.