toy model for identifying a coherent subset of equalities, cf https://homotopytypetheory.org/2014/03/03/hott-should-eat-itself/#comment-198200

toy_coherent.v

Import EqNotations.

Inductive TY := BOOL | UNIT.
Definition tyInterp (t : TY) := match t with BOOL => bool | UNIT => unit end.
Inductive EQ : TY -> TY -> Type :=
| RFL {t} : EQ t t
| SYM {a b} : EQ a b -> EQ b a
| TRANS {a b c} : EQ a b -> EQ b c -> EQ a c
.
Fixpoint eqInterp {a b : TY} (p : EQ a b) : tyInterp a = tyInterp b
  := match p with
     | RFL => eq_refl
     | SYM p => eq_sym (eqInterp p)
     | TRANS p q => eq_trans (eqInterp p) (eqInterp q)
     end.
(* we need a strict / set-level structure of normal forms, where EQ implies equality here *)
Fixpoint EQ_inj {a b} (p : EQ a b) : a = b
  := match p with
     | RFL => eq_refl
     | SYM p => eq_sym (EQ_inj p)
     | TRANS p q => eq_trans (EQ_inj p) (EQ_inj q)
     end.
Scheme Equality for TY.
Lemma TY_eq_dec_refl {a} : TY_eq_dec a a = left eq_refl.
Proof. induction a; reflexivity. Qed.
Lemma TY_alleq {a b : TY} (p q : a = b) : p = q.
Proof.
  transitivity match TY_eq_dec a b with left r => r | right _ => p end; [ destruct p | destruct q ].
  all: rewrite TY_eq_dec_refl.
  all: reflexivity.
Qed.
Lemma TY_K {a : TY} (p : a = a) : p = eq_refl.
Proof. apply TY_alleq. Qed.
Lemma eqInterp_K' {a b p}
  : @eqInterp a b p = match TY_eq_dec a b with
                      | left p => f_equal tyInterp p
                      | right npf => match npf (EQ_inj p) with end
                      end.
Proof.
  induction p; cbn [eqInterp].
  { rewrite TY_eq_dec_refl; reflexivity. }
  { rewrite IHp; repeat destruct TY_eq_dec; subst.
    all: repeat match goal with H : _ = _ |- _ => pose proof (TY_K H); subst H end.
    all: try reflexivity.
    all: match goal with |- context[match ?e with end] => destruct e end. }
  { rewrite IHp1, IHp2.
    repeat destruct TY_eq_dec; subst.
    all: repeat match goal with H : _ = _ |- _ => pose proof (TY_K H); subst H end.
    all: try reflexivity.
    all: match goal with |- context[match ?e with end] => destruct e end. }
Qed.
Lemma eqInterp_K {a b p q} : @eqInterp a b p = @eqInterp a b q.
Proof.
  rewrite !eqInterp_K'; destruct TY_eq_dec; [ reflexivity | ].
  match goal with |- context[match ?e with end] => destruct e end.
Qed.