diff --git a/src/AOP/Consistent.agda b/src/AOP/Consistent.agda
new file mode 100644
index 0000000..839d3a0
--- /dev/null
+++ b/src/AOP/Consistent.agda
@@ -0,0 +1,66 @@
+module Consistent where
+
+open import Relation.Binary.PropositionalEquality
+
+infixr 10 _⇒_
+
+-- Propositional formulas
+data Form : Set where
+  𝕡 𝕢   : Form
+  true  : Form
+  false : Form
+  _⇒_   : Form → Form → Form
+
+-- Unit type (from agda-stdlib)
+data ⊤ : Set where tt : ⊤
+
+-- Empty type (from agda-stdlib)
+data ⊥ : Set where
+
+-- Negation type (from agda-stdlib)
+¬_ : Set → Set
+¬ A = A → ⊥
+
+-- Validity of a formula
+-- i.e. `Valid A` means `A` is always true
+Valid : Form → Set
+Valid 𝕡        = ⊥
+Valid 𝕢        = ⊥
+Valid true     = ⊤
+Valid false    = ⊥
+Valid (A ⇒ B)  = Valid A → Valid B
+
+-- Example: formula `𝕡 ⇒ 𝕡` is valid
+id : Valid (𝕡 ⇒ 𝕡)
+id = λ z → z
+
+-- Observe: formula `false` is not valid
+false-not-valid : ¬ (Valid false)
+false-not-valid ()
+
+-- Provability of a formula
+-- i.e. `Proof A` means formula `A` is derivable
+data Proof : Form → Set where
+  T  : Proof true
+  K  : {A B : Form}   → Proof (A ⇒ B ⇒ A)
+  S  : {A B C : Form} → Proof ((A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ (A ⇒ C))
+  MP : {A B : Form}   → Proof (A ⇒ B) → Proof A → Proof B
+
+-- Example: formula `𝕡 ⇒ 𝕡` is provable
+id' : Proof (𝕡 ⇒ 𝕡)
+id' = MP (MP S K) (K {A = 𝕡} {B = 𝕢})
+
+p→v : (f : Form) → Proof f → Valid f
+p→v 𝕡 (MP {A} f x) with l ← p→v (A ⇒ 𝕡) f = l (p→v A x)
+p→v 𝕢 (MP {A} f x) with l ← p→v (A ⇒ 𝕢) f = l (p→v A x)
+p→v true p = tt
+p→v false (MP {A} f x) with l ← p→v (A ⇒ false) f = l (p→v A x)
+p→v (true ⇒ b) K tt vb = tt
+p→v (true ⇒ b) (MP {A} f x) tt with l ← p→v (A ⇒ true ⇒ b) f = l (p→v A x) tt
+p→v ((a ⇒ a') ⇒ b) K va vb va' = va va'
+p→v ((a ⇒ a') ⇒ b) S va vf va' = va va' (vf va')
+p→v ((a ⇒ a') ⇒ b) (MP {A} p q) va with l ← p→v (A ⇒ (a ⇒ a') ⇒ b) p = l (p→v A q) va
+
+-- Show: `false` is not provable
+consistent : ¬ (Proof false)
+consistent x = p→v false x
\ No newline at end of file
diff --git a/src/AOP/NatUIP.agda b/src/AOP/NatUIP.agda
new file mode 100644
index 0000000..8001f24
--- /dev/null
+++ b/src/AOP/NatUIP.agda
@@ -0,0 +1,60 @@
+{-# OPTIONS --safe --without-K #-}
+
+data Nat : Set where
+  zero : Nat
+  suc : Nat → Nat
+
+data _≡_ {A : Set} : A → A → Set where
+  refl : ∀ {x} → x ≡ x
+
+sym : ∀ {A : Set} {x y : A} → x ≡ y → y ≡ x
+sym refl = refl
+
+trans : ∀ {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
+trans refl refl = refl
+
+cong : ∀ {A B x y} (f : A → B) → x ≡ y → f x ≡ f y
+cong f refl = refl
+
+data _≡Nat_ : Nat → Nat → Set where
+  zero : zero ≡Nat zero
+  suc  : ∀ {x y} → x ≡Nat y → suc x ≡Nat suc y
+
+≡Nat-refl : ∀ {x} → x ≡Nat x
+≡Nat-refl {zero} = zero
+≡Nat-refl {suc x} = suc ≡Nat-refl
+
+≡Nat-prop : ∀ {x y} (x≡y₁ x≡y₂ : x ≡Nat y) → x≡y₁ ≡ x≡y₂
+≡Nat-prop zero zero = refl
+≡Nat-prop (suc x≡y₁) (suc x≡y₂) = cong suc (≡Nat-prop x≡y₁ x≡y₂)
+
+≡Nat⇒≡ : ∀ {x y} → x ≡Nat y → x ≡ y
+≡Nat⇒≡ zero = refl
+≡Nat⇒≡ (suc x≡y) = cong suc (≡Nat⇒≡ x≡y)
+
+≡⇒≡Nat : ∀ {x y} → x ≡ y → x ≡Nat y
+≡⇒≡Nat {zero} {zero} x≡y = zero
+≡⇒≡Nat {suc x} {suc y} refl = suc (≡⇒≡Nat refl)
+
+suc-inj : ∀ {x y : Nat} → suc x ≡ suc y → x ≡ y
+suc-inj {x} {y} refl = refl
+
+suc-inv : ∀ {x y : Nat} → (p : suc x ≡ suc y) → p ≡ cong suc (suc-inj p)
+suc-inv {x} {y} refl = refl
+
+Nat-loop-UIP : ∀ {x : Nat} (p : x ≡ x) → ≡⇒≡Nat p ≡ ≡Nat-refl → p ≡ refl
+Nat-loop-UIP {zero} refl q = refl
+Nat-loop-UIP {suc x} p q =
+  let IH = Nat-loop-UIP {x = x} (suc-inj p) (≡Nat-prop (≡⇒≡Nat (suc-inj p)) ≡Nat-refl) in
+  let z = cong (λ (p : x ≡ x) → cong Nat.suc p) IH in
+  trans (suc-inv p) z
+
+Nat-UIP : ∀ {x y : Nat} (x≡y₁ x≡y₂ : x ≡ y) → x≡y₁ ≡ x≡y₂
+Nat-UIP {zero} {zero} refl refl = refl
+Nat-UIP {suc x} {suc y} refl q = sym (Nat-loop-UIP q (≡Nat-prop (≡⇒≡Nat q) ≡Nat-refl))
+
+transport : {A : Set} (P : A → Set) {x y : A} (p : x ≡ y) (px : P x) → P y
+transport P refl px = px
+
+K : ∀ {x : Nat} {P : x ≡ x → Set} → P (refl {x = x}) → (h : x ≡ x) → P h
+K {x} {P} prefl x≡x = transport (λ x → P x) (Nat-UIP refl x≡x) prefl
diff --git a/src/AOP/Prefixes.agda b/src/AOP/Prefixes.agda
new file mode 100644
index 0000000..9aa32e6
--- /dev/null
+++ b/src/AOP/Prefixes.agda
@@ -0,0 +1,83 @@
+open import Data.Product
+open import Data.List
+open import Data.List.Properties
+open import Data.Nat
+open import Data.Empty
+open import Relation.Binary.PropositionalEquality hiding ([_])
+module Prefixes(Σ : Set) where 
+
+data Trace : Set where 
+   Finite : List Σ → Trace
+   Infinite : (ℕ → Σ) → Trace
+
+postulate ext : {A B : Set}{f g : A → B} → (∀ X → f X ≡ g X) → f ≡ g
+
+fininfin : List Σ → (ℕ → Σ) → ℕ → Σ
+fininfin [] f n = f n
+fininfin (x ∷ l) f zero = x
+fininfin (x ∷ l) f (suc n) = fininfin l f n
+
+_append_ : Trace → Trace → Trace
+Finite x append Finite x₁ = Finite (x ++ x₁)
+Finite x append Infinite x₁ = Infinite (fininfin x x₁)
+Infinite x append u = Infinite x 
+     
+_isPrefix_ : Trace → Trace → Set
+_isPrefix_ t u = ∃[ t′ ] u ≡ (t append t′)
+
+-- lemma: fininfin-assoc
+fininfin-assoc-n : ∀ {x y z} (n : ℕ) → fininfin (x ++ y) z n ≡ fininfin x (fininfin y z) n
+fininfin-assoc-n {[]} {y} {z} n = refl
+fininfin-assoc-n {x ∷ xs} {y} {z} zero = refl
+fininfin-assoc-n {x ∷ xs} {[]} {z} (suc n) = cong (λ p → fininfin p z n) (++-identityʳ xs)
+fininfin-assoc-n {x ∷ xs} {y ∷ ys} {z} (suc n) = fininfin-assoc-n {xs} {y ∷ ys} {z} n
+
+fininfin-assoc : ∀ {x y z} → fininfin (x ++ y) z ≡ fininfin x (fininfin y z)
+fininfin-assoc {x} {y} {z} = ext (fininfin-assoc-n {x} {y} {z})
+
+-- lemma: append-assoc
+append-assoc : ∀ {a b c} → (a append b) append c ≡ a append (b append c)
+append-assoc {Finite x} {Finite y} {Finite z} = cong Finite (++-assoc x y z)
+append-assoc {Finite x} {Finite y} {Infinite z} = cong Infinite (fininfin-assoc {x} {y} {z})
+append-assoc {Finite x} {Infinite y} {c} = refl
+append-assoc {Infinite x} {b} {c} = refl
+
+Finite-inj : {a b : List Σ} → Finite a ≡ Finite b → a ≡ b
+Finite-inj {[]} {[]} p = refl
+Finite-inj {x ∷ xs} {y ∷ ys} refl = refl
+
+-- lemma
+lemma1 : ∀ {a r} → Finite a append r ≡ Finite a → r ≡ Finite []
+lemma1 {[]} {Finite x} p = p
+lemma1 {x ∷ xs} {Finite r} p = cong Finite (++-identityʳ-unique (x ∷ xs) (Finite-inj (sym p)))
+
+lemma2 : ∀ {a b} → a append b ≡ Finite [] → a ≡ Finite [] × b ≡ Finite []
+lemma2 {Finite a} {Finite b} p = (cong Finite (++-conicalˡ a b (Finite-inj p))) , cong Finite (++-conicalʳ a b (Finite-inj p))
+
+-- doesn't matter what this is
+dummy : Trace
+dummy = Finite []
+
+prefl : ∀{t} → t isPrefix t
+prefl {Finite x} = Finite [] , cong Finite (sym (++-identityʳ x))
+prefl {Infinite x} = dummy , refl
+
+ptrans : ∀{t u v} → t isPrefix u → u isPrefix v → t isPrefix v
+ptrans {Finite t} {u} {v} (u-t , snd) (v-u , snd₁) =
+  let z1 = trans snd₁ (trans (cong (λ p → p append v-u) snd) append-assoc) in
+  (u-t append v-u) , z1
+ptrans {Infinite t} {u} {v} (fst , snd) (fst₁ , snd₁) =
+  let p = subst (λ x → v ≡ (x append fst₁)) snd snd₁ in
+  dummy , p
+
+pantisym : ∀{t u} → t isPrefix u → u isPrefix t → t ≡ u
+pantisym {Finite t} {Finite u} (u-t , p1) (t-u , p2) =
+  let z = subst (λ x → Finite u ≡ (x append u-t)) p2 p1 in 
+  let z1 = trans z append-assoc in
+  let z2 = lemma1 (sym z1) in
+  let z3 = lemma2 z2 in
+  let z4 = subst (λ z → Finite t ≡ Finite u append z) (z3 .proj₁) p2 in
+  let z5 = trans z4 (cong Finite (++-identityʳ u)) in
+  z5
+pantisym {t} {Infinite u} (u-t , p1) (t-u , p2) = p2
+ 
\ No newline at end of file
diff --git a/src/AOP/Thin.agda b/src/AOP/Thin.agda
new file mode 100644
index 0000000..85af85d
--- /dev/null
+++ b/src/AOP/Thin.agda
@@ -0,0 +1,141 @@
+open import Level using (Level)
+open import Data.List.Base using (List; []; _∷_; _++_)
+open import Data.Nat.Base using ()
+
+variable
+  a : Level
+  A : Set a
+  x y z : A
+  xs ys zs as bs cs : List A
+
+-- A thinning, also known as an order preserving embedding
+-- is a first order data structure explaining how a small
+-- list embeds into a bigger one.
+
+data Thin {A : Set a} : (xs ys : List A) → Set a where
+  -- The empty list trivially embeds into itself
+  done : Thin [] []
+  -- The remaining constructors are named based on what
+  -- we do with the head of the bigger list.
+  keep : (x : A) → Thin xs ys → Thin (x ∷ xs) (x ∷ ys)
+  drop : (y : A) → Thin xs ys → Thin xs       (y ∷ ys)
+
+-- We can for instance prove that we can embed the list
+-- [1,4] into the list [1,3,4] in an order preserving
+-- manner by giving the following thinning.
+
+thin₁ : Thin (1     ∷ 4 ∷ [])
+             (1 ∷ 3 ∷ 4 ∷ [])
+thin₁ = keep 1 (drop 3 (keep 4 done))
+
+-- And we can further embed [1,3,4] into [0,1,2,3,4]
+-- using the following thinning
+
+thin₂ : Thin (    1     ∷ 3 ∷ 4 ∷ [])
+             (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ [])
+thin₂ = drop 0 (keep 1 (drop 2 (keep 3 (keep 4 done))))
+
+
+------------------------------------------------------------------------
+-- Vertical composition
+
+-- By composing two thinnings that meet in the middle
+-- we ought to be able to obtain a third thinning spanning
+-- the gap between the smallest list and the largest one
+
+_seq_ : Thin xs ys →
+        Thin    ys zs →
+        Thin xs    zs
+
+-- e.g. reusing our prior example, we can prove that
+-- [1,4] embeds into [0,1,2,3,4] by "vertically"
+-- composing thin₁ and thin₂ like so:
+
+thin₃ : Thin (    1         ∷ 4 ∷ [])
+--           (    1     ∷ 3 ∷ 4 ∷ [])
+             (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ [])
+thin₃ = thin₁ seq thin₂
+
+-- Implement _seq_
+
+done seq x = x
+keep .x ph2 seq keep x th2 = keep x (ph2 seq th2)
+drop .x ph2 seq keep x th2 = drop x (ph2 seq th2)
+keep x ph2 seq drop y th2 = drop y (keep x ph2 seq th2)
+drop y ph2 seq drop z th2 = drop z ((drop y ph2) seq th2)
+
+------------------------------------------------------------------------
+-- Horizontal composition
+
+-- Similarly if we have two separate thinnings respectively
+-- between xs and ys on one hand, and as and bs on the other
+-- then we can paste them together "horizontally" and obtain
+-- a thinning between (xs ++ as) and (ys ++ bs)
+
+_par_ : Thin xs          ys →
+        Thin        as         bs →
+        Thin (xs ++ as) (ys ++ bs)
+
+
+-- e.g. reusing our prior example, we can prove that
+-- [1,4,1,3,4] embeds into [1,3,4,0,1,2,3,4] by "horizontally"
+-- composing thin₁ with thin₂*
+
+thin₄ : Thin (1     ∷ 4              ∷ 1     ∷ 3 ∷ 4 ∷ [])
+             (1 ∷ 3 ∷ 4          ∷ 0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ [])
+thin₄ =         thin₁      par            thin₂
+
+
+-- Implement _par_
+
+open import Relation.Binary.PropositionalEquality using (sym; subst)
+open import Data.List.Properties
+
+++-identity-Thin : ∀ {x y : List A} → Thin x y → Thin (x ++ []) (y ++ [])
+++-identity-Thin {x = x} {y = y} ph =
+  let ph1 = subst (λ xs → Thin xs y) (sym (++-identityʳ x)) ph in
+  subst (λ ys → Thin (x ++ []) ys) (sym (++-identityʳ y)) ph1
+
+done par th = th
+_par_ {xs = x ∷ xs₁} {ys = y ∷ ys₁} (keep x ph) done = keep x (++-identity-Thin ph)
+keep x ph par keep x₁ th = keep x (ph par keep x₁ th)
+keep x ph par drop y th = keep x (ph par (drop y th))
+_par_ {xs = xs} {ys = y ∷ ys₁} (drop y ph) done = drop y (++-identity-Thin ph)
+drop y ph par keep x th = drop y (ph par (keep x th))
+drop y ph par drop y₁ th = drop y (ph par drop y₁ th)
+
+------------------------------------------------------------------------
+-- Distributivity law
+
+-- Using our geometric intuition, a 2*2 tiling could be seen
+-- as rows of columns or columns of rows. Prove that we indeed
+-- get the same result no matter what:
+
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; trans)
+import Relation.Binary.PropositionalEquality as Eq
+open Eq.≡-Reasoning
+
+-- Implement cast
+
+infixl 5 _∙_
+_∙_ = trans
+
+lemma1 : ∀ (a : Thin xs ys) → a par done ≡ ++-identity-Thin a
+lemma1 done = refl
+lemma1 {xs = x ∷ xs₁} {ys = x ∷ ys₁} (keep x a) =
+  let IH = cong (keep x) (sym (lemma1 a)) in
+  IH ∙ {! refl  !}
+lemma1 (drop y a) = {! refl  !}
+
+lemma2 : ∀ (a : Thin xs ys) (b : Thin ys zs) → (a par done) seq (b par done) ≡ ++-identity-Thin (a seq b)
+lemma2 done b = lemma1 b
+lemma2 (keep x a) b = {!   !}
+lemma2 (drop y a) b = {!   !}
+
+cast :
+  (phᵗ : Thin xs ys) (phᵇ : Thin ys zs)
+  (thᵗ : Thin as bs) (thᵇ : Thin bs cs) →
+  (phᵗ seq phᵇ) par (thᵗ seq thᵇ) ≡ (phᵗ par thᵗ) seq (phᵇ par thᵇ)
+cast a b done done = lemma1 (a seq b) ∙ {!   !} ∙ {!   !} 
+cast a b c (keep x d) = {!   !}
+cast a b c (drop y d) = {!   !} 
\ No newline at end of file
diff --git a/src/Misc/CRDT.agda b/src/Misc/CRDT.agda
new file mode 100644
index 0000000..aa2485a
--- /dev/null
+++ b/src/Misc/CRDT.agda
@@ -0,0 +1,223 @@
+{-# OPTIONS --cubical #-}
+
+module Misc.CRDT where
+
+open import Agda.Primitive
+open import Data.List using (List; _∷_; [])
+open import Data.Nat using (ℕ)
+open import Data.Product
+open import Data.Bool
+open import Data.Empty
+open import Function
+open import Function.Properties.Equivalence using () renaming (sym to symEquiv)
+open import Relation.Binary.Bundles
+open import Relation.Binary.Definitions
+open import Relation.Binary.Consequences
+open import Relation.Binary.Structures
+import Relation.Binary.PropositionalEquality as Eq
+open import Relation.Binary.PropositionalEquality hiding (isEquivalence)
+open Eq.≡-Reasoning
+open import Relation.Nullary.Decidable
+open import Relation.Nullary.Reflects
+
+private
+  variable
+    ℓ ℓ' : Level
+
+module _ {ℓ ℓ' ℓ''} (TimeOrder : StrictTotalOrder ℓ ℓ' ℓ'') where
+  Time = TimeOrder .StrictTotalOrder.Carrier
+
+  record isCRDT {cℓ cℓ' : Level} (A : Set cℓ) : Set (lsuc (cℓ ⊔ cℓ' ⊔ ℓ ⊔ ℓ' ⊔ ℓ'')) where
+    field
+      op : Set cℓ'
+      noOp : op
+      apply2 : (o1 o2 : op) (t1 t2 : Time) → A → A
+      comm : (a : A) → (o1 o2 : op) (t1 t2 : Time) → apply2 o1 o2 t1 t2 a ≡ apply2 o2 o1 t2 t1 a
+
+  module _ where
+    open import Data.Nat
+    open isCRDT
+
+    Counter = ℕ
+
+    private
+      data Op : Set where
+        nop : Op
+        inc : Op
+
+      apply2' : Op → Op → Time → Time → Counter → Counter
+      apply2' nop nop t1 t2 c = c
+      apply2' nop inc t1 t2 c = suc c
+      apply2' inc nop t1 t2 c = suc c
+      apply2' inc inc t1 t2 c = suc (suc c)
+
+      comm' : (a : Counter) (o1 o2 : Op) (t1 t2 : Time) → apply2' o1 o2 t1 t2 a ≡ apply2' o2 o1 t2 t1 a
+      comm' c nop nop t1 t2 = refl
+      comm' c nop inc t1 t2 = refl
+      comm' c inc nop t1 t2 = refl
+      comm' c inc inc t1 t2 = refl
+    
+    CounterIsCRDT : isCRDT Counter
+    CounterIsCRDT .op = Op
+    CounterIsCRDT .noOp = nop
+    CounterIsCRDT .apply2 = apply2'
+    CounterIsCRDT .comm = comm'
+
+  module _ (K V : Set) (DecK : DecidableEquality K) where
+    open import Data.Unit
+    open import Data.Nat hiding (_⊔_)
+    open import Data.Product
+    open StrictTotalOrder (TimeOrder) renaming (compare to tcompare; _<_ to _t<_; _>_ to _t>_)
+    open isCRDT
+
+    Arb = (K × V) × (K × V)
+
+    postulate
+      JSMap : Set → Set → Set
+      rawGet : JSMap K V → K → V
+      JSMapExt : (m1 m2 : JSMap K V) → ((k : K) → rawGet m1 k ≡ rawGet m2 k) → m1 ≡ m2
+      rawInsert : (k : K) (v : V) (orig : JSMap K V) → Σ (JSMap K V) λ modif → rawGet modif k ≡ v
+
+      -- funExt : {A B : Set} (f g : A → B) → ((x : A) → f x ≡ g x) → f ≡ g
+      -- TODO: What is a clean way to get around this?
+      arb : (k1 k2 : K) (v1 v2 : V) → Arb
+      arb-comm : (k1 k2 : K) (v1 v2 : V) → arb k1 k2 v1 v2 ≡ arb k2 k1 v2 v1
+
+    private
+      data Op : Set where
+        nop : Op
+        insert : K → V → Op
+
+      apply : Op → JSMap K V → JSMap K V
+      apply nop m = m
+      apply (insert k v) m = rawInsert k v m .proj₁
+
+      TCompare : Time → Time → Set (ℓ' ⊔ ℓ'')
+      TCompare t1 t2 = Tri (t1 t< t2) (t1 ≈ t2) (flip _t<_ t1 t2)
+
+      doubleInsertSeq : (k1 k2 : K) (v1 v2 : V) → JSMap K V → JSMap K V
+      doubleInsertSeq k1 k2 v1 v2 m = rawInsert k2 v2 (rawInsert k1 v1 m .proj₁) .proj₁
+
+      k1Of : Arb → K
+      k1Of arb = arb .proj₁ .proj₁
+
+      k2Of : Arb → K
+      k2Of arb = arb .proj₂ .proj₁
+
+      doIt : (arb' : Arb) (d : Dec (k1Of arb' ≡ k2Of arb')) → JSMap K V → JSMap K V
+      -- just take the first one, since it doesn't matter
+      doIt arb' (true because _) m = rawInsert k1' v1' m .proj₁ where
+        k1' = arb' .proj₁ .proj₁
+        v1' = arb' .proj₁ .proj₂
+        k2' = arb' .proj₂ .proj₁
+        v2' = arb' .proj₂ .proj₂
+      -- insert both in order, since it doesn't matter
+      doIt arb' (false because _) m = doubleInsertSeq k1' k2' v1' v2' m where
+        k1' = arb' .proj₁ .proj₁
+        v1' = arb' .proj₁ .proj₂
+        k2' = arb' .proj₂ .proj₁
+        v2' = arb' .proj₂ .proj₂
+
+      doubleInsert : (k1 k2 : K) (v1 v2 : V) {t1 t2 : Time} (t1<t2 : TCompare t1 t2) → JSMap K V → JSMap K V
+      doubleInsert k1 k2 v1 v2 (tri< a ¬b ¬c) m = doubleInsertSeq k1 k2 v1 v2 m
+      doubleInsert k1 k2 v1 v2 {t1} {t2} (tri≈ ¬a b ¬c) m =
+        let arb' = arb k1 k2 v1 v2 in
+        doIt arb' (DecK (k1Of arb') (k2Of arb')) m
+      doubleInsert k1 k2 v1 v2 (tri> ¬a ¬b c) m = doubleInsertSeq k2 k1 v2 v1 m
+
+      apply2' : Op → Op → Time → Time → JSMap K V → JSMap K V
+      apply2' nop nop _ _ m = m
+      apply2' o1 nop _ _ m = apply o1 m
+      apply2' nop o2 _ _ m = apply o2 m
+      apply2' (insert k1 v1) (insert k2 v2) t1 t2 m = doubleInsert k1 k2 v1 v2 (tcompare t1 t2) m
+
+      comm' : (a : JSMap K V) (o1 o2 : Op) (t1 t2 : Time) → apply2' o1 o2 t1 t2 a ≡ apply2' o2 o1 t2 t1 a
+      comm' a nop nop t1 t2 = refl
+      comm' a (insert _ _) nop t1 t2 = refl
+      comm' a nop (insert _ _) t1 t2 = refl
+      comm' a (insert k1 v1) (insert k2 v2) t1 t2 = doubleInsertLemma (tcompare t1 t2) (tcompare t2 t1) where
+        a12 = doubleInsertSeq k1 k2 v1 v2 a
+        a21 = doubleInsertSeq k2 k1 v2 v1 a
+
+        x = _≈_
+        y = subst
+
+        doubleInsertLemma : (tc1 : TCompare t1 t2) (tc2 : TCompare t2 t1) → doubleInsert k1 k2 v1 v2 tc1 a ≡ doubleInsert k2 k1 v2 v1 tc2 a
+        doubleInsertLemma (tri< a ¬b ¬c) (tri< a₁ ¬b₁ ¬c₁) = ⊥-elim (asym a a₁)
+        doubleInsertLemma (tri< a ¬b ¬c) (tri≈ ¬a b ¬c₁) = ⊥-elim (irrefl (IsEquivalence.sym isEquivalence b) a)
+        doubleInsertLemma (tri< a ¬b ¬c) (tri> ¬a ¬b₁ c) = refl
+        doubleInsertLemma (tri≈ ¬a b ¬c) (tri< a ¬b ¬c₁) = ⊥-elim (irrefl (IsEquivalence.sym isEquivalence b) a)
+        doubleInsertLemma tc1 @ (tri≈ ¬a b ¬c) tc2 @ (tri≈ ¬a₁ b₁ ¬c₁) = doItLemma where
+          arb₁ = arb k1 k2 v1 v2
+          arb₂ = arb k2 k1 v2 v1
+          doItLemma : doIt arb₁ (DecK (k1Of arb₁) (k2Of arb₁)) a ≡ doIt arb₂ (DecK (k1Of arb₂) (k2Of arb₂)) a
+          doItLemma = cong (λ arb' → doIt arb' (DecK (k1Of arb') (k2Of arb')) a) (arb-comm k1 k2 v1 v2)
+          -- doItLemma (no ¬a) (yes a) = ⊥-elim (¬a (sym a))
+          -- doItLemma (yes a) (no ¬a) = ⊥-elim (¬a (sym a))
+          -- doItLemma (yes t) (yes t₁) = cong₂ (λ arb' q → doIt arb' q a) (arb-comm k1 k2 v1 v2) {!   !} where
+          -- doItLemma (no ¬a) (no ¬a₁) = {!   !}
+          -- -- doItLemma : Dec (k1 ≡ k2) → doubleInsert k1 k2 v1 v2 tc1 a ≡ doubleInsert k2 k1 v2 v1 tc2 a
+          -- -- doItLemma (true because proof₁) = cong (λ arb' → {!   !}) arb-same
+          -- -- doItLemma (false because proof₁) = {! refl  !}
+        doubleInsertLemma (tri≈ ¬a b ¬c) (tri> ¬a₁ ¬b c) = ⊥-elim (irrefl b c)
+        doubleInsertLemma (tri> ¬a ¬b c) (tri< a ¬b₁ ¬c) = refl
+        doubleInsertLemma (tri> ¬a ¬b c) (tri≈ ¬a₁ b ¬c) = ⊥-elim (irrefl b c)
+        doubleInsertLemma (tri> ¬a ¬b c) (tri> ¬a₁ ¬b₁ c₁) = ⊥-elim (asym c c₁)
+
+    LWWMapIsCRDT : isCRDT (JSMap K V)
+    LWWMapIsCRDT .op = Op
+    LWWMapIsCRDT .noOp = nop
+    LWWMapIsCRDT .apply2 = apply2'
+    LWWMapIsCRDT .comm = comm'
+
+
+------------------------------------------------------------------------
+-- Old
+
+--   Counter = ℕ
+
+--   private
+--     data Op : Set where inc : Op
+
+--   CounterIsCRDT : isCRDT Counter
+--   CounterIsCRDT .op = Op
+--   CounterIsCRDT .apply inc t y = {!   !}
+--   CounterIsCRDT .comm a inc inc = {!   !}
+
+-- -- Last-write wins
+-- module _ (K V : Set) where
+--   open import Data.Unit
+--   open import Data.Nat
+--   open import Data.Product
+--   open isCRDT
+
+--   postulate
+--     JSMap : Set → Set → Set
+--     rawNew : ⊤ → JSMap K V
+--     rawGet : JSMap K V → K → V
+--     funExt : {A B : Set} (f g : A → B) → ((x : A) → f x ≡ g x) → f ≡ g
+--     JSMapExt : (m1 m2 : JSMap K V) → ((k : K) → rawGet m1 k ≡ rawGet m2 k) → m1 ≡ m2
+--     rawInsert : (k : K) (v : V) (orig : JSMap K V) → Σ (JSMap K V) λ modif → rawGet modif k ≡ v
+
+--   {-# COMPILE JS JSMap = Map  #-}
+--   {-# COMPILE JS rawNew = new Map()  #-}
+
+--   private
+--     data Op : Set where
+--       insert : K → V → Op
+
+--     apply' : Op → Time → JSMap K V → JSMap K V
+--     apply' (insert k v) _ map = rawInsert k v map .proj₁
+
+--     comm' : (a : JSMap K V) (o1 o2 : Op) (t1 t2 : Time) → apply' o1 t1 (apply' o2 t2 a) ≡ apply' o2 t2 (apply' o1 t1 a)
+--     comm' map (insert k1 v1) (insert k2 v2) t1 t2 =
+--       let res1 = rawInsert k1 v1 map in
+--       let res2 = rawInsert k2 v2 map in
+--       let res12 = rawInsert k2 v2 (res1 .proj₁) in
+--       let res21 = rawInsert k1 v1 (res2 .proj₁) in
+--       JSMapExt (res21 .proj₁) (res12 .proj₁) λ k → {!   !}
+
+--   LWWMapIsCRDT : isCRDT (JSMap K V)
+--   LWWMapIsCRDT .op = Op     
+--   LWWMapIsCRDT .apply = apply'
+--   LWWMapIsCRDT .comm = comm'
\ No newline at end of file
diff --git a/src/ThesisWork/EMSpace.agda b/src/ThesisWork/EMSpace.agda
index 787ee28..7ec0cc0 100644
--- a/src/ThesisWork/EMSpace.agda
+++ b/src/ThesisWork/EMSpace.agda
@@ -38,7 +38,7 @@ module _ where
   open import Cubical.Algebra.Group.Instances.Int
   
   test : S¹ ≃ K[ ℤGroup ,1]
-  test = isoToEquiv (iso f g {!   !} {!   !}) where
+  test = isoToEquiv (iso {!   !} {!   !} {!   !} {!   !}) where
     loop^_ : ℤ → S¹-base ≡ S¹-base
     -- loop^ pos (suc n) = (loop^ (pos n)) ∙ S¹-loop
     -- loop^ pos zero = refl
@@ -53,21 +53,18 @@ module _ where
     -- f S¹-base = base
     -- f (S¹-loop i) = loop (subst Code1 {!   !} {!   !}) i
 
-    f : S¹ → K[ ℤGroup ,1]
-    f S¹-base = base
-    f (S¹-loop i) = loop (subst Code1 {!   !} {!   !}) i
+    -- f : S¹ → K[ ℤGroup ,1]
+    -- f S¹-base = base
+    -- f (S¹-loop i) = loop (subst Code1 {!   !} {!   !}) i
 
-    g : K[ ℤGroup ,1] → S¹
-    g base = S¹-base
-    g (loop x i) = {!   !}
-    g (loop-1g i i₁) = {!   !}
-    g (loop-∙ x y i i₁) = {!   !}
-    g (squash x x₁ p q r s i i₁ i₂) = {!   !}
+    -- g : K[ ℤGroup ,1] → S¹
+    -- g base = S¹-base
+    -- g (loop x i) = {!   !}
+    -- g (loop-1g i i₁) = {!   !}
+    -- g (loop-∙ x y i i₁) = {!   !}
+    -- g (squash x y p q r s i j k) = {!   !}
 
 
-module _ (G : Group ℓ) where
-  open GroupStr (G .snd)
-
 
 -------------------------------------------------------------------------------
 -- Properties
@@ -104,37 +101,54 @@ module _ (G : Group ℓ) where
       gf : retract (λ y → y ⊙ x) (λ y → y ⊙ inv x)
       gf a = sym (·Assoc a x (inv x)) ∙ cong (a ⊙_) (·InvR x) ∙ ·IdR a
 
-    f1≡id : f 1g ≡ idEquiv ⟨ G ⟩
-    f1≡id i = fnEq i , isEquivEq i where
-      fnEq : f 1g .fst ≡ idEquiv ⟨ G ⟩ .fst
-      fnEq i x = ·IdR x i
+    feq : (g : ⟨ G ⟩) → ⟨ G ⟩ ≡ ⟨ G ⟩
+    feq g = ua (f g)
 
-      isEquivEq : PathP (λ i → isEquiv (fnEq i)) (f 1g .snd) (idEquiv ⟨ G ⟩ .snd)
-      isEquivEq = toPathP (isPropIsEquiv (idfun ⟨ G ⟩) (subst isEquiv fnEq (f 1g .snd)) (idEquiv ⟨ G ⟩ .snd))
+    f1≡id : f 1g ≡ idEquiv ⟨ G ⟩
+    f1≡id = equivEq (funExt (λ x → ·IdR x))
+
+    feq1≡refl : feq 1g ≡ refl
+    feq1≡refl = cong ua f1≡id ∙ uaIdEquiv
+
+    flemma2 : (x y : ⟨ G ⟩) → f (x · y) ≡ compEquiv (f x) (f y)
+    flemma2 x y = equivEq (funExt (λ z → ·Assoc z x y))
+
+  S = Square
+  transpose : {A : Type ℓ} {a00 a01 a10 a11 : A}
+    {a0- : a00 ≡ a01} {a1- : a10 ≡ a11} {a-0 : a00 ≡ a10} {a-1 : a01 ≡ a11}
+    → Square a0- a1- a-0 a-1 → Square a-0 a-1 a0- a1-
+  transpose s i j = s j i
 
   Codes : K[G,1] → hSet ℓ
-  Codes = GT.rec isGroupoidHSet Codes' where
-    CodesFunc : ⟨ G ⟩ → ⟨ G ⟩ ≃ ⟨ G ⟩
-    CodesFunc g = {!   !}
+  Codes base = ⟨ G ⟩ , is-set
+  Codes (loop x i) = (Codes-aux.feq x i) , z i where
+    z : PathP (λ i → isSet (Codes-aux.feq x i)) is-set is-set
+    z = toPathP (isPropIsSet (transport (λ i₁ → isSet (Codes-aux.feq x i₁)) is-set) is-set)
+  Codes (loop-1g i j) = {!   !}
+  Codes (loop-∙ x y i j) = {!   !} , {!   !}
+  Codes (squash x y p q r s i j k) = CodesGpd (Codes x) (Codes y) (cong Codes p) (cong Codes q) (cong (cong Codes) r) (cong (cong Codes) s) i j k where
+    CodesGpd = isOfHLevelTypeOfHLevel 2
 
-    Codes' : K[ G ,1] → hSet ℓ
-    Codes' base = ⟨ G ⟩ , is-set
-    Codes' (loop x i) = ⟨ G ⟩ , is-set
-    Codes' (loop-1g i i₁) = {!   !}
-    Codes' (loop-∙ x y i i₁) = {!   !}
-    Codes' x = ?
+  -- For point-free transports
+  Codes2 : K[G,1] → Type ℓ
+  Codes2 x = Codes x .fst
 
-  module _ where
-    _ : (x y : ⟨ G ⟩) → subst {! λ x → Codes x .snd  !} {!   !} {!   !} ≡ {!   !}
+  fact : (x y : ⟨ G ⟩) → subst Codes2 (loop x) y ≡ y ⊙ x
+  fact x y = let z = sym (subst-filler {!   !} {!   !} {!   !}) in {!   !}
 
-  encode : (z : K[G,1]) → ∣ base ∣₃ ≡ z → ⟨ Codes z ⟩
-  encode z p = {!   !}
+  encode : (z : K[G,1]) → base ≡ z → ⟨ Codes z ⟩
+  encode z p = subst Codes2 p 1g
 
   decode : ⟨ G ⟩ → base ≡ base
   decode x = loop x
 
-  encode-decode : (z : ⟨ G ⟩) → encode base (decode z) ≡ z
-  encode-decode z = {!   !}
+  encode-decode : (x : ⟨ G ⟩) → encode base (decode x) ≡ x
+  encode-decode x =
+    encode base (decode x) ≡⟨ refl ⟩
+    encode base (loop x) ≡⟨ refl ⟩
+    subst Codes2 (loop x) 1g ≡⟨ fact x 1g ⟩
+    1g ⊙ x ≡⟨ ·IdL x ⟩
+    x ∎
 
   ΩKG1≃G' : GroupIso {! ΩK[G,1]  !} G