Added Unordered Pair

[guilhermehas]

I created Unordered Pair, which means that a , b = b , a.

[felixwellen]

Did you see the finite multisets: https://github.com/agda/cubical/blob/master/Cubical/HITs/FiniteMultiset/Base.agda ?
Unordered pairs are a special case and I think it would be better to define them as such, if you really have a use case specifically for pairs. Do you know the relation to that and
https://github.com/agda/cubical/blob/master/Cubical/HITs/ListedFiniteSet/Base.agda ?

[guilhermehas]

Yes, I know the relation. I will try to put in the properties.
For example, in Agda Stdlib (https://github.com/agda/agda-stdlib/blob/master/src/Data/Vec/Recursive.agda), they defined Vec using Product. So maybe it is possible to define a FiniteMultiset using this Unordered Pair with the same idea.

[felixwellen]

Only a renaming request...

[felixwellen]

Yes, I know the relation. I will try to put in the properties. For example, in Agda Stdlib (https://github.com/agda/agda-stdlib/blob/master/src/Data/Vec/Recursive.agda), they defined Vec using Product. So maybe it is possible to define a FiniteMultiset using this Unordered Pair with the same idea.

Maybe you can add a comment? Something like "the relation to ... should be ...".

[guilhermehas]

I was trying to define the recursive definition:

FMSet : (A : Type ℓ) (n : ℕ) → Type ℓ
FMSet A 0 = Unit*
FMSet A 1 = A
FMSet A (suc (suc n)) = {!!}

And I figured out that it is not possible to do, because both elements need to be of the same type.

Yes, I know the relation. I will try to put in the properties. For example, in Agda Stdlib (https://github.com/agda/agda-stdlib/blob/master/src/Data/Vec/Recursive.agda), they defined Vec using Product. So maybe it is possible to define a FiniteMultiset using this Unordered Pair with the same idea.

Maybe you can add a comment? Something like "the relation to ... should be ...".

Because of that, what I commented before was wrong.

[guilhermehas]

I figured out how to do:

addN : UnorderedPair (A × ℕ) → ℕ
addN = rec isSetℕ (λ x y → proj₂ x + proj₂ y) λ x y → +-comm (proj₂ x) (proj₂ y)

data FMSet (A : Type ℓ) : ℕ → Type ℓ where
  one : A → FMSet A 1
  join : (xs : UnorderedPair (A × ℕ)) → FMSet A (addN xs)

[plt-amy]

Since this construction is limited to the sets, wouldn't it be cleaner to implement it by a set-coequalizer? Consider the coequalizer of swap, id : A × A -> A × A, for example

[guilhermehas]

Since this construction is limited to the sets, wouldn't it be cleaner to implement it by a set-coequalizer? Consider the coequalizer of swap, id : A × A -> A × A, for example

Thanks for your suggestion. I proved that both are isomorphic.

[felixwellen]

As I just learned in the hallway, there is also an untruncated unordered pair notion, defined as maps from a set merely equivalent to Fin 2 to A. I guess for A a Set the Set-truncation of that notion should agree with your notion?

[guilhermehas]

As I just learned in the hallway, there is also an untruncated unordered pair notion, defined as maps from a set merely equivalent to Fin 2 to A. I guess for A a Set the Set-truncation of that notion should agree with your notion?

I didn't understand. Can you give a code example?

[plt-amy]

Let A be a type (of arbitrary h-level). We define the type of unordered pairs with coordinates in A as the type

Σ[ X ∈ Type ] (∥ X ≃ Bool ∥ × X → A)

This construction is at least a groupoid, but for A of h-level ≥ 3, it preserves h-levels. The idea is that, in the same way that a pair in A is the same as a function Bool→A, we can take away the ordering by allowing pairs to choose their own index types up to a mere equivalence; consumers of unordered pairs can't inspect the underlying type, and all they know is that it has two elements.

The pairing {x,y} is defined to be

Bool , inc id , λ { true → x; false → y }

This is equal to the pairing {y,x} because the type of identifications between unordered pairs is given by equivalences of their underlying types which commute with the projection function.

[guilhermehas]

Bool , inc id , λ { true → x; false → y }

This is equal to the pairing {y,x} because the type of identifications between unordered pairs is given by equivalences of their underlying types which commute with the projection function.

I am trying to do your implementation, but I am in trouble. What am I doing wrong?

UPairBool : Type ℓ → Type _
UPairBool A = Σ[ X ∈ Type ] (∥ X ≃ Bool ∥₁ × (X → A))

private
  uP₁ : UPairBool Bool
  uP₁ = Bool , ∣ idEquiv Bool ∣₁ , λ where false → false ; true → true

  uP₂ : UPairBool Bool
  uP₂ = Bool , ∣ notEquiv ∣₁ , λ where false → true ; true → false

  uP₁≡uP₂ : uP₁ ≡ uP₂
  uP₁≡uP₂ i = Bool , squash₁ ∣ idEquiv Bool ∣₁ ∣ notEquiv ∣₁ i  , {!!}

[felixwellen]

I am trying to do your implementation, but I am in trouble. What am I doing wrong?

What you are trying to prove is true. The first part of your term uP₁≡uP₂ should not be constantly Bool, but come from the not equivalence.

[plt-amy]

Also, isn't that the set-truncation? The equivalence has to be propositionally-truncated.

[felixwellen]

∥_∥₁ is propositional truncation.

[guilhermehas]

I am in trouble trying to prove this thing:

uP₁≡uP₂ : uP₁ ≡ uP₂
uP₁≡uP₂ = ΣPathP (notEq , ΣPathP (helper₁ , helper₂)) where
  helper₁ : PathP (λ z → ∥ notEq z ≃ Bool ∥₁) ∣ idEquiv Bool ∣₁ ∣ notEquiv ∣₁
  helper₁ i = {!squash₁ ∣ idEquiv Bool ∣₁ ∣ notEquiv ∣₁ i!}

  helper₂ : PathP (λ i → notEq i → Bool) (idfun Bool) not
  helper₂ i b = {!!}

[felixwellen]

You can, of course, also postpone the proof and wrap up the current PR...

[felixwellen]

I have a couple of comments and questions.

[felixwellen]

Sorry for the long wait and thanks for the updates. I am a bit puzzled about the recursive FMSets - maybe it is better to save those for a PR where you prove something about them? All the other files look good to me.

[guilhermehas]

I deleted the recursive file.

[felixwellen]

Thanks - will merge it now...