Do indices matter?

[SkySkimmer]

Why exactly does HoTT use -indices-matter?

[peterlefanulumsdaine]

Briefly, the effect of -indices-matter is to change how Coq calculates universe levels of inductive types/families, so that (among other things) it doesn’t put identity types automatically into Prop. So yes, for most HoTT-like purposes, they do matter.

In a little more detail: when calculating the universe level of a newly-defined inductive type/family, it should clearly be at least as large as the universe levels of the types of the arguments to its constructors. But there’s a non-obvious decision to make: should the levels of the types of the indices of an inductive family also be included?

[There’s a wrinkle here: you can choose to “squash” an inductive family down to a lower level than its calculated “natural” level — e.g. to Prop — but you then can’t eliminate out to types above the level you squashed to. So in the following I’m always talking about the calculated natural level.]

Coq’s default approach is to ignore the (levels of the types of) indices, and just check the (levels of types of) constructor arguments. In particular, this puts all identity types into the lowest universe Prop (which is special since it’s impredicative). This seems to correspond to how sizes look in classical models with UIP. It doesn’t quite imply UIP, as far as I know — since Coq doesn’t force types in Prop to be propositions in the HoTT sense — but it seems to go some way towards it, since we don’t have many (?any) homotopically non-trivial models of impredicative universes, and impredicativity implies at least some amount of Prop-like-ness (cf. Hurkens’ paradox). In particular, it’s not at all clear that this “indices don’t matter” approach is consistent with having a univalent universe containing any non-propositional types.

On the other hand, if you include the levels of indices in the calculation, you get something that seems to correspond to how sizes behave in the known homotopy-theoretic models, e.g. the simplicial model. In particular, Id A x y ends up living at the same universe level as A. So this seems to be what one wants for any HoTT development. Also this approach is the one that that should be translatable into something like Martin-Löf TT with à la Tarski universes closed under basic type formers (Π, Σ, 0, 1, +, W, Id).

All the above “…seems to correspond to…” haven’t been worked out properly anywhere on paper, as far as I know (unfortunately). Everything here comes from my memory of discussions around blackboards in the IAS in about Fall 2012, which were the background to the implementation of the -indices-matter option. If I’m misremembering anything, I hope others who were there at the time (especially @mattam82 ) will correct me :-)

[JasonGross]

HITs + UA + Id in Prop is inconsistent, right? Here's a sketch of the proof. (Has this been done before?) (Do we have the free group as a HIT formalized anywhere? Is the inject_injective property I admit below true and provable?)

Require Import Coq.Logic.Hurkens.

Module Import Free.
  Private Inductive free (A : Type) := base.

  Axiom inject : forall {A}, A -> base A = base A.
  Global Arguments base {_}, _.
End Free.

Definition bool := base = base :> free Prop.
Definition p2b : Prop -> bool := inject.
Definition b2p : bool -> Prop := fun b => forall P : Prop, b = inject P -> P.
Definition p2p1 : forall A : Prop, b2p (p2b A) -> A.
Proof.
  unfold b2p, p2b; intros A a.
  apply a; reflexivity.
Defined.
Lemma inject_injective : forall T (A B : T), inject A = inject B -> A = B.
Proof. (* requires UA, but should be provable *)
Admitted.
Definition p2p2 : forall A : Prop, A -> b2p (p2b A).
Proof.
  unfold b2p, p2b; intros A a P H.
  apply inject_injective in H; subst.
  assumption.
Defined.

Definition absurd : False := NoRetractFromSmallPropositionToProp.paradox bool p2b b2p p2p1 p2p2 False.

[mikeshulman]

Cute idea. The type you're using is equivalent to the suspension of Prop+1, so the fact that the 0-truncation of its identity types are the free group on Prop should follow from the van Kampen theorem (which is formalized in Agda, but not I think in Coq) -- Example 8.7.7 in the Book. It's an open question whether its identity types are already sets, but presumably that isn't necessary for your argument. However, I don't know whether we know constructively that every set maps injectively to its free group; it certainly seems like it should be true, but for sets without decidable equality there is no "reduced word" form for elements of the free group, so it's unclear to me how to proceed.

[SkySkimmer]

Briefly, the effect of -indices-matter is to change how Coq calculates universe levels of inductive types/families, so that (among other things) it doesn’t put identity types automatically into Prop. So yes, for most HoTT-like purposes, they do matter.

