Add Pi types for iterative sets

Cubical/Data/Empty/Properties.agda

@@ -34,3 +34,11 @@ uninhabEquiv ¬a ¬b = isoToEquiv isom
   isom .inv b = rec (¬b b)
   isom .sec b = rec (¬b b)
   isom .ret a = rec (¬a a)
+
+uninhabEquiv⊥ : ∀ {ℓ} {A : Type ℓ}
+  → (A → ⊥) → A ≃ ⊥
+uninhabEquiv⊥ ¬a = uninhabEquiv ¬a (λ ())
+
+uninhabEquiv⊥* : ∀ {ℓ ℓ'} {A : Type ℓ}
+  → (A → ⊥) → A ≃ ⊥* {ℓ'}
+uninhabEquiv⊥* ¬a = uninhabEquiv ¬a (λ ())

Cubical/Data/IterativeSets/OrderedPair.agda

@@ -9,6 +9,7 @@ open import Cubical.Foundations.Prelude
 
 open import Cubical.Functions.Embedding
 open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.HLevels
 open import Cubical.Data.Sigma
@@ -40,33 +41,60 @@ private
                             (singleton⁰ (singleton⁰ y))
                             unorderedPair⁰≢singleton⁰
 
+orderedPair⁰≡orderedPair⁰ : {x y a b : V⁰ {ℓ}} → ((⟨ x , y ⟩⁰ ≡ ⟨ a , b ⟩⁰) ≃ ((x ≡ a) × (y ≡ b)))
+orderedPair⁰≡orderedPair⁰ {ℓ = ℓ} {x = x} {y = y} {a = a} {b = b} = compEquiv (compEquiv (compEquiv step₁ step₂) step₃) step₄
+  where
+    step₁ : (⟨ x , y ⟩⁰ ≡ ⟨ a , b ⟩⁰)
+            ≃
+            (unorderedPair⁰ (singleton⁰ x) empty⁰ singleton⁰≢empty⁰ ≡ unorderedPair⁰ (singleton⁰ a) empty⁰ singleton⁰≢empty⁰)
+            × (singleton⁰ (singleton⁰ y) ≡ singleton⁰ (singleton⁰ b))
+    step₁ = unorderedPair⁰≡unorderedPair⁰' {x = unorderedPair⁰ (singleton⁰ x) empty⁰ (singleton⁰≢empty⁰ {x = x})}
+                                           {y = singleton⁰ (singleton⁰ y)}
+                                           {a = unorderedPair⁰ (singleton⁰ a) empty⁰ (singleton⁰≢empty⁰ {x = a})}
+                                           {b = singleton⁰ (singleton⁰ b)}
+                                           {x≢y = unorderedPair⁰≢singleton⁰}
+                                           {a≢b = unorderedPair⁰≢singleton⁰}
+                                           unorderedPair⁰≢singleton⁰
+
+    step₂ : (unorderedPair⁰ (singleton⁰ x) empty⁰ singleton⁰≢empty⁰ ≡ unorderedPair⁰ (singleton⁰ a) empty⁰ singleton⁰≢empty⁰)
+            × (singleton⁰ (singleton⁰ y) ≡ singleton⁰ (singleton⁰ b))
+            ≃
+            (((singleton⁰ x ≡ singleton⁰ a) × (empty⁰ {ℓ} ≡ empty⁰))
+              × ((singleton⁰ y ≡ singleton⁰ b)))
+    step₂ = ≃-× (unorderedPair⁰≡unorderedPair⁰' {x = singleton⁰ x}
+                                                         {y = empty⁰}
+                                                         {a = singleton⁰ a}
+                                                         {b = empty⁰}
+                                                         {x≢y = singleton⁰≢empty⁰ {x = x}}
+                                                         {a≢b = singleton⁰≢empty⁰ {x = a}}
+                                                         (singleton⁰≢empty⁰ {x = x}))
+                (invEquiv (singleton⁰≡singleton⁰ {x = singleton⁰ y} {y = singleton⁰ b}))
+
+    step₃ : (((singleton⁰ x ≡ singleton⁰ a) × (empty⁰ {ℓ} ≡ empty⁰))
+              × ((singleton⁰ y ≡ singleton⁰ b)))
+            ≃
+            ((singleton⁰ x ≡ singleton⁰ a) × (singleton⁰ y ≡ singleton⁰ b))
+    step₃ = ≃-× (Σ-contractSnd (λ _ → inhProp→isContr refl (isSetV⁰ empty⁰ empty⁰)))
+                (idEquiv (singleton⁰ y ≡ singleton⁰ b))
+    step₄ : ((singleton⁰ x ≡ singleton⁰ a) × (singleton⁰ y ≡ singleton⁰ b))
+            ≃
+            ((x ≡ a) × (y ≡ b))
+    step₄ = ≃-× (invEquiv (singleton⁰≡singleton⁰ {x = x} {y = a}))
+                (invEquiv (singleton⁰≡singleton⁰ {x = y} {y = b}))
+
 orderedPair⁰ : (V⁰ {ℓ} × V⁰ {ℓ}) → V⁰ {ℓ}
 orderedPair⁰ = uncurry ⟨_,_⟩⁰
 
 isEmbOrderedPair⁰ : isEmbedding (orderedPair⁰ {ℓ})
-isEmbOrderedPair⁰ {ℓ} = injEmbedding isSetV⁰ inj
-    where
-        inj : {s t : V⁰ {ℓ} × V⁰ {ℓ}} → orderedPair⁰ s ≡ orderedPair⁰ t → s ≡ t
-        inj {s = x , y} {t = a , b} p = ΣPathP (helper (unorderedPair⁰≡unorderedPair⁰ .fst p))
-            where
-                x≡a-helper : ((singleton⁰ x ≡ singleton⁰ a) × (empty⁰ {ℓ} ≡ empty⁰ {ℓ}))
-                              ⊎ ((singleton⁰ x ≡ empty⁰) × (empty⁰ ≡ singleton⁰ a))
-                             → x ≡ a
-                x≡a-helper (inl (p , _)) = invEq singleton⁰≡singleton⁰ p
-                x≡a-helper (inr (p , _)) = ⊥-elim (singleton⁰≢empty⁰ p)
-                helper : ((unorderedPair⁰ (singleton⁰ x) empty⁰ singleton⁰≢empty⁰
-                               ≡ unorderedPair⁰ (singleton⁰ a) empty⁰ singleton⁰≢empty⁰)
-                             × (singleton⁰ (singleton⁰ y) ≡ singleton⁰ (singleton⁰ b)))
-                           ⊎ ((unorderedPair⁰ (singleton⁰ x) empty⁰ singleton⁰≢empty⁰ ≡ singleton⁰ (singleton⁰ b))
-                             × (singleton⁰ (singleton⁰ y) ≡ unorderedPair⁰ (singleton⁰ a) empty⁰ singleton⁰≢empty⁰))
-                          → ((x ≡ a) × (y ≡ b))
-                helper (inl (u , s)) .fst = x≡a-helper (unorderedPair⁰≡unorderedPair⁰ .fst u)
-                helper (inl (u , s)) .snd = invEq singleton⁰≡singleton⁰ (invEq singleton⁰≡singleton⁰ s)
-                helper (inr (p , _)) = ⊥-elim {A = λ _ → (x ≡ a) × (y ≡ b)} (unorderedPair⁰≢singleton⁰ p)
+isEmbOrderedPair⁰ s t = E .snd
+  where
+    F : ((s .fst ≡ t .fst) × (s .snd ≡ t .snd)) ≃ (orderedPair⁰ s ≡ orderedPair⁰ t)
+    F = propBiimpl→Equiv (isProp× (isSetV⁰ (s .fst) (t .fst))
+                                  (isSetV⁰ (s .snd) (t .snd)))
+                         (isSetV⁰ (orderedPair⁰ s) (orderedPair⁰ t))
+                         (λ P i → ⟨ P .fst i , P .snd i ⟩⁰)
+                         (orderedPair⁰≡orderedPair⁰ .fst)
+     -- invEquiv (orderedPair⁰≡orderedPair⁰ {x = s .fst} {y = s .snd} {a = t .fst} {b = t .snd})
 
-orderedPair⁰≡orderedPair⁰ : {x y a b : V⁰ {ℓ}} → ((⟨ x , y ⟩⁰ ≡ ⟨ a , b ⟩⁰) ≃ ((x ≡ a) × (y ≡ b)))
-orderedPair⁰≡orderedPair⁰ {x = x} {y = y} {a = a} {b = b} = propBiimpl→Equiv
-                                          (isSetV⁰ _ _)
-                                          (isProp× (isSetV⁰ _ _) (isSetV⁰ _ _))
-                                          (PathPΣ ∘ (isEmbedding→Inj isEmbOrderedPair⁰ (x , y) (a , b)))
-                                          (λ (x≡a , y≡b) → cong ⟨_, y ⟩⁰ x≡a ∙ cong ⟨ a ,_⟩⁰ y≡b)
+    E : (s ≡ t) ≃ (orderedPair⁰ s ≡ orderedPair⁰ t)
+    E = compEquiv (isoToEquiv (invIso (ΣPathPIsoPathPΣ {x = s} {y = t}))) F

Cubical/Data/IterativeSets/Pi.agda

@@ -0,0 +1,142 @@
+{-# OPTIONS --lossy-unification #-}
+
+module Cubical.Data.IterativeSets.Pi where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Function
+open import Cubical.Data.Sigma
+open import Cubical.Functions.Embedding
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Homotopy.Base
+open import Cubical.Foundations.Transport
+
+open import Cubical.Data.IterativeMultisets.Base renaming (index to index∞ ; elements to elements-V∞)
+open import Cubical.Data.IterativeSets.Base
+open import Cubical.Data.IterativeSets.OrderedPair
+
+private
+  module _ {ℓ ℓ' : Level} {A : Type ℓ} {B : Type ℓ'} (f : A → B) where
+    Inj : Type (ℓ-max ℓ ℓ')
+    Inj = {x y : A} → f x ≡ f y → x ≡ y
+
+module GraphElements {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ {ℓ} x → V⁰ {ℓ}} where
+  graphEl⁰ : ((a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)) → El⁰ x → V⁰ {ℓ}
+  graphEl⁰ Φ a = ⟨ elements x a , elements (y a) (Φ a) ⟩⁰
+
+  module FstConst (Φ : (a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)) where
+    -- this is the same as graphEl⁰
+    graphEl⁰' : El⁰ x → V⁰ {ℓ}
+    graphEl⁰' = graphEl⁰ Φ
+
+    inj : Inj graphEl⁰'
+    inj {a} {b} p = isEmbedding→Inj
+                      {A = El⁰ x} {B = V⁰ {ℓ}} {f = elements x}
+                      (isEmbedding-elements x) a b
+                        (fst (orderedPair⁰≡orderedPair⁰
+                          {x = elements x a} {y = elements (y a) (Φ a)}
+                          {a = elements x b} {b = elements (y b) (Φ b)} .fst p))
+
+    emb : isEmbedding graphEl⁰'
+    emb = injEmbedding {A = El⁰ x} {B = V⁰ {ℓ}} isSetV⁰ inj
+
+  graphEl⁰-inj' : (Φ Ψ : (a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)) (a : El⁰ x)
+                   → graphEl⁰ Φ ≡ graphEl⁰ Ψ → Φ a ≡ Ψ a
+  graphEl⁰-inj' Φ Ψ a p = isEmbedding→Inj {A = index (y a)} {B = V⁰}
+                                          (isEmbedding-elements (y a)) (Φ a) (Ψ a) els≡₂
+    where
+      p' : graphEl⁰ Φ a ≡ graphEl⁰ Ψ a
+      p' = funExt⁻ p a
+
+      els≡ : (elements x a ≡ elements x a) ×
+         (elements (y a) (Φ a) ≡ elements (y a) (Ψ a))
+      els≡ = orderedPair⁰≡orderedPair⁰ {x = elements x a} {y = elements (y a) (Φ a)}
+                                    {a = elements x a} {b = elements (y a) (Ψ a)} .fst p'
+      els≡₂ : elements (y a) (Φ a) ≡ elements (y a) (Ψ a)
+      els≡₂ = els≡ .snd
+
+  graphEl⁰-inj : Inj graphEl⁰
+  graphEl⁰-inj {Φ} {Ψ} p = funExt λ a → graphEl⁰-inj' Φ Ψ a p
+
+  graphEl⁰-emb : isEmbedding graphEl⁰
+  graphEl⁰-emb = injEmbedding {A = (a : El⁰ x) → El⁰ (y a)} {B = El⁰ x → V⁰} {f = graphEl⁰}
+                              (isSet→ {A' = V⁰ {ℓ}} {A = El⁰ {ℓ} x} (isSetV⁰ {ℓ})) graphEl⁰-inj
+
+module Graph {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ {ℓ} x → V⁰ {ℓ}} where
+  open GraphElements {ℓ} {x} {y}
+
+  graph⁰ : ((a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)) → V⁰ {ℓ}
+  graph⁰ Φ = fromEmb E
+    where
+      E : Embedding V⁰ ℓ
+      E .fst = El⁰ x
+      E .snd .fst = FstConst.graphEl⁰' Φ
+      E .snd .snd = FstConst.emb Φ
+
+  graph⁰-inj : Inj graph⁰
+  graph⁰-inj {Φ} {Ψ} p = graphEl⁰-inj P
+    where
+      F : ((z : V⁰) → z ∈⁰ graph⁰ Φ → z ∈⁰ graph⁰ Ψ)
+           × ((z : V⁰) → z ∈⁰ graph⁰ Ψ → z ∈⁰ graph⁰ Φ)
+      F = ≡V⁰-≃-≃V⁰ {x = graph⁰ Φ} {y = graph⁰ Ψ} .fst p
+
+      F₂ : (z : V⁰) → z ∈⁰ graph⁰ Ψ → z ∈⁰ graph⁰ Φ
+      F₂ = F .snd
+
+      module _ (a : El⁰ x) where
+        s : V⁰
+        s = graphEl⁰ Ψ a
+
+        s∈Ψ : s ∈⁰ graph⁰ Ψ
+        s∈Ψ .fst = a
+        s∈Ψ .snd = refl
+
+        s∈Φ : s ∈⁰ graph⁰ Φ
+        s∈Φ = F₂ s s∈Ψ
+
+        a' : El⁰ x
+        a' = s∈Φ .fst
+
+        graphEl⁰≡' : graphEl⁰ Φ a' ≡ graphEl⁰ Ψ a
+        graphEl⁰≡' = s∈Φ .snd
+
+        els≡ : elements x a' ≡ elements x a
+        els≡ = orderedPair⁰≡orderedPair⁰ {x = elements x a'} {y = elements (y a') (Φ a')}
+                                         {a = elements x a } {b = elements (y a)  (Ψ a) } .fst graphEl⁰≡' .fst
+
+        a'≡a : a' ≡ a
+        a'≡a = isEmbedding→Inj {A = El⁰ x} {B = V⁰ {ℓ}} {f = elements x}
+                (isEmbedding-elements x) a' a els≡
+
+        graphEl⁰≡ : graphEl⁰ Φ a ≡ graphEl⁰ Ψ a
+        graphEl⁰≡ = subst (λ m → graphEl⁰ Φ m ≡ graphEl⁰ Ψ a) a'≡a graphEl⁰≡'
+
+      P : graphEl⁰ Φ ≡ graphEl⁰ Ψ
+      P = funExt graphEl⁰≡
+
+  graph⁰-emb : isEmbedding graph⁰
+  graph⁰-emb = injEmbedding {A = (a : El⁰ x) → El⁰ (y a)} {B = V⁰} {f = graph⁰} (isSetV⁰ {ℓ}) graph⁰-inj
+
+private
+  variable
+    ℓ : Level
+    x : V⁰ {ℓ}
+    y : El⁰ x → V⁰ {ℓ}
+
+Π⁰ : (x : V⁰ {ℓ}) → (El⁰ x → V⁰ {ℓ}) → V⁰ {ℓ}
+Π⁰ {ℓ} x y = fromEmb E
+  where
+    E : Embedding V⁰ ℓ
+    E .fst = (a : El⁰ x) → El⁰ (y a)
+    E .snd .fst = Graph.graph⁰ {ℓ} {x} {y}
+    E .snd .snd = Graph.graph⁰-emb {ℓ} {x} {y}
+
+El⁰Π⁰isΠ : El⁰ (Π⁰ x y) ≡ ((a : El⁰ x) → El⁰ (y a))
+El⁰Π⁰isΠ = refl
+
+_→⁰_ : V⁰ {ℓ} → V⁰ {ℓ} → V⁰ {ℓ}
+x →⁰ y = Π⁰ x (λ _ → y)
+
+El⁰→⁰is→ : {x y : V⁰ {ℓ}} → El⁰ (x →⁰ y) ≡ (El⁰ x → El⁰ y)
+El⁰→⁰is→ = refl