Added Unordered Pair

Cubical/HITs/UnorderedPair.agda

@@ -0,0 +1,5 @@
+{-# OPTIONS --safe #-}
+module Cubical.HITs.UnorderedPair where
+
+open import Cubical.HITs.UnorderedPair.Base public
+open import Cubical.HITs.UnorderedPair.Properties public

Cubical/HITs/UnorderedPair/Base.agda

@@ -0,0 +1,41 @@
+{-# OPTIONS --safe #-}
+module Cubical.HITs.UnorderedPair.Base where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+
+private variable
+  ℓ ℓ′ : Level
+  A : Type ℓ
+
+infixr 4 _,_
+
+data UnorderedPair (A : Type ℓ) : Type ℓ where
+  _,_ : (x y : A) → UnorderedPair A
+  swap : (x y : A) → (x , y) ≡ (y , x)
+  trunc : isSet (UnorderedPair A)
+
+module _ {B : UnorderedPair A → Type ℓ′}
+  (_,*_ : (x y : A) → B (x , y))
+  (swap* : (x y : A) → PathP (λ i → B (swap x y i)) (x ,* y) (y ,* x))
+  (trunc* : (xs : UnorderedPair A) → isSet (B xs)) where
+
+  elim : (xs : UnorderedPair A) → B xs
+  elim (x , y) = x ,* y
+  elim (swap x y i) = swap* x y i
+  elim (trunc x y p q i j) =
+    isOfHLevel→isOfHLevelDep 2 trunc* (elim x) (elim y) (cong elim p) (cong elim q) (trunc x y p q) i j
+
+module _ {B : UnorderedPair A → Type ℓ′}
+  (BProp : {xs : UnorderedPair A} → isProp (B xs))
+  (_,*_ : (x y : A) → B (x , y)) where
+
+  elimProp : (xs : UnorderedPair A) → B xs
+  elimProp = elim _,*_ (λ x y → toPathP (BProp (transport (λ i → B (swap x y i)) (x ,* y)) (y ,* x)))
+    λ _ → isProp→isSet BProp
+
+module _ {B : Type ℓ′} (BType : isSet B)
+  (_,*_ : (x y : A) → B) (swap* : (x y : A) → (x ,* y) ≡ (y ,* x)) where
+
+  rec : UnorderedPair A → B
+  rec = elim _,*_ swap* λ _ → BType

Cubical/HITs/UnorderedPair/Properties.agda

@@ -0,0 +1,40 @@
+{-# OPTIONS --safe #-}
+module Cubical.HITs.UnorderedPair.Properties where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Data.Sigma
+open import Cubical.HITs.SetCoequalizer as SQ
+
+open import Cubical.HITs.UnorderedPair.Base as UP
+
+open Iso
+
+private variable
+  ℓ : Level
+  A : Type ℓ
+
+SetCoequalizerPair : Type ℓ → Type ℓ
+SetCoequalizerPair A = SetCoequalizer (idfun (A × A)) (λ (a , b) → b , a)
+
+SetCoeq→UPair : SetCoequalizerPair A → UnorderedPair A
+SetCoeq→UPair = SQ.rec trunc (uncurry _,_) (uncurry swap)
+
+UPair→SetCoeq : UnorderedPair A → SetCoequalizerPair A
+UPair→SetCoeq = UP.rec squash (curry inc) (curry coeq)
+
+SetCoeq→UPair→SetCoeq : (xs : UnorderedPair A) → SetCoeq→UPair (UPair→SetCoeq xs) ≡ xs
+SetCoeq→UPair→SetCoeq = UP.elimProp (trunc _ _) λ _ _ → refl
+
+UPair→SetCoeq→SetCoeq : (xs : SetCoequalizerPair A) → UPair→SetCoeq (SetCoeq→UPair xs) ≡ xs
+UPair→SetCoeq→SetCoeq = SQ.elimProp (λ _ → squash _ _) λ _ → refl
+
+SetCoeqIsoUPair : Iso (SetCoequalizerPair A) (UnorderedPair A)
+fun SetCoeqIsoUPair = SetCoeq→UPair
+inv SetCoeqIsoUPair = UPair→SetCoeq
+rightInv SetCoeqIsoUPair = SetCoeq→UPair→SetCoeq
+leftInv SetCoeqIsoUPair = UPair→SetCoeq→SetCoeq
+
+SetCoeq≡UPair : SetCoequalizerPair A ≡ UnorderedPair A
+SetCoeq≡UPair = isoToPath SetCoeqIsoUPair