Skip to content

Commit 9ef8c26

Browse files
anshwad10anshwad10
committed
Heap!
I wonder if I should rename this to groud
1 parent d569148 commit 9ef8c26

File tree

3 files changed

+239
-0
lines changed

3 files changed

+239
-0
lines changed

‎Cubical/Algebra/Heap.agda‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
module Cubical.Algebra.Heap where
2+
3+
open import Cubical.Algebra.Heap.Base public
4+
open import Cubical.Algebra.Heap.Properties public

‎Cubical/Algebra/Heap/Base.agda‎

Lines changed: 86 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,86 @@
1+
module Cubical.Algebra.Heap.Base where
2+
3+
open import Cubical.Foundations.Prelude
4+
open import Cubical.Foundations.Equiv
5+
open import Cubical.Foundations.HLevels
6+
open import Cubical.Foundations.Function
7+
open import Cubical.Foundations.Isomorphism
8+
open import Cubical.Foundations.SIP
9+
10+
open import Cubical.Reflection.RecordEquiv
11+
12+
open import Cubical.Displayed.Base
13+
open import Cubical.Displayed.Auto
14+
open import Cubical.Displayed.Record
15+
open import Cubical.Displayed.Universe
16+
17+
open import Cubical.HITs.PropositionalTruncation
18+
19+
private variable
20+
ℓ ℓ' : Level
21+
X Y : Type ℓ
22+
23+
record IsHeap {H : Type ℓ} ([_,_,_] : H → H → H → H) : Type ℓ where
24+
no-eta-equality
25+
constructor isheap
26+
27+
field
28+
is-set : isSet H
29+
assoc : ∀ a b c d e → [ a , b , [ c , d , e ] ] ≡ [ [ a , b , c ] , d , e ]
30+
idl : ∀ a b → [ a , a , b ] ≡ b
31+
idr : ∀ a b → [ a , b , b ] ≡ a
32+
inhab : ∥ H ∥₁
33+
34+
unquoteDecl IsHeapIsoΣ = declareRecordIsoΣ IsHeapIsoΣ (quote IsHeap)
35+
36+
record HeapStr (H : Type ℓ) : Type ℓ where
37+
constructor heapstr
38+
39+
field
40+
[_,_,_] : H → H → H → H
41+
isHeap : IsHeap [_,_,_]
42+
43+
open IsHeap isHeap public
44+
45+
Heap : ∀ ℓ → Type (ℓ-suc ℓ)
46+
Heap ℓ = TypeWithStr ℓ HeapStr
47+
48+
record IsHeapHom {X : Type ℓ} {Y : Type ℓ'} (H : HeapStr X) (f : X → Y) (H' : HeapStr Y) : Type (ℓ-max ℓ ℓ') where
49+
constructor makeIsHeapHom
50+
51+
private
52+
module H = HeapStr H
53+
module H' = HeapStr H'
54+
field
55+
pres-[] : (a b c : X) → f H.[ a , b , c ] ≡ H'.[ f a , f b , f c ]
56+
57+
unquoteDecl IsHeapHomIsoΣ = declareRecordIsoΣ IsHeapHomIsoΣ (quote IsHeapHom)
58+
59+
isPropIsHeap : {H : Type ℓ} ([_,_,_] : H → H → H → H) → isProp (IsHeap [_,_,_])
60+
isPropIsHeap [_,_,_] = isOfHLevelRetractFromIso 1 IsHeapIsoΣ $ isPropΣ isPropIsSet λ is-set →
61+
isProp×3 (isPropΠ5 (λ _ _ _ _ _ → is-set _ _)) (isPropΠ2 λ _ _ → is-set _ _) (isPropΠ2 λ _ _ → is-set _ _) isPropPropTrunc
62+
63+
isPropIsHeapHom : (H : HeapStr X) (f : X → Y) (H' : HeapStr Y) → isProp (IsHeapHom H f H')
64+
isPropIsHeapHom H f H' = isOfHLevelRetractFromIso 1 IsHeapHomIsoΣ $ isPropΠ3 λ _ _ _ → H' .is-set _ _
65+
where open HeapStr
66+
67+
IsHeapEquiv : {X : Type ℓ} {Y : Type ℓ'} (H : HeapStr X) (e : X ≃ Y) (H' : HeapStr Y) → Type _
68+
IsHeapEquiv H e H' = IsHeapHom H (e .fst) H'
69+
70+
HeapEquiv : (H : Heap ℓ) (H' : Heap ℓ') → Type _
71+
HeapEquiv H H' = Σ[ e ∈ ⟨ H ⟩ ≃ ⟨ H' ⟩ ] IsHeapEquiv (str H) e (str H')
72+
73+
𝒮ᴰ-Heap : DUARel (𝒮-Univ ℓ) HeapStr ℓ
74+
𝒮ᴰ-Heap = 𝒮ᴰ-Record (𝒮-Univ _) IsHeapEquiv
75+
(fields:
76+
data[ [_,_,_] ∣ autoDUARel _ _ ∣ pres-[] ]
77+
prop[ isHeap ∣ (λ _ _ → isPropIsHeap _) ])
78+
where
79+
open HeapStr
80+
open IsHeapHom
81+
82+
HeapPath : (H H' : Heap ℓ) → HeapEquiv H H' ≃ (H ≡ H')
83+
HeapPath = ∫ 𝒮ᴰ-Heap .UARel.ua
84+
85+
uaHeap : {H H' : Heap ℓ} → HeapEquiv H H' → H ≡ H'
86+
uaHeap = HeapPath _ _ .fst

‎Cubical/Algebra/Heap/Properties.agda‎

Lines changed: 149 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,149 @@
1+
{--
2+
Defines the structure group of a heap,
3+
proves that a group is equivalently a pointed heap.
4+
TODO: A heap is equivalently a group equipped with a torsor
5+
--}
6+
7+
module Cubical.Algebra.Heap.Properties where
8+
9+
open import Cubical.Foundations.Prelude
10+
open import Cubical.Foundations.Equiv
11+
open import Cubical.Foundations.Function
12+
open import Cubical.Foundations.Isomorphism
13+
open import Cubical.Foundations.Univalence
14+
open import Cubical.Foundations.Structure
15+
16+
open import Cubical.HITs.PropositionalTruncation as PT
17+
18+
open import Cubical.Algebra.Group
19+
open import Cubical.Algebra.Group.Morphisms
20+
open import Cubical.Algebra.Group.MorphismProperties
21+
open import Cubical.Algebra.Group.GroupPath
22+
23+
open import Cubical.Algebra.Heap.Base
24+
25+
private variable
26+
ℓ : Level
27+
28+
module _ (G : Group ℓ) where
29+
open HeapStr
30+
open IsHeap
31+
open GroupStr (snd G) renaming (is-set to G-is-set)
32+
33+
GroupHasHeapStr : HeapStr ⟨ G ⟩
34+
GroupHasHeapStr .[_,_,_] a b c = a · inv b · c
35+
GroupHasHeapStr .isHeap .is-set = G-is-set
36+
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))
37+
GroupHasHeapStr .isHeap .idl a b = ·GroupAutomorphismL G a .Iso.rightInv b
38+
GroupHasHeapStr .isHeap .idr a b = congR _·_ (·InvL b) ∙ ·IdR a
39+
GroupHasHeapStr .isHeap .inhab = ∣ 1g ∣₁
40+
41+
GroupHeap : Heap ℓ
42+
GroupHeap = ⟨ G ⟩ , GroupHasHeapStr
43+
44+
module HeapTheory (H : Heap ℓ) where
45+
open HeapStr (snd H) public
46+
47+
wriggle : ∀ a b c d → [ [ a , b , c ] , d , [ d , c , b ] ] ≡ a
48+
wriggle a b c d =
49+
[ [ a , b , c ] , d , [ d , c , b ] ] ≡⟨ assoc [ a , b , c ] d d c b ⟩
50+
[ [ [ a , b , c ] , d , d ] , c , b ] ≡⟨ cong [_, c , b ] (idr [ a , b , c ] d) ⟩
51+
[ [ a , b , c ] , c , b ] ≡⟨ sym (assoc a b c c b) ⟩
52+
[ a , b , [ c , c , b ] ] ≡⟨ cong [ a , b ,_] (idl c b) ⟩
53+
[ a , b , b ] ≡⟨ idr a b ⟩
54+
a ∎
55+
56+
assocl : ∀ a b c d e → [ a , [ d , c , b ] , e ] ≡ [ [ a , b , c ] , d , e ]
57+
assocl a b c d e =
58+
[ a , [ d , c , b ] , e ] ≡⟨ cong [_, [ d , c , b ] , e ] (sym (wriggle a b c d)) ⟩
59+
[ [ [ a , b , c ] , d , [ d , c , b ] ] , [ d , c , b ] , e ] ≡⟨ sym (assoc [ a , b , c ] d [ d , c , b ] [ d , c , b ] e) ⟩
60+
[ [ a , b , c ] , d , [ [ d , c , b ] , [ d , c , b ] , e ] ] ≡⟨ cong [ [ a , b , c ] , d ,_] (idl [ d , c , b ] e) ⟩
61+
[ [ a , b , c ] , d , e ] ∎
62+
63+
assocr : ∀ a b c d e → [ a , [ d , c , b ] , e ] ≡ [ a , b , [ c , d , e ] ]
64+
assocr a b c d e =
65+
[ a , [ d , c , b ] , e ] ≡⟨ assocl a b c d e ⟩
66+
[ [ a , b , c ] , d , e ] ≡⟨ sym (assoc a b c d e) ⟩
67+
[ a , b , [ c , d , e ] ] ∎
68+
69+
idlr : ∀ a b c → [ a , [ b , c , a ] , b ] ≡ c
70+
idlr a b c =
71+
[ a , [ b , c , a ] , b ] ≡⟨ assocr a a c b b ⟩
72+
[ a , a , [ c , b , b ] ] ≡⟨ idl a [ c , b , b ] ⟩
73+
[ c , b , b ] ≡⟨ idr c b ⟩
74+
c ∎
75+
76+
StructureGroup : Heap ℓ → Group ℓ
77+
StructureGroup H = toldYaSo inhab module StructureGroup where
78+
open GroupStr hiding (is-set)
79+
open HeapTheory H
80+
81+
fromPoint : ⟨ H ⟩ → Group _
82+
fromPoint e .fst = ⟨ H ⟩
83+
fromPoint e .snd .1g = e
84+
fromPoint e .snd ._·_ a b = [ a , e , b ]
85+
fromPoint e .snd .inv a = [ e , a , e ]
86+
fromPoint e .snd .isGroup = makeIsGroup is-set
87+
(λ x y z → assoc x e y e z)
88+
(λ x → idr x e) -- is that a maybeJosiah reference
89+
(λ x → idl e x)
90+
(λ x → assoc x e e x e ∙∙ cong [_, x , e ] (idr x e) ∙∙ idl x e)
91+
(λ x → sym (assoc e x e e x) ∙∙ cong [ e , x ,_] (idl e x) ∙∙ idr e x)
92+
93+
φ : ∀ e e' → GroupHom (fromPoint e) (fromPoint e')
94+
φ e e' .fst x = [ e' , e , x ]
95+
φ e e' .snd = makeIsGroupHom λ x y →
96+
[ e' , e , [ x , e , y ] ] ≡⟨ assoc e' e x e y ⟩
97+
[ [ e' , e , x ] , e , y ] ≡⟨ cong [ [ e' , e , x ] ,_, y ] (sym (idr e e')) ⟩
98+
[ [ e' , e , x ] , [ e , e' , e' ] , y ] ≡⟨ assocr [ e' , e , x ] e' e' e y ⟩
99+
[ [ e' , e , x ] , e' , [ e' , e , y ] ] ∎
100+
101+
φ-coh : ∀ e e' e'' x → φ e' e'' .fst (φ e e' .fst x) ≡ φ e e'' .fst x
102+
φ-coh e e' e'' x =
103+
[ e'' , e' , [ e' , e , x ] ] ≡⟨ sym (assocr e'' e' e' e x) ⟩
104+
[ e'' , [ e , e' , e' ] , x ] ≡⟨ cong [ e'' ,_, x ] (idr e e') ⟩
105+
[ e'' , e , x ] ∎
106+
107+
φ-eqv : ∀ e e' → isEquiv (φ e e' .fst)
108+
φ-eqv e e' = isoToIsEquiv (iso (φ e e' .fst) (φ e' e .fst) (lemma e e') (lemma e' e)) where
109+
110+
lemma : ∀ e e' x → φ e e' .fst (φ e' e .fst x) ≡ x
111+
lemma e e' x = φ-coh e' e e' x ∙ idl e' x
112+
113+
toldYaSo : ∥ ⟨ H ⟩ ∥₁ → Group _
114+
toldYaSo = PropTrunc→Group fromPoint (λ e e' → (φ e e' .fst , φ-eqv e e') , φ e e' .snd) φ-coh
115+
116+
StructureGroupOfGroupHeap : (G : Group ℓ) → GroupEquiv (StructureGroup (GroupHeap G)) G
117+
StructureGroupOfGroupHeap G = idEquiv _ , makeIsGroupHom λ x y → congR _·_ $ congL _·_ inv1g ∙ ·IdL y
118+
where open GroupStr (G .snd); open GroupTheory G
119+
120+
GroupHeapOfStructureGroup : (H : Heap ℓ) → ∥ HeapEquiv (GroupHeap (StructureGroup H)) H ∥₁ -- unnatural isomorphism
121+
GroupHeapOfStructureGroup H = go inhab module GroupHeapOfStructureGroup where
122+
open HeapTheory H
123+
124+
fromPoint : (e : ⟨ H ⟩) → HeapEquiv (GroupHeap (StructureGroup.fromPoint H e)) H
125+
fromPoint e = idEquiv _ , makeIsHeapHom λ a b c →
126+
[ a , e , [ [ e , b , e ] , e , c ] ] ≡⟨ cong [ a , e ,_] (sym (assoc e b e e c)) ⟩
127+
[ a , e , [ e , b , [ e , e , c ] ] ] ≡⟨ cong [ a , e ,_] (cong [ e , b ,_] (idl e c)) ⟩
128+
[ a , e , [ e , b , c ] ] ≡⟨ assoc a e e b c ⟩
129+
[ [ a , e , e ] , b , c ] ≡⟨ cong [_, b , c ] (idr a e) ⟩
130+
[ a , b , c ] ∎
131+
132+
go : (p : ∥ ⟨ H ⟩ ∥₁) → ∥ HeapEquiv (GroupHeap (StructureGroup.toldYaSo H p)) H ∥₁
133+
go = PT.elim (λ _ → isPropPropTrunc) λ e → ∣ fromPoint e ∣₁
134+
135+
PointedHeap : ∀ ℓ → Type (ℓ-suc ℓ)
136+
PointedHeap ℓ = Σ[ H ∈ Heap ℓ ] ⟨ H ⟩
137+
138+
PointedHeap≡ : {(H , e) (H' , e') : PointedHeap ℓ} (eqv : HeapEquiv H H') (p : eqv .fst .fst e ≡ e') → (H , e) ≡ (H' , e')
139+
PointedHeap≡ eqv p = cong₂ _,_ (uaHeap eqv) (ua-gluePath _ p)
140+
141+
GroupsArePointedHeaps : Group ℓ ≃ PointedHeap ℓ
142+
GroupsArePointedHeaps {ℓ} = isoToEquiv asIso module GroupsArePointedHeaps where
143+
open Iso
144+
145+
asIso : Iso (Group ℓ) (PointedHeap ℓ)
146+
asIso .fun G = GroupHeap G , G .snd .GroupStr.1g
147+
asIso .inv (H , e) = StructureGroup.fromPoint H e
148+
asIso .rightInv (H , e) = PointedHeap≡ (GroupHeapOfStructureGroup.fromPoint H e) refl
149+
asIso .leftInv G = uaGroup (StructureGroupOfGroupHeap G)

0 commit comments

Comments
 (0)