If it's just about Prop wouldn't some sort of -never-use-Prop option be more appropriate? ie is there a problem with having Id A x y in Type0 regardless of the universe of A?

[JasonGross]

@mikeshulman What about the weaker property forall T (A B : T), inject A = inject B -> ~~ (A = B).?

Require Import Coq.Logic.Hurkens.

Module Import Free.
  Private Inductive free (A : Type) := base.

  Axiom inject : forall {A}, A -> base A = base A.
  Global Arguments base {_}, _.
End Free.
Import NoRetractToNegativeProp.

Definition NFalse : NProp := exist (fun P => ~~P -> P) False (ltac:(tauto) : ~~False -> False).

Definition bool : NProp := exist (fun P => ~~P -> P) (base = base :> free Prop) (fun _ => eq_refl).
Definition p2b : NProp -> El bool := fun x => inject (proj1_sig x).
Definition b2p : El bool -> NProp.
Proof.
  intro b.
  exists (forall P : NProp, b = inject (El P) -> El P).
  intros f P H.
  apply (proj2_sig P).
  intro p; apply f; intro f'.
  apply p, f', H.
Defined.
Definition p2p1 : forall A : NProp, El (b2p (p2b A)) -> El A.
Proof.
  unfold b2p, p2b; intros A a.
  simpl @El in *.
  apply a; reflexivity.
Defined.
Lemma inject_injective : forall T (A B : T), inject A = inject B -> ~~ (A = B).
Proof. (* requires UA, but should be provable *)
Admitted.
Definition p2p2 : forall A : NProp, El A -> El (b2p (p2b A)).
Proof.
  unfold b2p, p2b; intros A a P H.
  apply inject_injective in H.
  apply (proj2_sig P).
  intro p; apply H; intro h; apply p.
  destruct P; simpl in *; subst; assumption.
Defined.

Definition bad : False := paradox bool p2b b2p p2p1 p2p2 NFalse.

[mikeshulman]

@SkySkimmer I'd be very surprised if it were consistent to have x=y in Type0 regardless of the type of A, since we can put arbitrarily "large" types into identity types with HITs and univalence. But I don't have a proof.

@JasonGross it seems like it should be true, but I still don't know how to go about proving it.

[JasonGross]

Following up on this, I believe I now have a proof sketch that UA + Id in impredicative Prop is inconsistent (without the need for HITs).

