From c51e6ac61a66c366d84ac594548101d1db4fa4f0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fabian=20Lukas=20Grubm=C3=BCller?= Date: Wed, 29 Apr 2026 17:07:15 +0200 Subject: [PATCH 01/11] Add (non-terminating) Pi type codes for iterative sets --- Cubical/Data/IterativeSets/Pi.agda | 135 +++++++++++++++++++++++++++++ 1 file changed, 135 insertions(+) create mode 100644 Cubical/Data/IterativeSets/Pi.agda diff --git a/Cubical/Data/IterativeSets/Pi.agda b/Cubical/Data/IterativeSets/Pi.agda new file mode 100644 index 0000000000..18d46ee0ac --- /dev/null +++ b/Cubical/Data/IterativeSets/Pi.agda @@ -0,0 +1,135 @@ +{-# OPTIONS --lossy-unification #-} + +-- TODO: make type checking terminate + +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 (overline to overline-V∞ ; tilde to tilde-V∞) +open import Cubical.Data.IterativeSets.Base +open import Cubical.Data.IterativeSets.OrderedPair + +private + variable + ℓ : Level + x : V⁰ {ℓ} + y : El⁰ x → V⁰ {ℓ} + +private + module _ {ℓ ℓ' : Level} {A : Type ℓ} {B : Type ℓ'} (f : A → B) where + Inj : Type (ℓ-max ℓ ℓ') + Inj = {x y : A} → f x ≡ f y → x ≡ y + +private + module _ {ℓA ℓA' ℓB : Level} {A : Type ℓA} {A' : Type ℓA'} {B : A' → Type ℓB} (f : A → A') (g : (x : A) → B (f x)) where + Σfun : A → Σ A' B + Σfun x .fst = f x + Σfun x .snd = g x + + InjFstInj : Inj f → Inj Σfun + InjFstInj injf p = injf (cong fst p) + +private + module _ {ℓA ℓA' ℓB ℓB' : Level} {A : Type ℓA} {A' : Type ℓA'} {B : A → Type ℓB} {B' : A' → Type ℓB'} (setA' : isSet A') (f : A → A') (g : (x : A) → B x → B' (f x)) where + Σfun' : Σ A B → Σ A' B' + Σfun' pair .fst = f (pair .fst) + Σfun' pair .snd = uncurry g pair + + InjΣInj : Inj f → ((x : A) → Inj (g x)) → Inj Σfun' + InjΣInj injf injg {a , b} {c , d} p = ΣPathTransport→PathΣ (a , b) (c , d) (q1 , q2) + where + s : Σ[ p1 ∈ f a ≡ f c ] subst B' p1 (g a b) ≡ g c d + s = PathΣ→ΣPathTransport _ _ p + + q1 : a ≡ c + q1 = injf (s .fst) + + p1' : f a ≡ f c + p1' = cong f q1 + + s1≡p1' : (s .fst) ≡ (cong f q1) + s1≡p1' = setA' (f a) (f c) (s .fst) (cong f q1) + + p1'≡s1 : (cong f q1) ≡ s .fst + p1'≡s1 = setA' (f a) (f c) (cong f q1) (s .fst) + + α : subst (λ z → B' (f z)) q1 (g a b) ≡ g c (subst B q1 b) + α = substCommSlice (λ z → B z) (λ z → B' (f z)) g (injf (s .fst)) b + + β : subst (λ z → B' (f z)) q1 (g a b) ≡ subst B' (s .fst) (g a b) + β = cong (λ m → subst B' m (g a b)) p1'≡s1 + + p2 : g c (subst B q1 b) ≡ g c d + p2 = sym α ∙ β ∙ s .snd + + q2 : subst B q1 b ≡ d + q2 = injg c p2 + +graph⁰ : ((a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)) → V⁰ {ℓ} +graph⁰ {ℓ = ℓ} {x = x} {y = y} f = fromEmb E + where + E : Embedding (V⁰ {ℓ}) ℓ + E .fst = El⁰ x + E .snd .fst a = orderedPair⁰ (tilde x a , tilde (y a) (f a)) + E .snd .snd = injEmbedding isSetV⁰ (λ {v} {w} p → isEmbedding→Inj {f = tilde x} (isEmbedding-tilde x) v w (orderedPair⁰≡orderedPair⁰ .fst p .fst)) + +Π⁰ : (x : V⁰ {ℓ}) → ((a : El⁰ x) → V⁰ {ℓ}) → V⁰ {ℓ} +Π⁰ {ℓ} x y = fromEmb E + where + In : {f g : (a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)} → graph⁰ {x = x} {y = y} f ≡ graph⁰ {x = x} {y = y} g → (a : El⁰ x) → f a ≡ g a + In {f} {g} p a = + let + ∈⁰graph⁰-f→g : ((z : V⁰) → z ∈⁰ graph⁰ f → z ∈⁰ graph⁰ g) + ∈⁰graph⁰-f→g = ≡V⁰-≃-≃V⁰ .fst p .fst + + p : Σ[ a' ∈ El⁰ x ] orderedPair⁰ ((tilde x a') , (tilde (y a') (g a'))) ≡ orderedPair⁰ ((tilde x a) , (tilde (y a) (f a))) + p = ∈⁰graph⁰-f→g (orderedPair⁰ ((tilde x a) , (tilde (y a) (f a)))) (a , refl) + + a' : El⁰ x + a' = p .fst + + p₂ : orderedPair⁰ ((tilde x a') , (tilde (y a') (g a'))) ≡ orderedPair⁰ ((tilde x a) , (tilde (y a) (f a))) + p₂ = p .snd + + q : tilde x a' ≡ tilde x a + q = orderedPair⁰≡orderedPair⁰ .fst p₂ .fst + + r : a' ≡ a + r = isEmbedding→Inj {f = tilde x} (isEmbedding-tilde x) a' a q + + s : tilde (y a') (g a') ≡ tilde (y a) (f a) + s = orderedPair⁰≡orderedPair⁰ .fst p₂ .snd + + t : tilde (y a) (g a) ≡ tilde (y a') (g a') + t i = tilde (y (r (~ i))) (g (r (~ i))) + + goal : f a ≡ g a + goal = isEmbedding→Inj {f = tilde (y a)} (isEmbedding-tilde (y a)) (f a) (g a) (sym (t ∙ s)) + in goal + + + In' : {f g : (a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)} → graph⁰ {x = x} {y = y} f ≡ graph⁰ {x = x} {y = y} g → f ≡ g + In' p = funExt (In p) + + E : Embedding (V⁰ {ℓ}) ℓ + E .fst = (a : El⁰ x) → El⁰ (y a) + E .snd .fst f = graph⁰ {x = x} {y = y} f + E .snd .snd = injEmbedding isSetV⁰ In' + +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 From 683551989050bdc661bfd1b2d7b1720752ff06c3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fabian=20Lukas=20Grubm=C3=BCller?= Date: Wed, 29 Apr 2026 17:29:18 +0200 Subject: [PATCH 02/11] Rename `overline` to `index` and `tilde` to `elements` (to reflect upstream change) --- Cubical/Data/IterativeSets/Pi.agda | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/Cubical/Data/IterativeSets/Pi.agda b/Cubical/Data/IterativeSets/Pi.agda index 18d46ee0ac..f1999dfbc9 100644 --- a/Cubical/Data/IterativeSets/Pi.agda +++ b/Cubical/Data/IterativeSets/Pi.agda @@ -14,7 +14,7 @@ open import Cubical.Foundations.Isomorphism open import Cubical.Homotopy.Base open import Cubical.Foundations.Transport -open import Cubical.Data.IterativeMultisets.Base renaming (overline to overline-V∞ ; tilde to tilde-V∞) +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 @@ -79,8 +79,8 @@ graph⁰ {ℓ = ℓ} {x = x} {y = y} f = fromEmb E where E : Embedding (V⁰ {ℓ}) ℓ E .fst = El⁰ x - E .snd .fst a = orderedPair⁰ (tilde x a , tilde (y a) (f a)) - E .snd .snd = injEmbedding isSetV⁰ (λ {v} {w} p → isEmbedding→Inj {f = tilde x} (isEmbedding-tilde x) v w (orderedPair⁰≡orderedPair⁰ .fst p .fst)) + E .snd .fst a = orderedPair⁰ (elements x a , elements (y a) (f a)) + E .snd .snd = injEmbedding isSetV⁰ (λ {v} {w} p → isEmbedding→Inj {f = elements x} (isEmbedding-elements x) v w (orderedPair⁰≡orderedPair⁰ .fst p .fst)) Π⁰ : (x : V⁰ {ℓ}) → ((a : El⁰ x) → V⁰ {ℓ}) → V⁰ {ℓ} Π⁰ {ℓ} x y = fromEmb E @@ -91,29 +91,29 @@ graph⁰ {ℓ = ℓ} {x = x} {y = y} f = fromEmb E ∈⁰graph⁰-f→g : ((z : V⁰) → z ∈⁰ graph⁰ f → z ∈⁰ graph⁰ g) ∈⁰graph⁰-f→g = ≡V⁰-≃-≃V⁰ .fst p .fst - p : Σ[ a' ∈ El⁰ x ] orderedPair⁰ ((tilde x a') , (tilde (y a') (g a'))) ≡ orderedPair⁰ ((tilde x a) , (tilde (y a) (f a))) - p = ∈⁰graph⁰-f→g (orderedPair⁰ ((tilde x a) , (tilde (y a) (f a)))) (a , refl) + p : Σ[ a' ∈ El⁰ x ] orderedPair⁰ ((elements x a') , (elements (y a') (g a'))) ≡ orderedPair⁰ ((elements x a) , (elements (y a) (f a))) + p = ∈⁰graph⁰-f→g (orderedPair⁰ ((elements x a) , (elements (y a) (f a)))) (a , refl) a' : El⁰ x a' = p .fst - p₂ : orderedPair⁰ ((tilde x a') , (tilde (y a') (g a'))) ≡ orderedPair⁰ ((tilde x a) , (tilde (y a) (f a))) + p₂ : orderedPair⁰ ((elements x a') , (elements (y a') (g a'))) ≡ orderedPair⁰ ((elements x a) , (elements (y a) (f a))) p₂ = p .snd - q : tilde x a' ≡ tilde x a + q : elements x a' ≡ elements x a q = orderedPair⁰≡orderedPair⁰ .fst p₂ .fst r : a' ≡ a - r = isEmbedding→Inj {f = tilde x} (isEmbedding-tilde x) a' a q + r = isEmbedding→Inj {f = elements x} (isEmbedding-elements x) a' a q - s : tilde (y a') (g a') ≡ tilde (y a) (f a) + s : elements (y a') (g a') ≡ elements (y a) (f a) s = orderedPair⁰≡orderedPair⁰ .fst p₂ .snd - t : tilde (y a) (g a) ≡ tilde (y a') (g a') - t i = tilde (y (r (~ i))) (g (r (~ i))) + t : elements (y a) (g a) ≡ elements (y a') (g a') + t i = elements (y (r (~ i))) (g (r (~ i))) goal : f a ≡ g a - goal = isEmbedding→Inj {f = tilde (y a)} (isEmbedding-tilde (y a)) (f a) (g a) (sym (t ∙ s)) + goal = isEmbedding→Inj {f = elements (y a)} (isEmbedding-elements (y a)) (f a) (g a) (sym (t ∙ s)) in goal From aac23f0b1d13c3a0f58e4119595656c730fe02b2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fabian=20Lukas=20Grubm=C3=BCller?= Date: Wed, 29 Apr 2026 17:36:32 +0200 Subject: [PATCH 03/11] Add illegal whitespace to fail check and prevent CI from running non-terminating code --- Cubical/Data/IterativeSets/Pi.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cubical/Data/IterativeSets/Pi.agda b/Cubical/Data/IterativeSets/Pi.agda index f1999dfbc9..26abbbfb53 100644 --- a/Cubical/Data/IterativeSets/Pi.agda +++ b/Cubical/Data/IterativeSets/Pi.agda @@ -1,7 +1,7 @@ {-# OPTIONS --lossy-unification #-} -- TODO: make type checking terminate - + module Cubical.Data.IterativeSets.Pi where open import Cubical.Foundations.Prelude From aa00420a2f46e59e4d154df4d239a18974cfd1dc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fabian=20Lukas=20Grubm=C3=BCller?= Date: Tue, 12 May 2026 12:17:22 +0200 Subject: [PATCH 04/11] =?UTF-8?q?Improve=20performance=20of=20UnorderedPai?= =?UTF-8?q?r=20=E2=80=93=20now=20compiles=20fast=20without=20`--lossy-unif?= =?UTF-8?q?ication`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../IterativeSets/UnorderedPair/Base.agda | 97 ++++++++++++------- 1 file changed, 61 insertions(+), 36 deletions(-) diff --git a/Cubical/Data/IterativeSets/UnorderedPair/Base.agda b/Cubical/Data/IterativeSets/UnorderedPair/Base.agda index 5def6ace84..a5d57034b5 100644 --- a/Cubical/Data/IterativeSets/UnorderedPair/Base.agda +++ b/Cubical/Data/IterativeSets/UnorderedPair/Base.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --lossy-unification #-} - module Cubical.Data.IterativeSets.UnorderedPair.Base where open import Cubical.Foundations.Prelude @@ -8,8 +6,10 @@ open import Cubical.Foundations.Equiv open import Cubical.Foundations.HLevels open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.Function +open import Cubical.Foundations.Univalence open import Cubical.Functions.Embedding open import Cubical.Data.Sum +open import Cubical.Data.Sum.Properties open import Cubical.Data.Bool open import Cubical.Data.Sigma open import Cubical.Data.Empty renaming (elim to ⊥-elim) @@ -99,41 +99,66 @@ unorderedPair⁰-≢-witness-agnostic {x = x} {y = y} x≢y₁ x≢y₂ = cong ( x≢y₁≡x≢y₂ : x≢y₁ ≡ x≢y₂ x≢y₁≡x≢y₂ = isProp→ (λ ()) x≢y₁ x≢y₂ +private + -- maybe switch a and x, as well as b and y to make it closer to the place where we use it later + module _ {A : Type ℓ} (a b x y : A) (a≢b : ¬ a ≡ b) where + ⊎-×-≡-distr : Iso (((a ≡ x) ⊎ (a ≡ y)) + × ((b ≡ x) ⊎ (b ≡ y))) + (((a ≡ x) × (b ≡ y)) + ⊎ ((a ≡ y) × (b ≡ x))) + ⊎-×-≡-distr .Iso.fun (inl a≡x , inl b≡x) = ⊥-elim (a≢b (a≡x ∙ sym b≡x)) + ⊎-×-≡-distr .Iso.fun (inl a≡x , inr b≡y) = inl (a≡x , b≡y) + ⊎-×-≡-distr .Iso.fun (inr a≡y , inl b≡x) = inr (a≡y , b≡x) + ⊎-×-≡-distr .Iso.fun (inr a≡y , inr b≡y) = ⊥-elim (a≢b (a≡y ∙ sym b≡y)) + + ⊎-×-≡-distr .Iso.inv (inl (a≡x , b≡y)) .fst = inl a≡x + ⊎-×-≡-distr .Iso.inv (inl (a≡x , b≡y)) .snd = inr b≡y + ⊎-×-≡-distr .Iso.inv (inr (a≡y , b≡x)) .fst = inr a≡y + ⊎-×-≡-distr .Iso.inv (inr (a≡y , b≡x)) .snd = inl b≡x + + ⊎-×-≡-distr .Iso.sec (inl _) = refl + ⊎-×-≡-distr .Iso.sec (inr _) = refl + + ⊎-×-≡-distr .Iso.ret (inl a≡x , inl b≡x) = ⊥-elim {A = λ _ → ⊎-×-≡-distr .Iso.inv (⊎-×-≡-distr .Iso.fun (inl a≡x , inl b≡x)) ≡ (inl a≡x , inl b≡x)} (a≢b (a≡x ∙ sym b≡x)) + ⊎-×-≡-distr .Iso.ret (inl x , inr x₁) = refl + ⊎-×-≡-distr .Iso.ret (inr x , inl x₁) = refl + ⊎-×-≡-distr .Iso.ret (inr a≡y , inr b≡y) = ⊥-elim {A = λ _ → Iso.inv ⊎-×-≡-distr (Iso.fun ⊎-×-≡-distr (inr a≡y , inr b≡y)) + ≡ (inr a≡y , inr b≡y)} (a≢b (a≡y ∙ sym b≡y)) + unorderedPair⁰≡unorderedPair⁰ : {x y a b : V⁰ {ℓ}} {x≢y : ¬ (x ≡ y)} {a≢b : ¬ (a ≡ b)} → ((unorderedPair⁰ x y x≢y ≡ unorderedPair⁰ a b a≢b) ≃ (((x ≡ a) × (y ≡ b)) ⊎ ((x ≡ b) × (y ≡ a)))) unorderedPair⁰≡unorderedPair⁰ {x = x} {y = y} {a = a} {b = b} {x≢y = x≢y} {a≢b = a≢b} - = propBiimpl→Equiv (isSetV⁰ _ _) isPropRHS f g - where - isPropRHS : isProp (((x ≡ a) × (y ≡ b)) ⊎ ((x ≡ b) × (y ≡ a))) - isPropRHS = isProp⊎ (isProp× (isSetV⁰ _ _) (isSetV⁰ _ _)) - (isProp× (isSetV⁰ _ _) (isSetV⁰ _ _)) - (λ (x≡a , _) (_ , y≡a) → x≢y (x≡a ∙ (sym y≡a))) - - destruct : (unorderedPair⁰ x y _ ≡ unorderedPair⁰ a b _) - → ((x ≡ a) ⊎ (x ≡ b)) × ((y ≡ a) ⊎ (y ≡ b)) - destruct p .fst = unorderedPair⁰-is-unordered-pair-sym .fst - (≡V⁰-≃-≃V⁰ .fst p .fst x (lift false , refl)) - destruct p .snd = unorderedPair⁰-is-unordered-pair-sym .fst - (≡V⁰-≃-≃V⁰ .fst p .fst y (lift true , refl)) - - filter : ((x ≡ a) ⊎ (x ≡ b)) × ((y ≡ a) ⊎ (y ≡ b)) - → ((x ≡ a) × (y ≡ b)) ⊎ ((x ≡ b) × (y ≡ a)) - filter (inl x≡a , inl y≡a) = ⊥-elim (x≢y (x≡a ∙ (sym y≡a))) - filter (inl x≡a , inr y≡b) = inl (x≡a , y≡b) - filter (inr x≡b , inl y≡a) = inr (x≡b , y≡a) - filter (inr x≡b , inr y≡b) = ⊥-elim (x≢y (x≡b ∙ (sym y≡b))) - - f : unorderedPair⁰ x y _ ≡ unorderedPair⁰ a b _ - → ((x ≡ a) × (y ≡ b)) ⊎ ((x ≡ b) × (y ≡ a)) - f = filter ∘ destruct - - -- TODO: make more efficient somehow - g : ((x ≡ a) × (y ≡ b)) ⊎ ((x ≡ b) × (y ≡ a)) → unorderedPair⁰ x y _ ≡ unorderedPair⁰ a b _ - g (inl (x≡a , y≡b)) = unorderedPair⁰-≢-witness-agnostic x≢y _ - ∙∙ (λ i → unorderedPair⁰ (x≡a i) (y≡b i) (≢-move-i0→i x≡a y≡b i x≢y)) - ∙∙ unorderedPair⁰-≢-witness-agnostic _ a≢b - g (inr (x≡b , y≡a)) = (unorderedPair⁰-≢-witness-agnostic x≢y _ - ∙∙ (λ i → unorderedPair⁰ (x≡b i) (y≡a i) (≢-move-i0→i x≡b y≡a i x≢y)) - ∙∙ unorderedPair⁰-≢-witness-agnostic _ (λ b≡a → a≢b (sym b≡a))) - ∙ unorderedUnorderedPair⁰ + = compEquiv (compEquiv ≡V⁰-≃-≃V⁰' (compEquiv L M)) (isoToEquiv (⊎-×-≡-distr x y a b x≢y)) + where + L : ((z : V⁰) → (z ∈⁰ unorderedPair⁰ x y x≢y) ≃ (z ∈⁰ unorderedPair⁰ a b a≢b)) + ≃ + ((z : V⁰) → ((z ≡ x) ⊎ (z ≡ y)) ≃ ((z ≡ a) ⊎ (z ≡ b))) + L = equivΠCod (λ z → equivComp unorderedPair⁰-is-unordered-pair-sym + unorderedPair⁰-is-unordered-pair-sym) + + M : ((z : V⁰) → ((z ≡ x) ⊎ (z ≡ y)) ≃ ((z ≡ a) ⊎ (z ≡ b))) + ≃ + ((x ≡ a) ⊎ (x ≡ b)) × ((y ≡ a) ⊎ (y ≡ b)) + M = propBiimpl→Equiv propLHS propRHS f g + where + propLHS : isProp ((z : V⁰) → ((z ≡ x) ⊎ (z ≡ y)) ≃ ((z ≡ a) ⊎ (z ≡ b))) + propLHS = isPropΠ (λ z → isOfHLevel≃ 1 + (isProp⊎ (isSetV⁰ z x) (isSetV⁰ z y) (λ z≡x z≡y → x≢y (sym z≡x ∙ z≡y))) + (isProp⊎ (isSetV⁰ z a) (isSetV⁰ z b) (λ z≡a z≡b → a≢b (sym z≡a ∙ z≡b)))) + + propRHS : isProp (((x ≡ a) ⊎ (x ≡ b)) × ((y ≡ a) ⊎ (y ≡ b))) + propRHS = isProp× (isProp⊎ (isSetV⁰ x a) (isSetV⁰ x b) (λ x≡a x≡b → a≢b (sym x≡a ∙ x≡b))) + (isProp⊎ (isSetV⁰ y a) (isSetV⁰ y b) (λ y≡a y≡b → a≢b (sym y≡a ∙ y≡b))) + + f : ((z : V⁰) → ((z ≡ x) ⊎ (z ≡ y)) ≃ ((z ≡ a) ⊎ (z ≡ b))) → + ((x ≡ a) ⊎ (x ≡ b)) × ((y ≡ a) ⊎ (y ≡ b)) + f E .fst = E x .fst (inl refl) + f E .snd = E y .fst (inr refl) + + g : ((x ≡ a) ⊎ (x ≡ b)) × ((y ≡ a) ⊎ (y ≡ b)) → + (z : V⁰) → ((z ≡ x) ⊎ (z ≡ y)) ≃ ((z ≡ a) ⊎ (z ≡ b)) + g (inl x≡a , inl y≡a) = ⊥-elim (x≢y (x≡a ∙ sym y≡a)) + g (inl x≡a , inr y≡b) z = pathToEquiv (λ i → (z ≡ x≡a i) ⊎ (z ≡ y≡b i)) + g (inr x≡b , inl y≡a) z = compEquiv (pathToEquiv (λ i → (z ≡ x≡b i) ⊎ (z ≡ y≡a i))) ⊎-swap-≃ + g (inr x≡b , inr y≡b) = ⊥-elim (x≢y (x≡b ∙ sym y≡b)) From 7c4efc1cff820d2e14134eeca98b6614b0613f25 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fabian=20Lukas=20Grubm=C3=BCller?= Date: Tue, 12 May 2026 14:48:17 +0200 Subject: [PATCH 05/11] =?UTF-8?q?Improve=20legibility=20of=20ordered=20pai?= =?UTF-8?q?rs=20=E2=80=93=20still=20doesn't=20compile=20without=20`--lossy?= =?UTF-8?q?-unification`=20[skip=20ci]?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Cubical/Data/Empty/Properties.agda | 8 ++ Cubical/Data/IterativeSets/OrderedPair.agda | 78 +++++++++++++------ .../IterativeSets/UnorderedPair/Base.agda | 10 +++ 3 files changed, 71 insertions(+), 25 deletions(-) diff --git a/Cubical/Data/Empty/Properties.agda b/Cubical/Data/Empty/Properties.agda index bd3a473cd2..6da0851600 100644 --- a/Cubical/Data/Empty/Properties.agda +++ b/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 (λ ()) diff --git a/Cubical/Data/IterativeSets/OrderedPair.agda b/Cubical/Data/IterativeSets/OrderedPair.agda index 483a4b9f12..b38047a4cd 100644 --- a/Cubical/Data/IterativeSets/OrderedPair.agda +++ b/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 diff --git a/Cubical/Data/IterativeSets/UnorderedPair/Base.agda b/Cubical/Data/IterativeSets/UnorderedPair/Base.agda index a5d57034b5..6b2c1d86df 100644 --- a/Cubical/Data/IterativeSets/UnorderedPair/Base.agda +++ b/Cubical/Data/IterativeSets/UnorderedPair/Base.agda @@ -162,3 +162,13 @@ unorderedPair⁰≡unorderedPair⁰ {x = x} {y = y} {a = a} {b = b} {x≢y = x g (inl x≡a , inr y≡b) z = pathToEquiv (λ i → (z ≡ x≡a i) ⊎ (z ≡ y≡b i)) g (inr x≡b , inl y≡a) z = compEquiv (pathToEquiv (λ i → (z ≡ x≡b i) ⊎ (z ≡ y≡a i))) ⊎-swap-≃ g (inr x≡b , inr y≡b) = ⊥-elim (x≢y (x≡b ∙ sym y≡b)) + +unorderedPair⁰≡unorderedPair⁰' : {x y a b : V⁰ {ℓ}} {x≢y : ¬ (x ≡ y)} {a≢b : ¬ (a ≡ b)} + → ¬ x ≡ b + → (unorderedPair⁰ x y x≢y ≡ unorderedPair⁰ a b a≢b) + ≃ + ((x ≡ a) × (y ≡ b)) +unorderedPair⁰≡unorderedPair⁰' {x = x} {y = y} {a = a} {b = b} x≢b = compEquiv unorderedPair⁰≡unorderedPair⁰ + (compEquiv (⊎-equiv (idEquiv ((x ≡ a) × (y ≡ b))) + (uninhabEquiv⊥ (λ p → x≢b (p .fst)))) + ⊎-IdR-⊥-≃) From b0df8e264d1ecb5c29040fe586f6a8170d3dda16 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fabian=20Lukas=20Grubm=C3=BCller?= Date: Sat, 16 May 2026 18:10:13 +0200 Subject: [PATCH 06/11] Remove unnecessary definition --- Cubical/Data/IterativeSets/UnorderedPair/Base.agda | 7 ------- 1 file changed, 7 deletions(-) diff --git a/Cubical/Data/IterativeSets/UnorderedPair/Base.agda b/Cubical/Data/IterativeSets/UnorderedPair/Base.agda index 6b2c1d86df..34e5f68cd6 100644 --- a/Cubical/Data/IterativeSets/UnorderedPair/Base.agda +++ b/Cubical/Data/IterativeSets/UnorderedPair/Base.agda @@ -21,13 +21,6 @@ private variable ℓ : Level --- TODO: (possibly) rename and move -private - module _ where - ≢-move-i0→i : {ℓ : Level} {A : Type ℓ} {x y a b : A} (p : x ≡ a) (q : y ≡ b) - (i : I) → ¬ (x ≡ y) → ¬ (p i ≡ q i) - ≢-move-i0→i p q i x≢y pi≡qi = x≢y ((λ j → p (i ∧ j)) ∙∙ pi≡qi ∙∙ λ j → q (i ∧ ~ j)) - unorderedPair⁰ : (x y : V⁰ {ℓ}) → ¬ (x ≡ y) → V⁰ {ℓ} unorderedPair⁰ {ℓ} x y x≢y = fromEmb emb where From d74157dfcf4b0206e42052e5b4ee7de7dba72e9d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fabian=20Lukas=20Grubm=C3=BCller?= Date: Sat, 16 May 2026 18:10:34 +0200 Subject: [PATCH 07/11] Pi types checkpoint [skip ci] --- Cubical/Data/IterativeSets/Pi.agda | 238 +++++++++++++++++++---------- 1 file changed, 158 insertions(+), 80 deletions(-) diff --git a/Cubical/Data/IterativeSets/Pi.agda b/Cubical/Data/IterativeSets/Pi.agda index 26abbbfb53..18173033cf 100644 --- a/Cubical/Data/IterativeSets/Pi.agda +++ b/Cubical/Data/IterativeSets/Pi.agda @@ -25,111 +25,189 @@ private y : El⁰ x → V⁰ {ℓ} 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 _ {ℓ ℓ' : Level} {A : Type ℓ} {B : Type ℓ'} (f : A → B) where + Inj : Type (ℓ-max ℓ ℓ') + Inj = {x y : A} → f x ≡ f y → x ≡ y -private - module _ {ℓA ℓA' ℓB : Level} {A : Type ℓA} {A' : Type ℓA'} {B : A' → Type ℓB} (f : A → A') (g : (x : A) → B (f x)) where - Σfun : A → Σ A' B - Σfun x .fst = f x - Σfun x .snd = g x +apply⁰ : {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ x → V⁰ {ℓ}} → ((a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)) → El⁰ x → V⁰ {ℓ} +apply⁰ {ℓ} {x} {y} Φ a = ⟨ elements x a , elements (y a) (Φ a) ⟩⁰ - InjFstInj : Inj f → Inj Σfun - InjFstInj injf p = injf (cong fst p) +apply⁰-inj : {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ x → V⁰ {ℓ}} → (Φ : (a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)) → Inj (apply⁰ {ℓ} {x} {y} Φ) +apply⁰-inj {ℓ} {x} {y} Φ {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)) -private - module _ {ℓA ℓA' ℓB ℓB' : Level} {A : Type ℓA} {A' : Type ℓA'} {B : A → Type ℓB} {B' : A' → Type ℓB'} (setA' : isSet A') (f : A → A') (g : (x : A) → B x → B' (f x)) where - Σfun' : Σ A B → Σ A' B' - Σfun' pair .fst = f (pair .fst) - Σfun' pair .snd = uncurry g pair +apply⁰-emb : {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ x → V⁰ {ℓ}} → (Φ : (a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)) → isEmbedding (apply⁰ {ℓ} {x} {y} Φ) +apply⁰-emb {ℓ} {x} {y} Φ = injEmbedding {A = El⁰ x} {B = V⁰ {ℓ}} isSetV⁰ (apply⁰-inj {ℓ} {x} {y} Φ) + +apply⁰-inj2' : {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ x → V⁰ {ℓ}} (Φ Ψ : (a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)) (a : El⁰ x) → apply⁰ {ℓ} {x} {y} Φ ≡ apply⁰ {ℓ} {x} {y} Ψ → Φ a ≡ Ψ a +apply⁰-inj2' {ℓ} {x} {y} Φ Ψ a p = {!!} + +apply⁰-inj2 : {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ x → V⁰ {ℓ}} → Inj (apply⁰ {ℓ} {x} {y}) +apply⁰-inj2 {ℓ} {x} {y} {Φ} {Ψ} p = funExt λ a → apply⁰-inj2' {ℓ} {x} {y} Φ Ψ a p - InjΣInj : Inj f → ((x : A) → Inj (g x)) → Inj Σfun' - InjΣInj injf injg {a , b} {c , d} p = ΣPathTransport→PathΣ (a , b) (c , d) (q1 , q2) - where - s : Σ[ p1 ∈ f a ≡ f c ] subst B' p1 (g a b) ≡ g c d - s = PathΣ→ΣPathTransport _ _ p +apply⁰-emb2 : {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ x → V⁰ {ℓ}} → isEmbedding (apply⁰ {ℓ} {x} {y}) +apply⁰-emb2 {ℓ} {x} {y} = injEmbedding {A = (a : El⁰ x) → El⁰ (y a)} {B = El⁰ x → V⁰} {f = apply⁰ {ℓ} {x} {y}} (isSet→ {A' = V⁰ {ℓ}} {A = El⁰ {ℓ} x} (isSetV⁰ {ℓ})) (apply⁰-inj2 {ℓ} {x} {y}) + +graph⁰ : {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ x → V⁰ {ℓ}} → ((a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)) → V⁰ {ℓ} +graph⁰ {ℓ} {x} {y} Φ = fromEmb E + where + E : Embedding V⁰ ℓ + E .fst = El⁰ x + E .snd .fst = apply⁰ {ℓ} {x} {y} Φ + E .snd .snd = apply⁰-emb {ℓ} {x} {y} Φ + +graph⁰-helper : {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ x → V⁰ {ℓ}} (Φ : (a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)) (z : V⁰ {ℓ}) + → ((z ∈⁰ graph⁰ Φ) ≡ fiber (apply⁰ {ℓ} {x} {y} Φ) z) -- (Σ[ a ∈ El⁰ x ] apply⁰ {ℓ} {x} {y} Φ a ≡ z)) +graph⁰-helper {ℓ} {x} {y} Φ z = refl +-- propBiimpl→Equiv (isProp∈⁰ {x = graph⁰ Φ} {z = z}) (isEmbedding→hasPropFibers {f = apply⁰ {ℓ} {x} {y} Φ} (apply⁰-emb {ℓ} {x} {y} Φ) z) (idfun (z ∈⁰ graph⁰ Φ)) (idfun (fiber (apply⁰ Φ) z)) + +Π⁰ : (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⁰ + E .snd .snd = {!!} + +-- injEmbedding {A = (a : El⁰ x) → El⁰ (y a)} {B = V⁰ {ℓ}} isSetV⁰ λ {Φ Ψ : (a : El⁰ x) → El⁰ (y a)} (p : graph⁰ Φ ≡ graph⁰ Ψ) → ( +-- let +-- P : ((z : V⁰ {ℓ}) → z ∈⁰ graph⁰ Φ → z ∈⁰ graph⁰ Ψ) × ((z : V⁰ {ℓ}) → z ∈⁰ graph⁰ Ψ → z ∈⁰ graph⁰ Φ) +-- P = ≡V⁰-≃-≃V⁰ {x = graph⁰ Φ} {y = graph⁰ Ψ} .fst p + +-- P₁ : (z : V⁰) → z ∈⁰ graph⁰ Φ → z ∈⁰ graph⁰ Ψ +-- P₁ = P .fst - q1 : a ≡ c - q1 = injf (s .fst) +-- s : (a : El⁰ x) → V⁰ {ℓ} +-- s a = apply⁰ {ℓ} {x} {y} Φ a - p1' : f a ≡ f c - p1' = cong f q1 +-- s∈Φ : (a : El⁰ x) → (s a) ∈⁰ (graph⁰ Φ) +-- s∈Φ a = a , refl - s1≡p1' : (s .fst) ≡ (cong f q1) - s1≡p1' = setA' (f a) (f c) (s .fst) (cong f q1) +-- t : (a : El⁰ x) → index x +-- t a = s∈Φ a .fst - p1'≡s1 : (cong f q1) ≡ s .fst - p1'≡s1 = setA' (f a) (f c) (cong f q1) (s .fst) +-- t-fib : (a : El⁰ x) → apply⁰ Φ a ≡ apply⁰ Φ a +-- t-fib a = s∈Φ a .snd - α : subst (λ z → B' (f z)) q1 (g a b) ≡ g c (subst B q1 b) - α = substCommSlice (λ z → B z) (λ z → B' (f z)) g (injf (s .fst)) b +-- s∈Ψ : (a : El⁰ x) → (s a) ∈⁰ (graph⁰ Ψ) +-- s∈Ψ a = P₁ (s a) (s∈Φ a) - β : subst (λ z → B' (f z)) q1 (g a b) ≡ subst B' (s .fst) (g a b) - β = cong (λ m → subst B' m (g a b)) p1'≡s1 +-- t' : (a : El⁰ x) → index x +-- t' a = s∈Ψ a .fst - p2 : g c (subst B q1 b) ≡ g c d - p2 = sym α ∙ β ∙ s .snd +-- t'-fib : (a : El⁰ x) → apply⁰ Ψ +-- (≡V⁰-≃-≃V⁰ .fst p .fst (apply⁰ Φ a) +-- (a , (λ _ → elements (graph⁰ Φ) a)) .fst) +-- ≡ apply⁰ Φ a +-- t'-fib a = s∈Ψ a .snd - q2 : subst B q1 b ≡ d - q2 = injg c p2 +-- goal' : (a : El⁰ x) → Φ a ≡ Ψ a +-- goal' a = {!!} + +-- goal : Φ ≡ Ψ +-- goal = funExt goal' +-- in goal) -graph⁰ : ((a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)) → V⁰ {ℓ} -graph⁰ {ℓ = ℓ} {x = x} {y = y} f = fromEmb E - where - E : Embedding (V⁰ {ℓ}) ℓ - E .fst = El⁰ x - E .snd .fst a = orderedPair⁰ (elements x a , elements (y a) (f a)) - E .snd .snd = injEmbedding isSetV⁰ (λ {v} {w} p → isEmbedding→Inj {f = elements x} (isEmbedding-elements x) v w (orderedPair⁰≡orderedPair⁰ .fst p .fst)) +-- private +-- module _ {ℓA ℓA' ℓB : Level} {A : Type ℓA} {A' : Type ℓA'} {B : A' → Type ℓB} (f : A → A') (g : (x : A) → B (f x)) where +-- Σfun : A → Σ A' B +-- Σfun x .fst = f x +-- Σfun x .snd = g x -Π⁰ : (x : V⁰ {ℓ}) → ((a : El⁰ x) → V⁰ {ℓ}) → V⁰ {ℓ} -Π⁰ {ℓ} x y = fromEmb E - where - In : {f g : (a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)} → graph⁰ {x = x} {y = y} f ≡ graph⁰ {x = x} {y = y} g → (a : El⁰ x) → f a ≡ g a - In {f} {g} p a = - let - ∈⁰graph⁰-f→g : ((z : V⁰) → z ∈⁰ graph⁰ f → z ∈⁰ graph⁰ g) - ∈⁰graph⁰-f→g = ≡V⁰-≃-≃V⁰ .fst p .fst +-- InjFstInj : Inj f → Inj Σfun +-- InjFstInj injf p = injf (cong fst p) - p : Σ[ a' ∈ El⁰ x ] orderedPair⁰ ((elements x a') , (elements (y a') (g a'))) ≡ orderedPair⁰ ((elements x a) , (elements (y a) (f a))) - p = ∈⁰graph⁰-f→g (orderedPair⁰ ((elements x a) , (elements (y a) (f a)))) (a , refl) +-- private +-- module _ {ℓA ℓA' ℓB ℓB' : Level} {A : Type ℓA} {A' : Type ℓA'} {B : A → Type ℓB} {B' : A' → Type ℓB'} (setA' : isSet A') (f : A → A') (g : (x : A) → B x → B' (f x)) where +-- Σfun' : Σ A B → Σ A' B' +-- Σfun' pair .fst = f (pair .fst) +-- Σfun' pair .snd = uncurry g pair - a' : El⁰ x - a' = p .fst +-- InjΣInj : Inj f → ((x : A) → Inj (g x)) → Inj Σfun' +-- InjΣInj injf injg {a , b} {c , d} p = ΣPathTransport→PathΣ (a , b) (c , d) (q1 , q2) +-- where +-- s : Σ[ p1 ∈ f a ≡ f c ] subst B' p1 (g a b) ≡ g c d +-- s = PathΣ→ΣPathTransport _ _ p - p₂ : orderedPair⁰ ((elements x a') , (elements (y a') (g a'))) ≡ orderedPair⁰ ((elements x a) , (elements (y a) (f a))) - p₂ = p .snd +-- q1 : a ≡ c +-- q1 = injf (s .fst) - q : elements x a' ≡ elements x a - q = orderedPair⁰≡orderedPair⁰ .fst p₂ .fst +-- p1' : f a ≡ f c +-- p1' = cong f q1 - r : a' ≡ a - r = isEmbedding→Inj {f = elements x} (isEmbedding-elements x) a' a q +-- s1≡p1' : (s .fst) ≡ (cong f q1) +-- s1≡p1' = setA' (f a) (f c) (s .fst) (cong f q1) - s : elements (y a') (g a') ≡ elements (y a) (f a) - s = orderedPair⁰≡orderedPair⁰ .fst p₂ .snd +-- p1'≡s1 : (cong f q1) ≡ s .fst +-- p1'≡s1 = setA' (f a) (f c) (cong f q1) (s .fst) + +-- α : subst (λ z → B' (f z)) q1 (g a b) ≡ g c (subst B q1 b) +-- α = substCommSlice (λ z → B z) (λ z → B' (f z)) g (injf (s .fst)) b + +-- β : subst (λ z → B' (f z)) q1 (g a b) ≡ subst B' (s .fst) (g a b) +-- β = cong (λ m → subst B' m (g a b)) p1'≡s1 + +-- p2 : g c (subst B q1 b) ≡ g c d +-- p2 = sym α ∙ β ∙ s .snd + +-- q2 : subst B q1 b ≡ d +-- q2 = injg c p2 + +-- graph⁰ : ((a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)) → V⁰ {ℓ} +-- graph⁰ {ℓ = ℓ} {x = x} {y = y} f = fromEmb E +-- where +-- E : Embedding (V⁰ {ℓ}) ℓ +-- E .fst = El⁰ x +-- E .snd .fst a = orderedPair⁰ (elements x a , elements (y a) (f a)) +-- E .snd .snd = injEmbedding isSetV⁰ (λ {v} {w} p → isEmbedding→Inj {f = elements x} (isEmbedding-elements x) v w (orderedPair⁰≡orderedPair⁰ .fst p .fst)) + +-- Π⁰ : (x : V⁰ {ℓ}) → ((a : El⁰ x) → V⁰ {ℓ}) → V⁰ {ℓ} +-- Π⁰ {ℓ} x y = fromEmb E +-- where +-- In : {f g : (a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)} → graph⁰ {x = x} {y = y} f ≡ graph⁰ {x = x} {y = y} g → (a : El⁰ x) → f a ≡ g a +-- In {f} {g} p a = +-- let +-- ∈⁰graph⁰-f→g : ((z : V⁰) → z ∈⁰ graph⁰ f → z ∈⁰ graph⁰ g) +-- ∈⁰graph⁰-f→g = ≡V⁰-≃-≃V⁰ .fst p .fst + +-- p : Σ[ a' ∈ El⁰ x ] orderedPair⁰ ((elements x a') , (elements (y a') (g a'))) ≡ orderedPair⁰ ((elements x a) , (elements (y a) (f a))) +-- p = ∈⁰graph⁰-f→g (orderedPair⁰ ((elements x a) , (elements (y a) (f a)))) (a , refl) + +-- a' : El⁰ x +-- a' = p .fst + +-- p₂ : orderedPair⁰ ((elements x a') , (elements (y a') (g a'))) ≡ orderedPair⁰ ((elements x a) , (elements (y a) (f a))) +-- p₂ = p .snd + +-- q : elements x a' ≡ elements x a +-- q = orderedPair⁰≡orderedPair⁰ .fst p₂ .fst + +-- r : a' ≡ a +-- r = isEmbedding→Inj {f = elements x} (isEmbedding-elements x) a' a q + +-- s : elements (y a') (g a') ≡ elements (y a) (f a) +-- s = orderedPair⁰≡orderedPair⁰ .fst p₂ .snd - t : elements (y a) (g a) ≡ elements (y a') (g a') - t i = elements (y (r (~ i))) (g (r (~ i))) +-- t : elements (y a) (g a) ≡ elements (y a') (g a') +-- t i = elements (y (r (~ i))) (g (r (~ i))) - goal : f a ≡ g a - goal = isEmbedding→Inj {f = elements (y a)} (isEmbedding-elements (y a)) (f a) (g a) (sym (t ∙ s)) - in goal +-- goal : f a ≡ g a +-- goal = isEmbedding→Inj {f = elements (y a)} (isEmbedding-elements (y a)) (f a) (g a) (sym (t ∙ s)) +-- in goal - In' : {f g : (a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)} → graph⁰ {x = x} {y = y} f ≡ graph⁰ {x = x} {y = y} g → f ≡ g - In' p = funExt (In p) +-- In' : {f g : (a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)} → graph⁰ {x = x} {y = y} f ≡ graph⁰ {x = x} {y = y} g → f ≡ g +-- In' p = funExt (In p) - E : Embedding (V⁰ {ℓ}) ℓ - E .fst = (a : El⁰ x) → El⁰ (y a) - E .snd .fst f = graph⁰ {x = x} {y = y} f - E .snd .snd = injEmbedding isSetV⁰ In' +-- E : Embedding (V⁰ {ℓ}) ℓ +-- E .fst = (a : El⁰ x) → El⁰ (y a) +-- E .snd .fst f = graph⁰ {x = x} {y = y} f +-- E .snd .snd = injEmbedding isSetV⁰ In' -El⁰Π⁰isΠ : El⁰ (Π⁰ x y) ≡ ((a : El⁰ x) → El⁰ (y a)) -El⁰Π⁰isΠ = refl +-- El⁰Π⁰isΠ : El⁰ (Π⁰ x y) ≡ ((a : El⁰ x) → El⁰ (y a)) +-- El⁰Π⁰isΠ = refl -_→⁰_ : V⁰ {ℓ} → V⁰ {ℓ} → V⁰ {ℓ} -x →⁰ y = Π⁰ x (λ _ → y) +-- _→⁰_ : V⁰ {ℓ} → V⁰ {ℓ} → V⁰ {ℓ} +-- x →⁰ y = Π⁰ x (λ _ → y) -El⁰→⁰is→ : {x y : V⁰ {ℓ}} → El⁰ (x →⁰ y) ≡ (El⁰ x → El⁰ y) -El⁰→⁰is→ = refl +-- El⁰→⁰is→ : {x y : V⁰ {ℓ}} → El⁰ (x →⁰ y) ≡ (El⁰ x → El⁰ y) +-- El⁰→⁰is→ = refl From 6e081c23f6084abc7c6d6c1d3f4b423b3fa62b0c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fabian=20Lukas=20Grubm=C3=BCller?= Date: Sat, 16 May 2026 22:11:39 +0200 Subject: [PATCH 08/11] Complete `Cubical.Data.IterativeSets.Pi` such that it compiles within a (reasonably) finite time; cleanup needed --- Cubical/Data/IterativeSets/Pi.agda | 213 +++++++++-------------------- 1 file changed, 66 insertions(+), 147 deletions(-) diff --git a/Cubical/Data/IterativeSets/Pi.agda b/Cubical/Data/IterativeSets/Pi.agda index 18173033cf..0bec0a3906 100644 --- a/Cubical/Data/IterativeSets/Pi.agda +++ b/Cubical/Data/IterativeSets/Pi.agda @@ -38,15 +38,6 @@ apply⁰-inj {ℓ} {x} {y} Φ {a} {b} p = isEmbedding→Inj {A = El⁰ x} {B = V apply⁰-emb : {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ x → V⁰ {ℓ}} → (Φ : (a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)) → isEmbedding (apply⁰ {ℓ} {x} {y} Φ) apply⁰-emb {ℓ} {x} {y} Φ = injEmbedding {A = El⁰ x} {B = V⁰ {ℓ}} isSetV⁰ (apply⁰-inj {ℓ} {x} {y} Φ) -apply⁰-inj2' : {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ x → V⁰ {ℓ}} (Φ Ψ : (a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)) (a : El⁰ x) → apply⁰ {ℓ} {x} {y} Φ ≡ apply⁰ {ℓ} {x} {y} Ψ → Φ a ≡ Ψ a -apply⁰-inj2' {ℓ} {x} {y} Φ Ψ a p = {!!} - -apply⁰-inj2 : {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ x → V⁰ {ℓ}} → Inj (apply⁰ {ℓ} {x} {y}) -apply⁰-inj2 {ℓ} {x} {y} {Φ} {Ψ} p = funExt λ a → apply⁰-inj2' {ℓ} {x} {y} Φ Ψ a p - -apply⁰-emb2 : {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ x → V⁰ {ℓ}} → isEmbedding (apply⁰ {ℓ} {x} {y}) -apply⁰-emb2 {ℓ} {x} {y} = injEmbedding {A = (a : El⁰ x) → El⁰ (y a)} {B = El⁰ x → V⁰} {f = apply⁰ {ℓ} {x} {y}} (isSet→ {A' = V⁰ {ℓ}} {A = El⁰ {ℓ} x} (isSetV⁰ {ℓ})) (apply⁰-inj2 {ℓ} {x} {y}) - graph⁰ : {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ x → V⁰ {ℓ}} → ((a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)) → V⁰ {ℓ} graph⁰ {ℓ} {x} {y} Φ = fromEmb E where @@ -58,156 +49,84 @@ graph⁰ {ℓ} {x} {y} Φ = fromEmb E graph⁰-helper : {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ x → V⁰ {ℓ}} (Φ : (a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)) (z : V⁰ {ℓ}) → ((z ∈⁰ graph⁰ Φ) ≡ fiber (apply⁰ {ℓ} {x} {y} Φ) z) -- (Σ[ a ∈ El⁰ x ] apply⁰ {ℓ} {x} {y} Φ a ≡ z)) graph⁰-helper {ℓ} {x} {y} Φ z = refl --- propBiimpl→Equiv (isProp∈⁰ {x = graph⁰ Φ} {z = z}) (isEmbedding→hasPropFibers {f = apply⁰ {ℓ} {x} {y} Φ} (apply⁰-emb {ℓ} {x} {y} Φ) z) (idfun (z ∈⁰ graph⁰ Φ)) (idfun (fiber (apply⁰ Φ) z)) -Π⁰ : (x : V⁰ {ℓ}) → (El⁰ x → V⁰ {ℓ}) → V⁰ {ℓ} -Π⁰ {ℓ} x y = fromEmb E +apply⁰-inj2' : {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ x → V⁰ {ℓ}} (Φ Ψ : (a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)) (a : El⁰ x) → apply⁰ {ℓ} {x} {y} Φ ≡ apply⁰ {ℓ} {x} {y} Ψ → Φ a ≡ Ψ a +apply⁰-inj2' {ℓ} {x} {y} Φ Ψ a p = isEmbedding→Inj {A = index (y a)} {B = V⁰} (isEmbedding-elements (y a)) (Φ a) (Ψ a) (P .snd) where - E : Embedding V⁰ ℓ - E .fst = (a : El⁰ x) → El⁰ (y a) - E .snd .fst = graph⁰ - E .snd .snd = {!!} - --- injEmbedding {A = (a : El⁰ x) → El⁰ (y a)} {B = V⁰ {ℓ}} isSetV⁰ λ {Φ Ψ : (a : El⁰ x) → El⁰ (y a)} (p : graph⁰ Φ ≡ graph⁰ Ψ) → ( --- let --- P : ((z : V⁰ {ℓ}) → z ∈⁰ graph⁰ Φ → z ∈⁰ graph⁰ Ψ) × ((z : V⁰ {ℓ}) → z ∈⁰ graph⁰ Ψ → z ∈⁰ graph⁰ Φ) --- P = ≡V⁰-≃-≃V⁰ {x = graph⁰ Φ} {y = graph⁰ Ψ} .fst p + p' : apply⁰ Φ a ≡ apply⁰ Ψ a + p' = funExt⁻ p a --- P₁ : (z : V⁰) → z ∈⁰ graph⁰ Φ → z ∈⁰ graph⁰ Ψ --- P₁ = P .fst + P : (elements x a ≡ elements x a) × + (elements (y a) (Φ a) ≡ elements (y a) (Ψ a)) + P = orderedPair⁰≡orderedPair⁰ {x = elements x a} {y = elements (y a) (Φ a)} {a = elements x a} {b = elements (y a) (Ψ a)} .fst p' --- s : (a : El⁰ x) → V⁰ {ℓ} --- s a = apply⁰ {ℓ} {x} {y} Φ a --- s∈Φ : (a : El⁰ x) → (s a) ∈⁰ (graph⁰ Φ) --- s∈Φ a = a , refl +apply⁰-inj2 : {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ x → V⁰ {ℓ}} → Inj (apply⁰ {ℓ} {x} {y}) +apply⁰-inj2 {ℓ} {x} {y} {Φ} {Ψ} p = funExt λ a → apply⁰-inj2' {ℓ} {x} {y} Φ Ψ a p --- t : (a : El⁰ x) → index x --- t a = s∈Φ a .fst +apply⁰-emb2 : {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ x → V⁰ {ℓ}} → isEmbedding (apply⁰ {ℓ} {x} {y}) +apply⁰-emb2 {ℓ} {x} {y} = injEmbedding {A = (a : El⁰ x) → El⁰ (y a)} {B = El⁰ x → V⁰} {f = apply⁰ {ℓ} {x} {y}} (isSet→ {A' = V⁰ {ℓ}} {A = El⁰ {ℓ} x} (isSetV⁰ {ℓ})) (apply⁰-inj2 {ℓ} {x} {y}) + +graph⁰-inj : {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ x → V⁰ {ℓ}} → Inj (graph⁰ {ℓ} {x} {y}) +graph⁰-inj {ℓ} {x} {y} {Φ} {Ψ} p = apply⁰-inj2 {ℓ} {x} {y} 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 .fst + + F₂ : (z : V⁰) → z ∈⁰ graph⁰ Ψ → z ∈⁰ graph⁰ Φ + F₂ = F .snd + + module _ (a : El⁰ x) where + s : V⁰ + s = apply⁰ {ℓ} {x} {y} Ψ a + + s∈Ψ : s ∈⁰ graph⁰ Ψ + s∈Ψ .fst = a + s∈Ψ .snd = refl + + s∈Φ : s ∈⁰ graph⁰ Φ + s∈Φ = F₂ s s∈Ψ --- t-fib : (a : El⁰ x) → apply⁰ Φ a ≡ apply⁰ Φ a --- t-fib a = s∈Φ a .snd + a' : El⁰ x + a' = s∈Φ .fst --- s∈Ψ : (a : El⁰ x) → (s a) ∈⁰ (graph⁰ Ψ) --- s∈Ψ a = P₁ (s a) (s∈Φ a) + q : apply⁰ {ℓ} {x} {y} Φ a' ≡ apply⁰ {ℓ} {x} {y} Ψ a + q = s∈Φ .snd --- t' : (a : El⁰ x) → index x --- t' a = s∈Ψ a .fst - --- t'-fib : (a : El⁰ x) → apply⁰ Ψ --- (≡V⁰-≃-≃V⁰ .fst p .fst (apply⁰ Φ a) --- (a , (λ _ → elements (graph⁰ Φ) a)) .fst) --- ≡ apply⁰ Φ a --- t'-fib a = s∈Ψ a .snd - --- goal' : (a : El⁰ x) → Φ a ≡ Ψ a --- goal' a = {!!} - --- goal : Φ ≡ Ψ --- goal = funExt goal' --- in goal) - --- private --- module _ {ℓA ℓA' ℓB : Level} {A : Type ℓA} {A' : Type ℓA'} {B : A' → Type ℓB} (f : A → A') (g : (x : A) → B (f x)) where --- Σfun : A → Σ A' B --- Σfun x .fst = f x --- Σfun x .snd = g x - --- InjFstInj : Inj f → Inj Σfun --- InjFstInj injf p = injf (cong fst p) - --- private --- module _ {ℓA ℓA' ℓB ℓB' : Level} {A : Type ℓA} {A' : Type ℓA'} {B : A → Type ℓB} {B' : A' → Type ℓB'} (setA' : isSet A') (f : A → A') (g : (x : A) → B x → B' (f x)) where --- Σfun' : Σ A B → Σ A' B' --- Σfun' pair .fst = f (pair .fst) --- Σfun' pair .snd = uncurry g pair - --- InjΣInj : Inj f → ((x : A) → Inj (g x)) → Inj Σfun' --- InjΣInj injf injg {a , b} {c , d} p = ΣPathTransport→PathΣ (a , b) (c , d) (q1 , q2) --- where --- s : Σ[ p1 ∈ f a ≡ f c ] subst B' p1 (g a b) ≡ g c d --- s = PathΣ→ΣPathTransport _ _ p - --- q1 : a ≡ c --- q1 = injf (s .fst) - --- p1' : f a ≡ f c --- p1' = cong f q1 - --- s1≡p1' : (s .fst) ≡ (cong f q1) --- s1≡p1' = setA' (f a) (f c) (s .fst) (cong f q1) - --- p1'≡s1 : (cong f q1) ≡ s .fst --- p1'≡s1 = setA' (f a) (f c) (cong f q1) (s .fst) - --- α : subst (λ z → B' (f z)) q1 (g a b) ≡ g c (subst B q1 b) --- α = substCommSlice (λ z → B z) (λ z → B' (f z)) g (injf (s .fst)) b - --- β : subst (λ z → B' (f z)) q1 (g a b) ≡ subst B' (s .fst) (g a b) --- β = cong (λ m → subst B' m (g a b)) p1'≡s1 - --- p2 : g c (subst B q1 b) ≡ g c d --- p2 = sym α ∙ β ∙ s .snd - --- q2 : subst B q1 b ≡ d --- q2 = injg c p2 - --- graph⁰ : ((a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)) → V⁰ {ℓ} --- graph⁰ {ℓ = ℓ} {x = x} {y = y} f = fromEmb E --- where --- E : Embedding (V⁰ {ℓ}) ℓ --- E .fst = El⁰ x --- E .snd .fst a = orderedPair⁰ (elements x a , elements (y a) (f a)) --- E .snd .snd = injEmbedding isSetV⁰ (λ {v} {w} p → isEmbedding→Inj {f = elements x} (isEmbedding-elements x) v w (orderedPair⁰≡orderedPair⁰ .fst p .fst)) - --- Π⁰ : (x : V⁰ {ℓ}) → ((a : El⁰ x) → V⁰ {ℓ}) → V⁰ {ℓ} --- Π⁰ {ℓ} x y = fromEmb E --- where --- In : {f g : (a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)} → graph⁰ {x = x} {y = y} f ≡ graph⁰ {x = x} {y = y} g → (a : El⁰ x) → f a ≡ g a --- In {f} {g} p a = --- let --- ∈⁰graph⁰-f→g : ((z : V⁰) → z ∈⁰ graph⁰ f → z ∈⁰ graph⁰ g) --- ∈⁰graph⁰-f→g = ≡V⁰-≃-≃V⁰ .fst p .fst - --- p : Σ[ a' ∈ El⁰ x ] orderedPair⁰ ((elements x a') , (elements (y a') (g a'))) ≡ orderedPair⁰ ((elements x a) , (elements (y a) (f a))) --- p = ∈⁰graph⁰-f→g (orderedPair⁰ ((elements x a) , (elements (y a) (f a)))) (a , refl) + r : elements x a' ≡ elements x a + r = orderedPair⁰≡orderedPair⁰ {x = elements x a'} {y = elements (y a') (Φ a')} {a = elements x a} {b = elements (y a) (Ψ a)} .fst q .fst --- a' : El⁰ x --- a' = p .fst - --- p₂ : orderedPair⁰ ((elements x a') , (elements (y a') (g a'))) ≡ orderedPair⁰ ((elements x a) , (elements (y a) (f a))) --- p₂ = p .snd - --- q : elements x a' ≡ elements x a --- q = orderedPair⁰≡orderedPair⁰ .fst p₂ .fst - --- r : a' ≡ a --- r = isEmbedding→Inj {f = elements x} (isEmbedding-elements x) a' a q - --- s : elements (y a') (g a') ≡ elements (y a) (f a) --- s = orderedPair⁰≡orderedPair⁰ .fst p₂ .snd - --- t : elements (y a) (g a) ≡ elements (y a') (g a') --- t i = elements (y (r (~ i))) (g (r (~ i))) - --- goal : f a ≡ g a --- goal = isEmbedding→Inj {f = elements (y a)} (isEmbedding-elements (y a)) (f a) (g a) (sym (t ∙ s)) --- in goal - + a'≡a : a' ≡ a + a'≡a = isEmbedding→Inj {A = El⁰ x} {B = V⁰ {ℓ}} {f = elements x} + (isEmbedding-elements x) a' a r + + gg : apply⁰ {ℓ} {x} {y} Φ a ≡ apply⁰ {ℓ} {x} {y} Ψ a + gg = transport (cong (λ m → apply⁰ {ℓ} {x} {y} Φ m ≡ apply⁰ {ℓ} {x} {y} Ψ a) a'≡a) q + --- In' : {f g : (a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)} → graph⁰ {x = x} {y = y} f ≡ graph⁰ {x = x} {y = y} g → f ≡ g --- In' p = funExt (In p) + P : apply⁰ {ℓ} {x} {y} Φ ≡ apply⁰ {ℓ} {x} {y} Ψ + P = funExt gg + +graph⁰-emb : {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ x → V⁰ {ℓ}} → isEmbedding (graph⁰ {ℓ} {x} {y}) +graph⁰-emb {ℓ} {x} {y} = injEmbedding {A = (a : El⁰ x) → El⁰ (y a)} {B = V⁰} {f = graph⁰} (isSetV⁰ {ℓ}) (graph⁰-inj {ℓ} {x} {y}) --- E : Embedding (V⁰ {ℓ}) ℓ --- E .fst = (a : El⁰ x) → El⁰ (y a) --- E .snd .fst f = graph⁰ {x = x} {y = y} f --- E .snd .snd = injEmbedding isSetV⁰ In' +Π⁰ : (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⁰ + E .snd .snd = graph⁰-emb {ℓ} {x} {y} --- El⁰Π⁰isΠ : El⁰ (Π⁰ x y) ≡ ((a : El⁰ x) → El⁰ (y a)) --- El⁰Π⁰isΠ = refl +El⁰Π⁰isΠ : El⁰ (Π⁰ x y) ≡ ((a : El⁰ x) → El⁰ (y a)) +El⁰Π⁰isΠ = refl --- _→⁰_ : V⁰ {ℓ} → V⁰ {ℓ} → V⁰ {ℓ} --- x →⁰ y = Π⁰ x (λ _ → y) +_→⁰_ : V⁰ {ℓ} → V⁰ {ℓ} → V⁰ {ℓ} +x →⁰ y = Π⁰ x (λ _ → y) --- El⁰→⁰is→ : {x y : V⁰ {ℓ}} → El⁰ (x →⁰ y) ≡ (El⁰ x → El⁰ y) --- El⁰→⁰is→ = refl +El⁰→⁰is→ : {x y : V⁰ {ℓ}} → El⁰ (x →⁰ y) ≡ (El⁰ x → El⁰ y) +El⁰→⁰is→ = refl From 7e4cc7d59b7ae0c8fef751adeb196d48884a3e39 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fabian=20Lukas=20Grubm=C3=BCller?= Date: Sun, 17 May 2026 16:50:21 +0200 Subject: [PATCH 09/11] Polish code for Pi types; compiles (with `--lossy-unification`) in (reasonably) finite time --- Cubical/Data/IterativeSets/Pi.agda | 166 +++++++++++++++-------------- 1 file changed, 88 insertions(+), 78 deletions(-) diff --git a/Cubical/Data/IterativeSets/Pi.agda b/Cubical/Data/IterativeSets/Pi.agda index 0bec0a3906..26ef038238 100644 --- a/Cubical/Data/IterativeSets/Pi.agda +++ b/Cubical/Data/IterativeSets/Pi.agda @@ -1,7 +1,5 @@ {-# OPTIONS --lossy-unification #-} --- TODO: make type checking terminate - module Cubical.Data.IterativeSets.Pi where open import Cubical.Foundations.Prelude @@ -18,109 +16,121 @@ open import Cubical.Data.IterativeMultisets.Base renaming (index to index∞ ; e open import Cubical.Data.IterativeSets.Base open import Cubical.Data.IterativeSets.OrderedPair -private - variable - ℓ : Level - x : V⁰ {ℓ} - y : El⁰ x → V⁰ {ℓ} - private module _ {ℓ ℓ' : Level} {A : Type ℓ} {B : Type ℓ'} (f : A → B) where Inj : Type (ℓ-max ℓ ℓ') Inj = {x y : A} → f x ≡ f y → x ≡ y -apply⁰ : {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ x → V⁰ {ℓ}} → ((a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)) → El⁰ x → V⁰ {ℓ} -apply⁰ {ℓ} {x} {y} Φ a = ⟨ elements x a , elements (y a) (Φ a) ⟩⁰ - -apply⁰-inj : {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ x → V⁰ {ℓ}} → (Φ : (a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)) → Inj (apply⁰ {ℓ} {x} {y} Φ) -apply⁰-inj {ℓ} {x} {y} Φ {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)) - -apply⁰-emb : {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ x → V⁰ {ℓ}} → (Φ : (a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)) → isEmbedding (apply⁰ {ℓ} {x} {y} Φ) -apply⁰-emb {ℓ} {x} {y} Φ = injEmbedding {A = El⁰ x} {B = V⁰ {ℓ}} isSetV⁰ (apply⁰-inj {ℓ} {x} {y} Φ) - -graph⁰ : {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ x → V⁰ {ℓ}} → ((a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)) → V⁰ {ℓ} -graph⁰ {ℓ} {x} {y} Φ = fromEmb E - where - E : Embedding V⁰ ℓ - E .fst = El⁰ x - E .snd .fst = apply⁰ {ℓ} {x} {y} Φ - E .snd .snd = apply⁰-emb {ℓ} {x} {y} Φ - -graph⁰-helper : {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ x → V⁰ {ℓ}} (Φ : (a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)) (z : V⁰ {ℓ}) - → ((z ∈⁰ graph⁰ Φ) ≡ fiber (apply⁰ {ℓ} {x} {y} Φ) z) -- (Σ[ a ∈ El⁰ x ] apply⁰ {ℓ} {x} {y} Φ a ≡ z)) -graph⁰-helper {ℓ} {x} {y} Φ z = refl - -apply⁰-inj2' : {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ x → V⁰ {ℓ}} (Φ Ψ : (a : El⁰ {ℓ} x) → El⁰ {ℓ} (y a)) (a : El⁰ x) → apply⁰ {ℓ} {x} {y} Φ ≡ apply⁰ {ℓ} {x} {y} Ψ → Φ a ≡ Ψ a -apply⁰-inj2' {ℓ} {x} {y} Φ Ψ a p = isEmbedding→Inj {A = index (y a)} {B = V⁰} (isEmbedding-elements (y a)) (Φ a) (Ψ a) (P .snd) - where - p' : apply⁰ Φ a ≡ apply⁰ Ψ a - p' = funExt⁻ p a - - P : (elements x a ≡ elements x a) × +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)) - P = orderedPair⁰≡orderedPair⁰ {x = elements x a} {y = elements (y a) (Φ a)} {a = elements x a} {b = elements (y a) (Ψ a)} .fst p' + 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 -apply⁰-inj2 : {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ x → V⁰ {ℓ}} → Inj (apply⁰ {ℓ} {x} {y}) -apply⁰-inj2 {ℓ} {x} {y} {Φ} {Ψ} p = funExt λ a → apply⁰-inj2' {ℓ} {x} {y} Φ Ψ 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 -apply⁰-emb2 : {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ x → V⁰ {ℓ}} → isEmbedding (apply⁰ {ℓ} {x} {y}) -apply⁰-emb2 {ℓ} {x} {y} = injEmbedding {A = (a : El⁰ x) → El⁰ (y a)} {B = El⁰ x → V⁰} {f = apply⁰ {ℓ} {x} {y}} (isSet→ {A' = V⁰ {ℓ}} {A = El⁰ {ℓ} x} (isSetV⁰ {ℓ})) (apply⁰-inj2 {ℓ} {x} {y}) +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 : {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ x → V⁰ {ℓ}} → Inj (graph⁰ {ℓ} {x} {y}) -graph⁰-inj {ℓ} {x} {y} {Φ} {Ψ} p = apply⁰-inj2 {ℓ} {x} {y} P - where - F : ((z : V⁰) → z ∈⁰ graph⁰ Φ → z ∈⁰ graph⁰ Ψ) - × ((z : V⁰) → z ∈⁰ graph⁰ Ψ → z ∈⁰ graph⁰ Φ) - F = ≡V⁰-≃-≃V⁰ {x = graph⁰ Φ} {y = graph⁰ Ψ} .fst p + 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 - F₁ : (z : V⁰) → z ∈⁰ graph⁰ Φ → z ∈⁰ graph⁰ Ψ - F₁ = F .fst + module _ (a : El⁰ x) where + s : V⁰ + s = graphEl⁰ Ψ a - F₂ : (z : V⁰) → z ∈⁰ graph⁰ Ψ → z ∈⁰ graph⁰ Φ - F₂ = F .snd + s∈Ψ : s ∈⁰ graph⁰ Ψ + s∈Ψ .fst = a + s∈Ψ .snd = refl - module _ (a : El⁰ x) where - s : V⁰ - s = apply⁰ {ℓ} {x} {y} Ψ a + s∈Φ : s ∈⁰ graph⁰ Φ + s∈Φ = F₂ s s∈Ψ - s∈Ψ : s ∈⁰ graph⁰ Ψ - s∈Ψ .fst = a - s∈Ψ .snd = refl + a' : El⁰ x + a' = s∈Φ .fst - s∈Φ : s ∈⁰ graph⁰ Φ - s∈Φ = F₂ s s∈Ψ + graphEl⁰≡' : graphEl⁰ Φ a' ≡ graphEl⁰ Ψ a + graphEl⁰≡' = s∈Φ .snd - a' : El⁰ x - a' = s∈Φ .fst + 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 - q : apply⁰ {ℓ} {x} {y} Φ a' ≡ apply⁰ {ℓ} {x} {y} Ψ a - q = s∈Φ .snd + a'≡a : a' ≡ a + a'≡a = isEmbedding→Inj {A = El⁰ x} {B = V⁰ {ℓ}} {f = elements x} + (isEmbedding-elements x) a' a els≡ - r : elements x a' ≡ elements x a - r = orderedPair⁰≡orderedPair⁰ {x = elements x a'} {y = elements (y a') (Φ a')} {a = elements x a} {b = elements (y a) (Ψ a)} .fst q .fst + graphEl⁰≡ : graphEl⁰ Φ a ≡ graphEl⁰ Ψ a + graphEl⁰≡ = transport (cong (λ m → graphEl⁰ Φ m ≡ graphEl⁰ Ψ a) a'≡a) graphEl⁰≡' - a'≡a : a' ≡ a - a'≡a = isEmbedding→Inj {A = El⁰ x} {B = V⁰ {ℓ}} {f = elements x} - (isEmbedding-elements x) a' a r + P : graphEl⁰ Φ ≡ graphEl⁰ Ψ + P = funExt graphEl⁰≡ - gg : apply⁰ {ℓ} {x} {y} Φ a ≡ apply⁰ {ℓ} {x} {y} Ψ a - gg = transport (cong (λ m → apply⁰ {ℓ} {x} {y} Φ m ≡ apply⁰ {ℓ} {x} {y} Ψ a) a'≡a) q - - - P : apply⁰ {ℓ} {x} {y} Φ ≡ apply⁰ {ℓ} {x} {y} Ψ - P = funExt gg + graph⁰-emb : isEmbedding graph⁰ + graph⁰-emb = injEmbedding {A = (a : El⁰ x) → El⁰ (y a)} {B = V⁰} {f = graph⁰} (isSetV⁰ {ℓ}) graph⁰-inj -graph⁰-emb : {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ x → V⁰ {ℓ}} → isEmbedding (graph⁰ {ℓ} {x} {y}) -graph⁰-emb {ℓ} {x} {y} = injEmbedding {A = (a : El⁰ x) → El⁰ (y a)} {B = V⁰} {f = graph⁰} (isSetV⁰ {ℓ}) (graph⁰-inj {ℓ} {x} {y}) +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⁰ - E .snd .snd = graph⁰-emb {ℓ} {x} {y} + 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 From 241ff3b617ef22581ffff89326c13ff5d79f9c62 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fabian=20Lukas=20Grubm=C3=BCller?= Date: Sun, 17 May 2026 17:01:57 +0200 Subject: [PATCH 10/11] Fix whitespace --- Cubical/Data/IterativeSets/OrderedPair.agda | 4 ++-- Cubical/Data/IterativeSets/Pi.agda | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Cubical/Data/IterativeSets/OrderedPair.agda b/Cubical/Data/IterativeSets/OrderedPair.agda index b38047a4cd..ff609ec064 100644 --- a/Cubical/Data/IterativeSets/OrderedPair.agda +++ b/Cubical/Data/IterativeSets/OrderedPair.agda @@ -55,7 +55,7 @@ orderedPair⁰≡orderedPair⁰ {ℓ = ℓ} {x = x} {y = y} {a = a} {b = b} = co {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)) ≃ @@ -76,7 +76,7 @@ orderedPair⁰≡orderedPair⁰ {ℓ = ℓ} {x = x} {y = y} {a = a} {b = b} = co ((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)) + step₄ : ((singleton⁰ x ≡ singleton⁰ a) × (singleton⁰ y ≡ singleton⁰ b)) ≃ ((x ≡ a) × (y ≡ b)) step₄ = ≃-× (invEquiv (singleton⁰≡singleton⁰ {x = x} {y = a})) diff --git a/Cubical/Data/IterativeSets/Pi.agda b/Cubical/Data/IterativeSets/Pi.agda index 26ef038238..ec0c7b0d63 100644 --- a/Cubical/Data/IterativeSets/Pi.agda +++ b/Cubical/Data/IterativeSets/Pi.agda @@ -65,7 +65,7 @@ module GraphElements {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ {ℓ} x → V⁰ 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 From 08f78831e778184ae152d64515b6cc4c6e0a166c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fabian=20Lukas=20Grubm=C3=BCller?= Date: Sun, 17 May 2026 17:44:17 +0200 Subject: [PATCH 11/11] Make transport via cong into subst --- Cubical/Data/IterativeSets/Pi.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cubical/Data/IterativeSets/Pi.agda b/Cubical/Data/IterativeSets/Pi.agda index ec0c7b0d63..d7499d400b 100644 --- a/Cubical/Data/IterativeSets/Pi.agda +++ b/Cubical/Data/IterativeSets/Pi.agda @@ -110,7 +110,7 @@ module Graph {ℓ : Level} {x : V⁰ {ℓ}} {y : El⁰ {ℓ} x → V⁰ {ℓ}} w (isEmbedding-elements x) a' a els≡ graphEl⁰≡ : graphEl⁰ Φ a ≡ graphEl⁰ Ψ a - graphEl⁰≡ = transport (cong (λ m → graphEl⁰ Φ m ≡ graphEl⁰ Ψ a) a'≡a) graphEl⁰≡' + graphEl⁰≡ = subst (λ m → graphEl⁰ Φ m ≡ graphEl⁰ Ψ a) a'≡a graphEl⁰≡' P : graphEl⁰ Φ ≡ graphEl⁰ Ψ P = funExt graphEl⁰≡