Trying to unnest the "pathological" example of an inductive type that nests with an indexed family, here equality (compiles with coq 8.16, equations 1.3)

unnestingEq.v

(** Trying to unnest the "pathological" example of an inductive type
 that nests with an indexed family, here equality *)

Inductive I := K : forall x : I, x = x -> I.


(* A more general induction principle for I than what Coq generates *)
Section GeneralElim.

Definition J {A : Type} (x : A) (P : forall (y : A) (e : x = y), Type)
             (hr : P x eq_refl) (y : A) (e : x = y) : P y e :=
  match e with
  | eq_refl => hr
  end.

Context (P : I -> Type)
  (Q : forall x y : I, x = y -> Type)
  (hK : forall x : I, P x -> forall e : x = x, Q x x e -> P (K x e))
  (heq_refl : forall x : I, P x -> Q x x eq_refl).

Fixpoint Ielim (i : I) : P i := 
  match i as i0 return (P i0) with
  | K x e => hK x (Ielim x) e (J x (Q x) (heq_refl x (Ielim x)) x e)
  end.
End GeneralElim.

(** Un-nesting the instance of equality in I would naively give
 rise to the following inductive-inductive definition that
 is not accepted by Coq (no support for induction-induction *)

(* Inductive I := K : forall (x : I), E x x -> I *)
(* with E : I -> I -> Type := erefl : forall (x : I), E x x  *)

(** Instead we apply the technique of
  Kaposi, Ambrus ; Kovács, András ; Lafont, Ambroise
  For Finitary Induction-Induction, Induction Is Enough
  https://drops.dagstuhl.de/opus/volltexte/2020/13070/

and first define the underlying carrier type that we refine later with the correct indexing discipline
 *)
Inductive I0 := K0 : I0 -> E0 -> I0
with E0 := e0 : I0 -> E0.

Scheme I0_rectp := Induction for I0 Sort Type with
E0_rectp := Induction for E0 Sort Type.

Combined Scheme I0_E0_rect from I0_rectp, E0_rectp.

(** We will need the fact that the carrier is an hSet to obtain that the
    refinement layer is indeed an hProp and derive the induction principle at
    the end *)
From Equations Require Import Equations.
Derive NoConfusion for I0 E0.

Definition uip_at {A} (x : A) := forall (y : A) (e e' : x = y), e = e'.

Lemma I0_E0_eqdec : UIP I0 * UIP E0.
Proof.
  apply I0_E0_rect.
  + intros; noconf e1; noconf e'.
    now rewrite (H i e' eq_refl), (H0 e e1 eq_refl).
  + intros; noconf e; noconf e'. now rewrite (H i H0 eq_refl).
Qed.

#[global]
Instance: UIP I0 := fst I0_E0_eqdec.
#[global]
Instance: UIP E0 := snd I0_E0_eqdec.

(** Refinement layer, v stands for "valid" *)

Fixpoint vI0 (x : I0) : Prop :=
  match x with
  | K0 x e => vI0 x /\ vE0 e x x
  end
with vE0 (e : E0) (x y : I0) : Prop :=
  match e with
  | e0 x0 => vI0 x0 /\ x0 = x /\ x0 = y
  end.

Definition pirr (P : Prop) := forall x y : P, x = y.

Lemma vI0_E0_pirr : (forall x, pirr (vI0 x)) * (forall e x y, pirr (vE0 e x y)).
Proof.
  apply I0_E0_rect.
  + intros i hi e he [? ?] [? ?]; f_equal; [apply hi| apply he].
  + intros i hi x y [? [? ?]] [? [? ?]]; f_equal; [apply hi|f_equal; apply uip].
Qed.


(** Packing the carrier together with the refinement
    We also get the expected introduction forms *)
Import Sigma_Notations.

Definition I1 := Σ x : I0, vI0 x.
Definition E1 (x y : I1) := Σ e : E0, vE0 e x.1 y.1.

#[program]
Definition K1 (x : I1) (e : E1 x x) : I1 := (K0 x.1 e.1 , _).
Next Obligation.
  split; [exact x.2 | exact e.2].
Defined.

#[program]
Definition e1 (x : I1) : E1 x x := (e0 x.1, _).
Next Obligation.
  split; [exact x.2| split; reflexivity].
Defined.

(** And the same eliminator on I1 as I, and E1 as (eq I) *)

Section GeneralElim1.
Context (P : I1 -> Type)
  (Q : forall x y : I1, E1 x y -> Type)
  (hK : forall x : I1, P x -> forall e : E1 x x, Q x x e -> P (K1 x e))
  (he : forall x : I1, P x -> Q x x (e1 x)).

Fixpoint Ielim01 (i : I0) : forall (vi : vI0 i), P (i, vi)
with Eelim01 (e : E0) : forall (x y : I0) vx vy (ve : vE0 e x y), Q (x, vx) (y, vy) (e, ve).
Proof.
  + refine (
        match i as i0 return forall (vi : vI0 i0), (P (i0, vi)) with
        | K0 x e => fun vi => _
        end).
    destruct vi.
    refine (hK (x, _) (Ielim01 x _) (e, _) (Eelim01 e _ _ _ _ _)).
  + refine (
        match e as e0 return forall (y z : I0) vy vz (ve : vE0 e0 y z), Q (y, vy) (z, vz) (e0, ve) with
        | e0 x => fun y z vy vz ve => _
        end).
    destruct ve as [h [<- <-]].
    assert (vy = h) as -> by apply (fst vI0_E0_pirr).
    assert (vz = h) as -> by apply (fst vI0_E0_pirr).
    apply (he (x, _) (Ielim01 x _)).
Defined.

Definition I1elim (i : I1) : P i := Ielim01 i.1 i.2.
Definition E1elim {x y} (e : E1 x y) : Q x y e := Eelim01 e.1 x.1 y.1 x.2 y.2 e.2. 

End GeneralElim1.