I expect that there should be a variant of Hurkens that operates on FiniteProp, i.e., { P : Prop & exists n, inhabited (P <~> Fin.t n) }. My intuition for this is that, in the presence of function extensionality, FiniteProp should be closed under forall (and it certainly has True and False).
Additionally, if we have UA + Id in Prop, then FiniteProp has the type Bool = Bool (which also has true (id) and false (negb) and is closed under (dependent) products. Then we can get a logical equivalence between FiniteProp and bool = bool (where bool = bool -> FiniteProp -> bool = bool is the identity and FiniteProp -> bool = bool -> FiniteProp collapses each FiniteProp to either True or False). This should satisfy the precondition of this variant of Hurkens.

Some WIP on a proof of this

Require Import Coq.Logic.Hurkens.
Require Import Coq.Logic.Decidable.
Require Import Coq.Vectors.Fin.
Import EqNotations.
Set Primitive Projections.
Set Implicit Arguments.
(** A typeclass that includes the data making [f] into an adjoint equivalence. *)
Class IsEquiv {A B : Type} (f : A -> B) := {
  equiv_inv : B -> A ;
  eisretr : forall x, f (equiv_inv x) = x ;
  eissect : forall x, equiv_inv (f x) = x ;
  eisadj : forall x : A, eisretr (f x) = f_equal f (eissect x) ;
}.

Arguments equiv_inv {A B}%type_scope f%function_scope {_} _.
Arguments eisretr {A B}%type_scope f%function_scope {_} _.
Arguments eissect {A B}%type_scope f%function_scope {_} _.
Arguments eisadj {A B}%type_scope f%function_scope {_} _.
Arguments IsEquiv {A B}%type_scope f%function_scope.

(** We mark [eisadj] as Opaque to deter Coq from unfolding it when simplifying. Since proofs of [eisadj] typically have larger proofs than the rest of the equivalence data, we gain some speed up as a result. *)
Global Opaque eisadj.

(** A record that includes all the data of an adjoint equivalence. *)
Record Equiv A B := {
  equiv_fun : A -> B ;
  equiv_isequiv : IsEquiv equiv_fun
}.

Coercion equiv_fun : Equiv >-> Funclass.
Coercion equiv_isequiv : Equiv >-> IsEquiv.

Global Existing Instance equiv_isequiv.

Arguments equiv_fun {A B} _ _.
Arguments equiv_isequiv {A B} _.

Bind Scope equiv_scope with Equiv.

Class finite (P : Prop) := isfinite : exists n : nat, inhabited (Equiv P (Fin.t n)).

Lemma finite_ind (Q : Prop -> Prop)
      (H0 : forall (P : Prop), Equiv P False -> Q P)
      (HS : forall (P : Prop) (p : P), finite { p' : P | p' <> p } -> (forall p' : P, p' = p \/ p' <> p) -> Q { p' : P | p' <> p } -> Q P)
      (P : Prop) (H : finite P)
 P.
Proof.
  destruct H as [n [[f H]] ].
  revert P f H; induction n as [|n IH]; intros; [ apply H0 | ].
  { unshelve econstructor.
    { intro p; pose proof (f p) as Hp; inversion Hp. }
    unshelve econstructor.
    all: try solve [ intro x; inversion x
                   | intro p; pose proof (f p) as Hp; inversion Hp ]. }
  { specialize (HS P).
    apply (HS (equiv_inv f F1)).
    { exists n; constructor.
      unshelve eexists.
      { intros [p' pf].
        pose proof (eissect f p') as Hgf.
        destruct H as [g gf fg adj]; cbn in *.
        generalize dependent (f p'); clear gf fg adj f IH.
        intro fp'.
        revert g pf.
        refine match fp' in Fin.t Sn
                     return match Sn return Fin.t Sn -> Set with
                            | O => fun _ => unit
                            | S n => fun fp' => forall g : Fin.t (S n) -> P, p' <> g F1 -> g fp' = p' -> Fin.t n
                            end fp'
               with
               | F1 => fun _ bad H => match bad (eq_sym H) with end
               | FS v => fun _ _ _ => v
               end. }
      { unshelve econstructor.
        { intro v. exists (equiv_inv f (FS v)). intro H'.
          apply (f_equal f) in H'.
          generalize (eq_trans (eq_sym (eisretr f _)) (eq_trans H' (eisretr f _))); clear.
          inversion 1. }
        all: cbn.
        2: { cbn
        { cbn.

          cut (FS v
        1-2: simple refine (fun v => exist (fun p' => p' <> equiv_inv f F1) (equiv_inv f (FS v)) _).

        1-2: intro H'; apply (f_equal
                                    return forall H : Equiv P (Fin.t (S n)), { p' : P | p' <> g H F1 }
                              with
                              | F1 => fun H => _
                              | FS v => fun H => _
                              end H).
        intros; subst.

        generalize dependent (g H); intros gH; intros.
      unshelve eexists (fun '(exist _ p' pf) => match H.(fwd) p' as fp' in Fin.t Sn
                                                      return H.(g) fp' = p' -> Fin.t (pred Sn) with
                                       | @F1 0 => _
                                       | @F1 (S _) => _
                                       | FS v => v
                                                end).
      cbv beta in *.

    {

#[export]
 Instance True_finite : finite True.
Proof.
  exists 1%nat; constructor.
  unshelve econstructor.
  { constructor. }
  { unshelve econstructor; try solve [ constructor ].
    { intros []; reflexivity. }
    { intro x.
      refine match x in Fin.t n return match n return Fin.t n -> Prop with
                                       | 1%nat => fun x => F1 = x
                                       | _ => fun _ => True
                                       end x with
             | @F1 0%nat => eq_refl
             | @FS n t => _
             | F0 => I
             end.
      destruct n; [ inversion t | constructor ]. } }
Qed.

#[export]
 Instance False_finite : finite False.
Proof.
  exists 0%nat.
  unshelve econstructor.
  unshelve econstructor.
  { inversion 1. }.
  unshelve econstructor.
  all: intro x; inversion x.
Qed.

#[export]
 Instance Forall_finite (Funext : forall (A : Prop) (B : A -> Prop) (f g : forall x : A, B x), (forall x, f x = g x) -> f = g)
 {P Q} {HP : finite P} {HQ : forall p : P, finite (Q p)} : finite (forall p : P, Q p).
Proof.
  destruct HP as [n [HP] ].
  revert dependent P; induction n as [|n IH]; intros.
  { exists 1%nat.
    unshelve econstructor.
    unshelve econstructor.
    { constructor. }
    unshelve econstructor.
    1,3: intros ? x; pose proof (HP.(fwd) x) as bad; exfalso; inversion bad.
    all: cbv.
    { intro x; apply Funext.
      intro p.
      pose proof (HP.(fwd) p) as bad; exfalso; inversion bad. }
    { { intro x.
      refine match x in Fin.t n return match n return Fin.t n -> Prop with
                                       | 1%nat => fun x => F1 = x
                                       | _ => fun _ => True
                                       end x with
             | @F1 0%nat => eq_refl
             | @FS n t => _
             | F0 => I
             end.
      destruct n; [ inversion t | constructor ]. } } }
  {
    2: {
    { inversion 1. }.

  all: intro x; inversion x.
Qed.



#[export]
 Instance Forall_finite {P Q} {HP : finite P} {HQ : forall p : P, finite (Q p)} : finite (forall p : P, Q p).
Proof.
  destruct HP as [n HP].
  destruct n as [|n].
  { destruct (HP (fun bad => match bad with end)) as [bad].
    inversion bad. }
  induction n as [|n IH].
  {
    case bad.
  exists 1%nat; intro f.
  destruct (f F1).
Qed.



Class subfinite (P : Prop) := is_subfinite : exists n, forall (f : Fin.t n -> P), exists n1 n2, n1 <> n2 /\ f n1 = f n2.
#[export]
 Instance True_subfinite : subfinite True.
Proof.
  exists 2%nat; intro f.
  exists F1.
  exists (FS F1).
  split; [ congruence | ].
  do 2 destruct f; reflexivity.
Qed.
#[export]
 Instance False_subfinite : subfinite False.
Proof.
  exists 1%nat; intro f.
  destruct (f F1).
Qed.
Existing Class decidable.

#[export]
 Instance True_decidable : decidable True.
Proof. solve [ constructor; constructor ]. Qed.
#[export]
 Instance False_decidable : decidable False.
Proof. intuition. Qed.

#[export]
 Instance Forall_subfinite_of_decidable {P Q} {HP : subfinite P} {HQ : forall p : P, subfinite (Q p)} : subfinite (forall p : P, Q p).
Proof.
  destruct HP as [n HP].
Record IsEquiv {A B} (f : A -> B) : Type :=
  { g : B -> A
  ; gf : forall x, g (f x) = x
  ; h : B -> A
  ; fh : forall x, f (h x) = x }.
Record Equiv A B := { fwd :> A -> B ; isequiv :> IsEquiv fwd }.
Definition idequiv {A} : Equiv A A
  := {| fwd := @id A
     ; isequiv := {| g := @id A ; gf := fun _ => eq_refl ; h := @id A ; fh := fun _ => eq_refl |} |}.
Definition idtoequiv {A B} (p : A = B) : Equiv A B
  := rew [Equiv A] p in idequiv.


#[export]
 Instance Forall_subfinite {P Q} {HP : subfinite P} {HQ : forall p : P, subfinite (Q p)} : subfinite (forall p : P, Q p).
Proof.
  destruct HP as [n HP].
  destruct n as [|n].
  { destruct (HP (fun bad => match bad with end)) as [bad].
    inversion bad. }
  induction n as [|n IH].
  {
    case bad.
  exists 1%nat; intro f.
  destruct (f F1).
Qed.


Section __.
  Context (Univalence : forall {A B}, IsEquiv (@idtoequiv A B)).

  Definition xorb_equiv (A : Prop) : Equiv Prop Prop.
    refine {| fwd P := (A -> ~P) /\ (~A -> P)
           ; isequiv := {| g P := (A -> ~P) /\ (~A -> P) ; h P := _ |} |}.
    intro P.
    apply (Univalence.(g)).
  unshelveeapply idtoequiv.

  Theorem absurd : False.
  Proof.
    unshelve eapply NoRetractFromSmallPropositionToProp.paradox.
    { exact (Prop = Prop). }
    { exact (fun P =>