Equivalence on UnordPair

[iacore]

https://github.com/HigherOrderCO/Kind1/blob/master/blog/1-beyond-inductive-datatypes.md#possibility-3-higher-inductive-types

I saw the call for answer here:

UPair(A: Type): Type
  self(P: UPair(A) -> Type) ->
  (make: (a: A) -> (b: A) -> P(UPair.make(A, a,b))) ->
  (swap: (a: A) -> (b: A) -> Equal(_, make(a,b), make(b,a))) ->
  P(self)

UPair.make(A: Type, a: A, b: A): UPair(A)
  (P, make, swap) make(a, b)

What happens if you use equivalence class here, not Equal?

[iacore]

Two other ideas regarding self types.

3-state time crystal thing

Having 3 self types (selfX, selfY, selfZ) that circulate irregularly.

for example, having the decimal digits of pi in ternary decide which one to prove next.

Important: it's irregular yet deterministic.

Let's say you have a sequence like this Y Z X Z Z Y Z Z Y Y Y Z ...

kind of like how having three different UPair called UPairX UPairY UPairZ that refers to each other (like how Path and I refers to each other), but the pattern is irregular.

can't prove stuff like true = false in this one due to the irregularity

Immediate past

It's kind of like type universe, yet infinite.

Similar idea as above.

UPair0 refers to UPair1 refers to UPair2

Maybe possible to prove stuff about UPair u in UPair (u + 1)

it is consistent; not sure about the usefulness of this one

---

sighs, incompleteness is hard