From 9ef8c26b135b83c9573510b290d04cff13780c38 Mon Sep 17 00:00:00 2001 From: anshwad10 <109362320+anshwad10@users.noreply.github.com> Date: Sat, 22 Nov 2025 21:28:38 +0530 Subject: [PATCH 1/5] Heap! I wonder if I should rename this to groud --- Cubical/Algebra/Heap.agda | 4 + Cubical/Algebra/Heap/Base.agda | 86 ++++++++++++++++ Cubical/Algebra/Heap/Properties.agda | 149 +++++++++++++++++++++++++++ 3 files changed, 239 insertions(+) create mode 100644 Cubical/Algebra/Heap.agda create mode 100644 Cubical/Algebra/Heap/Base.agda create mode 100644 Cubical/Algebra/Heap/Properties.agda diff --git a/Cubical/Algebra/Heap.agda b/Cubical/Algebra/Heap.agda new file mode 100644 index 0000000000..f7d2684517 --- /dev/null +++ b/Cubical/Algebra/Heap.agda @@ -0,0 +1,4 @@ +module Cubical.Algebra.Heap where + +open import Cubical.Algebra.Heap.Base public +open import Cubical.Algebra.Heap.Properties public diff --git a/Cubical/Algebra/Heap/Base.agda b/Cubical/Algebra/Heap/Base.agda new file mode 100644 index 0000000000..000858d0de --- /dev/null +++ b/Cubical/Algebra/Heap/Base.agda @@ -0,0 +1,86 @@ +module Cubical.Algebra.Heap.Base where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Function +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.SIP + +open import Cubical.Reflection.RecordEquiv + +open import Cubical.Displayed.Base +open import Cubical.Displayed.Auto +open import Cubical.Displayed.Record +open import Cubical.Displayed.Universe + +open import Cubical.HITs.PropositionalTruncation + +private variable + ℓ ℓ' : Level + X Y : Type ℓ + +record IsHeap {H : Type ℓ} ([_,_,_] : H → H → H → H) : Type ℓ where + no-eta-equality + constructor isheap + + field + is-set : isSet H + assoc : ∀ a b c d e → [ a , b , [ c , d , e ] ] ≡ [ [ a , b , c ] , d , e ] + idl : ∀ a b → [ a , a , b ] ≡ b + idr : ∀ a b → [ a , b , b ] ≡ a + inhab : ∥ H ∥₁ + +unquoteDecl IsHeapIsoΣ = declareRecordIsoΣ IsHeapIsoΣ (quote IsHeap) + +record HeapStr (H : Type ℓ) : Type ℓ where + constructor heapstr + + field + [_,_,_] : H → H → H → H + isHeap : IsHeap [_,_,_] + + open IsHeap isHeap public + +Heap : ∀ ℓ → Type (ℓ-suc ℓ) +Heap ℓ = TypeWithStr ℓ HeapStr + +record IsHeapHom {X : Type ℓ} {Y : Type ℓ'} (H : HeapStr X) (f : X → Y) (H' : HeapStr Y) : Type (ℓ-max ℓ ℓ') where + constructor makeIsHeapHom + + private + module H = HeapStr H + module H' = HeapStr H' + field + pres-[] : (a b c : X) → f H.[ a , b , c ] ≡ H'.[ f a , f b , f c ] + +unquoteDecl IsHeapHomIsoΣ = declareRecordIsoΣ IsHeapHomIsoΣ (quote IsHeapHom) + +isPropIsHeap : {H : Type ℓ} ([_,_,_] : H → H → H → H) → isProp (IsHeap [_,_,_]) +isPropIsHeap [_,_,_] = isOfHLevelRetractFromIso 1 IsHeapIsoΣ $ isPropΣ isPropIsSet λ is-set → + isProp×3 (isPropΠ5 (λ _ _ _ _ _ → is-set _ _)) (isPropΠ2 λ _ _ → is-set _ _) (isPropΠ2 λ _ _ → is-set _ _) isPropPropTrunc + +isPropIsHeapHom : (H : HeapStr X) (f : X → Y) (H' : HeapStr Y) → isProp (IsHeapHom H f H') +isPropIsHeapHom H f H' = isOfHLevelRetractFromIso 1 IsHeapHomIsoΣ $ isPropΠ3 λ _ _ _ → H' .is-set _ _ + where open HeapStr + +IsHeapEquiv : {X : Type ℓ} {Y : Type ℓ'} (H : HeapStr X) (e : X ≃ Y) (H' : HeapStr Y) → Type _ +IsHeapEquiv H e H' = IsHeapHom H (e .fst) H' + +HeapEquiv : (H : Heap ℓ) (H' : Heap ℓ') → Type _ +HeapEquiv H H' = Σ[ e ∈ ⟨ H ⟩ ≃ ⟨ H' ⟩ ] IsHeapEquiv (str H) e (str H') + +𝒮ᴰ-Heap : DUARel (𝒮-Univ ℓ) HeapStr ℓ +𝒮ᴰ-Heap = 𝒮ᴰ-Record (𝒮-Univ _) IsHeapEquiv + (fields: + data[ [_,_,_] ∣ autoDUARel _ _ ∣ pres-[] ] + prop[ isHeap ∣ (λ _ _ → isPropIsHeap _) ]) + where + open HeapStr + open IsHeapHom + +HeapPath : (H H' : Heap ℓ) → HeapEquiv H H' ≃ (H ≡ H') +HeapPath = ∫ 𝒮ᴰ-Heap .UARel.ua + +uaHeap : {H H' : Heap ℓ} → HeapEquiv H H' → H ≡ H' +uaHeap = HeapPath _ _ .fst diff --git a/Cubical/Algebra/Heap/Properties.agda b/Cubical/Algebra/Heap/Properties.agda new file mode 100644 index 0000000000..c4e05fe238 --- /dev/null +++ b/Cubical/Algebra/Heap/Properties.agda @@ -0,0 +1,149 @@ +{-- +Defines the structure group of a heap, +proves that a group is equivalently a pointed heap. +TODO: A heap is equivalently a group equipped with a torsor +--} + +module Cubical.Algebra.Heap.Properties where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Function +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Univalence +open import Cubical.Foundations.Structure + +open import Cubical.HITs.PropositionalTruncation as PT + +open import Cubical.Algebra.Group +open import Cubical.Algebra.Group.Morphisms +open import Cubical.Algebra.Group.MorphismProperties +open import Cubical.Algebra.Group.GroupPath + +open import Cubical.Algebra.Heap.Base + +private variable + ℓ : Level + +module _ (G : Group ℓ) where + open HeapStr + open IsHeap + open GroupStr (snd G) renaming (is-set to G-is-set) + + GroupHasHeapStr : HeapStr ⟨ G ⟩ + GroupHasHeapStr .[_,_,_] a b c = a · inv b · c + GroupHasHeapStr .isHeap .is-set = G-is-set + GroupHasHeapStr .isHeap .assoc a b c d e = ·Assoc a (inv b) (c · inv d · e) ∙∙ ·Assoc (a · inv b) c (inv d · e) ∙∙ congL _·_ (sym (·Assoc a (inv b) c)) + GroupHasHeapStr .isHeap .idl a b = ·GroupAutomorphismL G a .Iso.rightInv b + GroupHasHeapStr .isHeap .idr a b = congR _·_ (·InvL b) ∙ ·IdR a + GroupHasHeapStr .isHeap .inhab = ∣ 1g ∣₁ + + GroupHeap : Heap ℓ + GroupHeap = ⟨ G ⟩ , GroupHasHeapStr + +module HeapTheory (H : Heap ℓ) where + open HeapStr (snd H) public + + wriggle : ∀ a b c d → [ [ a , b , c ] , d , [ d , c , b ] ] ≡ a + wriggle a b c d = + [ [ a , b , c ] , d , [ d , c , b ] ] ≡⟨ assoc [ a , b , c ] d d c b ⟩ + [ [ [ a , b , c ] , d , d ] , c , b ] ≡⟨ cong [_, c , b ] (idr [ a , b , c ] d) ⟩ + [ [ a , b , c ] , c , b ] ≡⟨ sym (assoc a b c c b) ⟩ + [ a , b , [ c , c , b ] ] ≡⟨ cong [ a , b ,_] (idl c b) ⟩ + [ a , b , b ] ≡⟨ idr a b ⟩ + a ∎ + + assocl : ∀ a b c d e → [ a , [ d , c , b ] , e ] ≡ [ [ a , b , c ] , d , e ] + assocl a b c d e = + [ a , [ d , c , b ] , e ] ≡⟨ cong [_, [ d , c , b ] , e ] (sym (wriggle a b c d)) ⟩ + [ [ [ a , b , c ] , d , [ d , c , b ] ] , [ d , c , b ] , e ] ≡⟨ sym (assoc [ a , b , c ] d [ d , c , b ] [ d , c , b ] e) ⟩ + [ [ a , b , c ] , d , [ [ d , c , b ] , [ d , c , b ] , e ] ] ≡⟨ cong [ [ a , b , c ] , d ,_] (idl [ d , c , b ] e) ⟩ + [ [ a , b , c ] , d , e ] ∎ + + assocr : ∀ a b c d e → [ a , [ d , c , b ] , e ] ≡ [ a , b , [ c , d , e ] ] + assocr a b c d e = + [ a , [ d , c , b ] , e ] ≡⟨ assocl a b c d e ⟩ + [ [ a , b , c ] , d , e ] ≡⟨ sym (assoc a b c d e) ⟩ + [ a , b , [ c , d , e ] ] ∎ + + idlr : ∀ a b c → [ a , [ b , c , a ] , b ] ≡ c + idlr a b c = + [ a , [ b , c , a ] , b ] ≡⟨ assocr a a c b b ⟩ + [ a , a , [ c , b , b ] ] ≡⟨ idl a [ c , b , b ] ⟩ + [ c , b , b ] ≡⟨ idr c b ⟩ + c ∎ + +StructureGroup : Heap ℓ → Group ℓ +StructureGroup H = toldYaSo inhab module StructureGroup where + open GroupStr hiding (is-set) + open HeapTheory H + + fromPoint : ⟨ H ⟩ → Group _ + fromPoint e .fst = ⟨ H ⟩ + fromPoint e .snd .1g = e + fromPoint e .snd ._·_ a b = [ a , e , b ] + fromPoint e .snd .inv a = [ e , a , e ] + fromPoint e .snd .isGroup = makeIsGroup is-set + (λ x y z → assoc x e y e z) + (λ x → idr x e) -- is that a maybeJosiah reference + (λ x → idl e x) + (λ x → assoc x e e x e ∙∙ cong [_, x , e ] (idr x e) ∙∙ idl x e) + (λ x → sym (assoc e x e e x) ∙∙ cong [ e , x ,_] (idl e x) ∙∙ idr e x) + + φ : ∀ e e' → GroupHom (fromPoint e) (fromPoint e') + φ e e' .fst x = [ e' , e , x ] + φ e e' .snd = makeIsGroupHom λ x y → + [ e' , e , [ x , e , y ] ] ≡⟨ assoc e' e x e y ⟩ + [ [ e' , e , x ] , e , y ] ≡⟨ cong [ [ e' , e , x ] ,_, y ] (sym (idr e e')) ⟩ + [ [ e' , e , x ] , [ e , e' , e' ] , y ] ≡⟨ assocr [ e' , e , x ] e' e' e y ⟩ + [ [ e' , e , x ] , e' , [ e' , e , y ] ] ∎ + + φ-coh : ∀ e e' e'' x → φ e' e'' .fst (φ e e' .fst x) ≡ φ e e'' .fst x + φ-coh e e' e'' x = + [ e'' , e' , [ e' , e , x ] ] ≡⟨ sym (assocr e'' e' e' e x) ⟩ + [ e'' , [ e , e' , e' ] , x ] ≡⟨ cong [ e'' ,_, x ] (idr e e') ⟩ + [ e'' , e , x ] ∎ + + φ-eqv : ∀ e e' → isEquiv (φ e e' .fst) + φ-eqv e e' = isoToIsEquiv (iso (φ e e' .fst) (φ e' e .fst) (lemma e e') (lemma e' e)) where + + lemma : ∀ e e' x → φ e e' .fst (φ e' e .fst x) ≡ x + lemma e e' x = φ-coh e' e e' x ∙ idl e' x + + toldYaSo : ∥ ⟨ H ⟩ ∥₁ → Group _ + toldYaSo = PropTrunc→Group fromPoint (λ e e' → (φ e e' .fst , φ-eqv e e') , φ e e' .snd) φ-coh + +StructureGroupOfGroupHeap : (G : Group ℓ) → GroupEquiv (StructureGroup (GroupHeap G)) G +StructureGroupOfGroupHeap G = idEquiv _ , makeIsGroupHom λ x y → congR _·_ $ congL _·_ inv1g ∙ ·IdL y + where open GroupStr (G .snd); open GroupTheory G + +GroupHeapOfStructureGroup : (H : Heap ℓ) → ∥ HeapEquiv (GroupHeap (StructureGroup H)) H ∥₁ -- unnatural isomorphism +GroupHeapOfStructureGroup H = go inhab module GroupHeapOfStructureGroup where + open HeapTheory H + + fromPoint : (e : ⟨ H ⟩) → HeapEquiv (GroupHeap (StructureGroup.fromPoint H e)) H + fromPoint e = idEquiv _ , makeIsHeapHom λ a b c → + [ a , e , [ [ e , b , e ] , e , c ] ] ≡⟨ cong [ a , e ,_] (sym (assoc e b e e c)) ⟩ + [ a , e , [ e , b , [ e , e , c ] ] ] ≡⟨ cong [ a , e ,_] (cong [ e , b ,_] (idl e c)) ⟩ + [ a , e , [ e , b , c ] ] ≡⟨ assoc a e e b c ⟩ + [ [ a , e , e ] , b , c ] ≡⟨ cong [_, b , c ] (idr a e) ⟩ + [ a , b , c ] ∎ + + go : (p : ∥ ⟨ H ⟩ ∥₁) → ∥ HeapEquiv (GroupHeap (StructureGroup.toldYaSo H p)) H ∥₁ + go = PT.elim (λ _ → isPropPropTrunc) λ e → ∣ fromPoint e ∣₁ + +PointedHeap : ∀ ℓ → Type (ℓ-suc ℓ) +PointedHeap ℓ = Σ[ H ∈ Heap ℓ ] ⟨ H ⟩ + +PointedHeap≡ : {(H , e) (H' , e') : PointedHeap ℓ} (eqv : HeapEquiv H H') (p : eqv .fst .fst e ≡ e') → (H , e) ≡ (H' , e') +PointedHeap≡ eqv p = cong₂ _,_ (uaHeap eqv) (ua-gluePath _ p) + +GroupsArePointedHeaps : Group ℓ ≃ PointedHeap ℓ +GroupsArePointedHeaps {ℓ} = isoToEquiv asIso module GroupsArePointedHeaps where + open Iso + + asIso : Iso (Group ℓ) (PointedHeap ℓ) + asIso .fun G = GroupHeap G , G .snd .GroupStr.1g + asIso .inv (H , e) = StructureGroup.fromPoint H e + asIso .rightInv (H , e) = PointedHeap≡ (GroupHeapOfStructureGroup.fromPoint H e) refl + asIso .leftInv G = uaGroup (StructureGroupOfGroupHeap G) From c2aa3e83ab7ad60dea35d52305d8d773bf1656fb Mon Sep 17 00:00:00 2001 From: anshwad10 <109362320+anshwad10@users.noreply.github.com> Date: Sat, 22 Nov 2025 21:52:17 +0530 Subject: [PATCH 2/5] appease the whitespace gods --- Cubical/Algebra/Heap/Properties.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Cubical/Algebra/Heap/Properties.agda b/Cubical/Algebra/Heap/Properties.agda index c4e05fe238..b0ef720b64 100644 --- a/Cubical/Algebra/Heap/Properties.agda +++ b/Cubical/Algebra/Heap/Properties.agda @@ -92,14 +92,14 @@ StructureGroup H = toldYaSo inhab module StructureGroup where φ : ∀ e e' → GroupHom (fromPoint e) (fromPoint e') φ e e' .fst x = [ e' , e , x ] - φ e e' .snd = makeIsGroupHom λ x y → + φ e e' .snd = makeIsGroupHom λ x y → [ e' , e , [ x , e , y ] ] ≡⟨ assoc e' e x e y ⟩ [ [ e' , e , x ] , e , y ] ≡⟨ cong [ [ e' , e , x ] ,_, y ] (sym (idr e e')) ⟩ [ [ e' , e , x ] , [ e , e' , e' ] , y ] ≡⟨ assocr [ e' , e , x ] e' e' e y ⟩ [ [ e' , e , x ] , e' , [ e' , e , y ] ] ∎ φ-coh : ∀ e e' e'' x → φ e' e'' .fst (φ e e' .fst x) ≡ φ e e'' .fst x - φ-coh e e' e'' x = + φ-coh e e' e'' x = [ e'' , e' , [ e' , e , x ] ] ≡⟨ sym (assocr e'' e' e' e x) ⟩ [ e'' , [ e , e' , e' ] , x ] ≡⟨ cong [ e'' ,_, x ] (idr e e') ⟩ [ e'' , e , x ] ∎ @@ -141,7 +141,7 @@ PointedHeap≡ eqv p = cong₂ _,_ (uaHeap eqv) (ua-gluePath _ p) GroupsArePointedHeaps : Group ℓ ≃ PointedHeap ℓ GroupsArePointedHeaps {ℓ} = isoToEquiv asIso module GroupsArePointedHeaps where open Iso - + asIso : Iso (Group ℓ) (PointedHeap ℓ) asIso .fun G = GroupHeap G , G .snd .GroupStr.1g asIso .inv (H , e) = StructureGroup.fromPoint H e From 35e2752848b78542b33b6e12c6f5cee139615f7e Mon Sep 17 00:00:00 2001 From: anshwad10 <109362320+anshwad10@users.noreply.github.com> Date: Sat, 22 Nov 2025 22:08:39 +0530 Subject: [PATCH 3/5] credit where credit is due --- Cubical/Algebra/Heap/Properties.agda | 1 + 1 file changed, 1 insertion(+) diff --git a/Cubical/Algebra/Heap/Properties.agda b/Cubical/Algebra/Heap/Properties.agda index b0ef720b64..4e32a90dca 100644 --- a/Cubical/Algebra/Heap/Properties.agda +++ b/Cubical/Algebra/Heap/Properties.agda @@ -53,6 +53,7 @@ module HeapTheory (H : Heap ℓ) where [ a , b , b ] ≡⟨ idr a b ⟩ a ∎ + -- Wagner's theory of generalized heaps, theorem 8.2.13 assocl : ∀ a b c d e → [ a , [ d , c , b ] , e ] ≡ [ [ a , b , c ] , d , e ] assocl a b c d e = [ a , [ d , c , b ] , e ] ≡⟨ cong [_, [ d , c , b ] , e ] (sym (wriggle a b c d)) ⟩ From 518533e71987b63823471417e1dedc03a7cd5580 Mon Sep 17 00:00:00 2001 From: anshwad10 <109362320+anshwad10@users.noreply.github.com> Date: Sun, 23 Nov 2025 14:27:28 +0530 Subject: [PATCH 4/5] shorten line length --- Cubical/Algebra/Heap/Properties.agda | 51 ++++++++++++++++++---------- 1 file changed, 34 insertions(+), 17 deletions(-) diff --git a/Cubical/Algebra/Heap/Properties.agda b/Cubical/Algebra/Heap/Properties.agda index 4e32a90dca..3989dc7ca9 100644 --- a/Cubical/Algebra/Heap/Properties.agda +++ b/Cubical/Algebra/Heap/Properties.agda @@ -33,7 +33,11 @@ module _ (G : Group ℓ) where GroupHasHeapStr : HeapStr ⟨ G ⟩ GroupHasHeapStr .[_,_,_] a b c = a · inv b · c GroupHasHeapStr .isHeap .is-set = G-is-set - GroupHasHeapStr .isHeap .assoc a b c d e = ·Assoc a (inv b) (c · inv d · e) ∙∙ ·Assoc (a · inv b) c (inv d · e) ∙∙ congL _·_ (sym (·Assoc a (inv b) c)) + GroupHasHeapStr .isHeap .assoc a b c d e = + a · inv b · c · inv d · e ≡⟨ ·Assoc a (inv b) (c · inv d · e) ⟩ + (a · inv b) · c · inv d · e ≡⟨ ·Assoc (a · inv b) c (inv d · e) ⟩ + ((a · inv b) · c) · inv d · e ≡⟨ congL _·_ (sym (·Assoc a (inv b) c)) ⟩ + (a · inv b · c) · inv d · e ∎ GroupHasHeapStr .isHeap .idl a b = ·GroupAutomorphismL G a .Iso.rightInv b GroupHasHeapStr .isHeap .idr a b = congR _·_ (·InvL b) ∙ ·IdR a GroupHasHeapStr .isHeap .inhab = ∣ 1g ∣₁ @@ -56,10 +60,12 @@ module HeapTheory (H : Heap ℓ) where -- Wagner's theory of generalized heaps, theorem 8.2.13 assocl : ∀ a b c d e → [ a , [ d , c , b ] , e ] ≡ [ [ a , b , c ] , d , e ] assocl a b c d e = - [ a , [ d , c , b ] , e ] ≡⟨ cong [_, [ d , c , b ] , e ] (sym (wriggle a b c d)) ⟩ - [ [ [ a , b , c ] , d , [ d , c , b ] ] , [ d , c , b ] , e ] ≡⟨ sym (assoc [ a , b , c ] d [ d , c , b ] [ d , c , b ] e) ⟩ - [ [ a , b , c ] , d , [ [ d , c , b ] , [ d , c , b ] , e ] ] ≡⟨ cong [ [ a , b , c ] , d ,_] (idl [ d , c , b ] e) ⟩ - [ [ a , b , c ] , d , e ] ∎ + [ a , [ d , c , b ] , e ] ≡⟨ cong [_, [ d , c , b ] , e ] (sym (wriggle a b c d)) ⟩ + [ [ [ a , b , c ] , d , [ d , c , b ] ] , [ d , c , b ] , e ] + ≡⟨ sym (assoc [ a , b , c ] d [ d , c , b ] [ d , c , b ] e) ⟩ + [ [ a , b , c ] , d , [ [ d , c , b ] , [ d , c , b ] , e ] ] + ≡⟨ cong [ [ a , b , c ] , d ,_] (idl [ d , c , b ] e) ⟩ + [ [ a , b , c ] , d , e ] ∎ assocr : ∀ a b c d e → [ a , [ d , c , b ] , e ] ≡ [ a , b , [ c , d , e ] ] assocr a b c d e = @@ -75,7 +81,8 @@ module HeapTheory (H : Heap ℓ) where c ∎ StructureGroup : Heap ℓ → Group ℓ -StructureGroup H = toldYaSo inhab module StructureGroup where +StructureGroup H = go inhab + module StructureGroup where open GroupStr hiding (is-set) open HeapTheory H @@ -86,7 +93,7 @@ StructureGroup H = toldYaSo inhab module StructureGroup where fromPoint e .snd .inv a = [ e , a , e ] fromPoint e .snd .isGroup = makeIsGroup is-set (λ x y z → assoc x e y e z) - (λ x → idr x e) -- is that a maybeJosiah reference + (λ x → idr x e) (λ x → idl e x) (λ x → assoc x e e x e ∙∙ cong [_, x , e ] (idr x e) ∙∙ idl x e) (λ x → sym (assoc e x e e x) ∙∙ cong [ e , x ,_] (idl e x) ∙∙ idr e x) @@ -95,7 +102,7 @@ StructureGroup H = toldYaSo inhab module StructureGroup where φ e e' .fst x = [ e' , e , x ] φ e e' .snd = makeIsGroupHom λ x y → [ e' , e , [ x , e , y ] ] ≡⟨ assoc e' e x e y ⟩ - [ [ e' , e , x ] , e , y ] ≡⟨ cong [ [ e' , e , x ] ,_, y ] (sym (idr e e')) ⟩ + [ [ e' , e , x ] , e , y ] ≡⟨ congR [_,_, y ] (sym (idr e e')) ⟩ [ [ e' , e , x ] , [ e , e' , e' ] , y ] ≡⟨ assocr [ e' , e , x ] e' e' e y ⟩ [ [ e' , e , x ] , e' , [ e' , e , y ] ] ∎ @@ -111,15 +118,24 @@ StructureGroup H = toldYaSo inhab module StructureGroup where lemma : ∀ e e' x → φ e e' .fst (φ e' e .fst x) ≡ x lemma e e' x = φ-coh e' e e' x ∙ idl e' x - toldYaSo : ∥ ⟨ H ⟩ ∥₁ → Group _ - toldYaSo = PropTrunc→Group fromPoint (λ e e' → (φ e e' .fst , φ-eqv e e') , φ e e' .snd) φ-coh + go : ∥ ⟨ H ⟩ ∥₁ → Group _ + go = PropTrunc→Group fromPoint (λ e e' → (φ e e' .fst , φ-eqv e e') , φ e e' .snd) φ-coh StructureGroupOfGroupHeap : (G : Group ℓ) → GroupEquiv (StructureGroup (GroupHeap G)) G -StructureGroupOfGroupHeap G = idEquiv _ , makeIsGroupHom λ x y → congR _·_ $ congL _·_ inv1g ∙ ·IdL y - where open GroupStr (G .snd); open GroupTheory G - -GroupHeapOfStructureGroup : (H : Heap ℓ) → ∥ HeapEquiv (GroupHeap (StructureGroup H)) H ∥₁ -- unnatural isomorphism -GroupHeapOfStructureGroup H = go inhab module GroupHeapOfStructureGroup where +StructureGroupOfGroupHeap G = idEquiv _ , makeIsGroupHom λ x y → + [ x , 1g , y ] ≡⟨⟩ + x · inv 1g · y ≡⟨ congR _·_ (congL _·_ inv1g) ⟩ + x · 1g · y ≡⟨ congR _·_ (·IdL y) ⟩ + x · y ∎ + where + open GroupStr (G .snd) + open GroupTheory G + open HeapTheory (GroupHeap G) + +GroupHeapOfStructureGroup : (H : Heap ℓ) + → ∥ HeapEquiv (GroupHeap (StructureGroup H)) H ∥₁ -- unnatural isomorphism +GroupHeapOfStructureGroup H = go inhab + module GroupHeapOfStructureGroup where open HeapTheory H fromPoint : (e : ⟨ H ⟩) → HeapEquiv (GroupHeap (StructureGroup.fromPoint H e)) H @@ -130,13 +146,14 @@ GroupHeapOfStructureGroup H = go inhab module GroupHeapOfStructureGroup where [ [ a , e , e ] , b , c ] ≡⟨ cong [_, b , c ] (idr a e) ⟩ [ a , b , c ] ∎ - go : (p : ∥ ⟨ H ⟩ ∥₁) → ∥ HeapEquiv (GroupHeap (StructureGroup.toldYaSo H p)) H ∥₁ + go : (p : ∥ ⟨ H ⟩ ∥₁) → ∥ HeapEquiv (GroupHeap (StructureGroup.go H p)) H ∥₁ go = PT.elim (λ _ → isPropPropTrunc) λ e → ∣ fromPoint e ∣₁ PointedHeap : ∀ ℓ → Type (ℓ-suc ℓ) PointedHeap ℓ = Σ[ H ∈ Heap ℓ ] ⟨ H ⟩ -PointedHeap≡ : {(H , e) (H' , e') : PointedHeap ℓ} (eqv : HeapEquiv H H') (p : eqv .fst .fst e ≡ e') → (H , e) ≡ (H' , e') +PointedHeap≡ : {(H , e) (H' , e') : PointedHeap ℓ} (eqv : HeapEquiv H H') (p : eqv .fst .fst e ≡ e') + → (H , e) ≡ (H' , e') PointedHeap≡ eqv p = cong₂ _,_ (uaHeap eqv) (ua-gluePath _ p) GroupsArePointedHeaps : Group ℓ ≃ PointedHeap ℓ From 688e8af1f3373bc1cbad1c3e295794c7f4d9d3c3 Mon Sep 17 00:00:00 2001 From: anshwad10 <109362320+anshwad10@users.noreply.github.com> Date: Sun, 23 Nov 2025 14:31:17 +0530 Subject: [PATCH 5/5] fix line length --- Cubical/Algebra/Heap/Base.agda | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/Cubical/Algebra/Heap/Base.agda b/Cubical/Algebra/Heap/Base.agda index 000858d0de..894c5b4c2d 100644 --- a/Cubical/Algebra/Heap/Base.agda +++ b/Cubical/Algebra/Heap/Base.agda @@ -45,7 +45,9 @@ record HeapStr (H : Type ℓ) : Type ℓ where Heap : ∀ ℓ → Type (ℓ-suc ℓ) Heap ℓ = TypeWithStr ℓ HeapStr -record IsHeapHom {X : Type ℓ} {Y : Type ℓ'} (H : HeapStr X) (f : X → Y) (H' : HeapStr Y) : Type (ℓ-max ℓ ℓ') where +record IsHeapHom {X : Type ℓ} {Y : Type ℓ'} (H : HeapStr X) (f : X → Y) (H' : HeapStr Y) + : Type (ℓ-max ℓ ℓ') where + constructor makeIsHeapHom private @@ -58,10 +60,14 @@ unquoteDecl IsHeapHomIsoΣ = declareRecordIsoΣ IsHeapHomIsoΣ (quote IsHeapHom) isPropIsHeap : {H : Type ℓ} ([_,_,_] : H → H → H → H) → isProp (IsHeap [_,_,_]) isPropIsHeap [_,_,_] = isOfHLevelRetractFromIso 1 IsHeapIsoΣ $ isPropΣ isPropIsSet λ is-set → - isProp×3 (isPropΠ5 (λ _ _ _ _ _ → is-set _ _)) (isPropΠ2 λ _ _ → is-set _ _) (isPropΠ2 λ _ _ → is-set _ _) isPropPropTrunc + isProp×3 (isPropΠ5 λ _ _ _ _ _ → is-set _ _) + (isPropΠ2 λ _ _ → is-set _ _) + (isPropΠ2 λ _ _ → is-set _ _) + isPropPropTrunc isPropIsHeapHom : (H : HeapStr X) (f : X → Y) (H' : HeapStr Y) → isProp (IsHeapHom H f H') -isPropIsHeapHom H f H' = isOfHLevelRetractFromIso 1 IsHeapHomIsoΣ $ isPropΠ3 λ _ _ _ → H' .is-set _ _ +isPropIsHeapHom H f H' = isOfHLevelRetractFromIso 1 IsHeapHomIsoΣ $ + isPropΠ3 λ _ _ _ → H' .is-set _ _ where open HeapStr IsHeapEquiv : {X : Type ℓ} {Y : Type ℓ'} (H : HeapStr X) (e : X ≃ Y) (H' : HeapStr Y) → Type _