Wrote some more on indexed h-propositions. Tried proving that the family Compare is an indexed h-prop, to no avail.