diff --git a/src/Realizability/Assembly/Base.agda b/src/Realizability/Assembly/Base.agda
index 21be2d4..8ddc335 100644
--- a/src/Realizability/Assembly/Base.agda
+++ b/src/Realizability/Assembly/Base.agda
@@ -2,6 +2,10 @@
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Functions.FunExtEquiv
 open import Cubical.Data.Sigma
 open import Cubical.HITs.PropositionalTruncation
 open import Cubical.Reflection.RecordEquiv
@@ -11,32 +15,55 @@ module Realizability.Assembly.Base {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra
   record Assembly (X : Type ℓ) : Type (ℓ-suc ℓ) where
     infix 25 _⊩_
     field
-      isSetX : isSet X
       _⊩_ : A → X → Type ℓ
+      isSetX : isSet X
       ⊩isPropValued : ∀ a x → isProp (a ⊩ x)
       ⊩surjective : ∀ x → ∃[ a ∈ A ] a ⊩ x
 
+  open Assembly public
+  _⊩[_]_ : ∀ {X : Type ℓ} → A → Assembly X → X → Type ℓ
+  a ⊩[ A ] x = A ._⊩_ a x
 
   AssemblyΣ : Type ℓ → Type _
   AssemblyΣ X =
-    Σ[ isSetX ∈ isSet X ]
     Σ[ _⊩_ ∈ (A → X → hProp ℓ) ]
-    (∀ x → ∃[ a ∈ A ] ⟨ a ⊩ x ⟩)
-
-  AssemblyΣX→isSetX : ∀ X → AssemblyΣ X → isSet X
-  AssemblyΣX→isSetX X (isSetX , _ , _) = isSetX
-
-  AssemblyΣX→⊩ : ∀ X → AssemblyΣ X → (A → X → hProp ℓ)
-  AssemblyΣX→⊩ X (_ , ⊩ , _) = ⊩
-
-  AssemblyΣX→⊩surjective : ∀ X → (asm : AssemblyΣ X) → (∀ x → ∃[ a ∈ A ] ⟨ AssemblyΣX→⊩ X asm a x ⟩)
-  AssemblyΣX→⊩surjective X (_ , _ , ⊩surjective) = ⊩surjective
+    (∀ x → ∃[ a ∈ A ] ⟨ a ⊩ x ⟩) ×
+    (isSet X)
 
   isSetAssemblyΣ : ∀ X → isSet (AssemblyΣ X)
-  isSetAssemblyΣ X = isSetΣ (isProp→isSet isPropIsSet) λ isSetX → isSetΣ (isSetΠ (λ a → isSetΠ λ x → isSetHProp)) λ _⊩_ → isSetΠ λ x → isProp→isSet isPropPropTrunc
+  isSetAssemblyΣ X = isSetΣ (isSetΠ2 λ _ _ → isSetHProp) (λ rel → isSet× (isSetΠ λ x → isProp→isSet isPropPropTrunc) (isProp→isSet isPropIsSet))
   
-  unquoteDecl AssemblyIsoΣ = declareRecordIsoΣ AssemblyIsoΣ (quote Assembly)
+  AssemblyΣ≡Equiv : ∀ X → (a b : AssemblyΣ X) → (a ≡ b) ≃ (∀ r x → ⟨ a .fst r x ⟩ ≃ ⟨ b .fst r x ⟩)
+  AssemblyΣ≡Equiv X a b =
+    a ≡ b
+      ≃⟨ invEquiv (Σ≡PropEquiv (λ rel → isProp× (isPropΠ λ x → isPropPropTrunc) isPropIsSet) {u = a} {v = b}) ⟩
+    a .fst ≡ b .fst
+      ≃⟨ invEquiv (funExt₂Equiv {f = a .fst} {g = b .fst}) ⟩
+    (∀ (r : A) (x : X) → a .fst r x ≡ b .fst r x)
+      ≃⟨
+        equivΠCod
+          (λ r →
+            equivΠCod
+              λ x →
+                compEquiv
+                  (invEquiv (Σ≡PropEquiv (λ _ → isPropIsProp) {u = a .fst r x} {v = b .fst r x}))
+                  (univalence {A = a .fst r x .fst} {B = b .fst r x .fst}))
+       ⟩
+    (∀ (r : A) (x : X) → ⟨ a .fst r x ⟩ ≃ ⟨ b .fst r x ⟩)
+      ■
 
-  open Assembly public
+  -- definitional isomorphism
+  AssemblyΣIsoAssembly : ∀ X → Iso (AssemblyΣ X) (Assembly X)
+  _⊩_ (Iso.fun (AssemblyΣIsoAssembly X) (rel , surj , isSetX)) a x = ⟨ rel a x ⟩
+  Assembly.isSetX (Iso.fun (AssemblyΣIsoAssembly X) (rel , surj , isSetX)) = isSetX
+  ⊩isPropValued (Iso.fun (AssemblyΣIsoAssembly X) (rel , surj , isSetX)) a x = str (rel a x)
+  ⊩surjective (Iso.fun (AssemblyΣIsoAssembly X) (rel , surj , isSetX)) x = surj x
+  Iso.inv (AssemblyΣIsoAssembly X) asm = (λ a x → (a ⊩[ asm ] x) , (asm .⊩isPropValued a x)) , (λ x → asm .⊩surjective x) , asm .isSetX
+  Iso.rightInv (AssemblyΣIsoAssembly X) asm = refl
+  Iso.leftInv (AssemblyΣIsoAssembly X) (rel , surj , isSetX) = refl
 
-  
+  AssemblyΣ≃Assembly : ∀ X → AssemblyΣ X ≃ Assembly X
+  AssemblyΣ≃Assembly X = isoToEquiv (AssemblyΣIsoAssembly X)
+
+  isSetAssembly : ∀ X → isSet (Assembly X)
+  isSetAssembly X = isOfHLevelRespectEquiv 2 (AssemblyΣ≃Assembly X) (isSetAssemblyΣ X)
diff --git a/src/Realizability/Assembly/BinCoproducts.agda b/src/Realizability/Assembly/BinCoproducts.agda
index 502cfa9..4648b7d 100644
--- a/src/Realizability/Assembly/BinCoproducts.agda
+++ b/src/Realizability/Assembly/BinCoproducts.agda
@@ -3,7 +3,7 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
 open import Cubical.Data.Sum hiding (map)
 open import Cubical.Data.Sigma
-open import Cubical.Data.Fin
+open import Cubical.Data.FinData
 open import Cubical.Data.Nat
 open import Cubical.Data.Vec hiding (map)
 open import Cubical.HITs.PropositionalTruncation hiding (map)
@@ -11,7 +11,7 @@ open import Cubical.HITs.PropositionalTruncation.Monad
 open import Cubical.Categories.Category
 open import Cubical.Categories.Limits.BinCoproduct
 open import Realizability.CombinatoryAlgebra
-open import Realizability.ApplicativeStructure renaming (λ*-chain to `λ*; λ*-naturality to `λ*ComputationRule) hiding (λ*)
+open import Realizability.ApplicativeStructure
 
 module Realizability.Assembly.BinCoproducts {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
 
@@ -20,9 +20,6 @@ open import Realizability.Assembly.Base ca
 open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a)
 open import Realizability.Assembly.Morphism ca
 
-λ* = `λ* as fefermanStructure
-λ*ComputationRule = `λ*ComputationRule as fefermanStructure
-
 infixl 23 _⊕_
 _⊕_ : {A B : Type ℓ} → Assembly A → Assembly B → Assembly (A ⊎ B)
 (as ⊕ bs) .isSetX = isSet⊎ (as .isSetX) (bs .isSetX)
@@ -61,12 +58,13 @@ _⊕_ : {A B : Type ℓ} → Assembly A → Assembly B → Assembly (A ⊎ B)
 [ f , g ] .map (inr y) = g .map y
 [_,_] {asmZ = asmZ} f g .tracker =
   do
+    -- these are not considered structurally smaller since these are in the propositional truncation
     (f~ , f~tracks) ← f .tracker
     (g~ , g~tracks) ← g .tracker
     -- if (pr₁ r) then f (pr₂ r) else g (pr₂ r)
     let
       tracker : Term as (suc zero)
-      tracker = ` Id ̇ (` pr₁ ̇ (# fzero)) ̇ (` f~ ̇ (` pr₂ ̇ (# fzero))) ̇ (` g~ ̇ (` pr₂ ̇ (# fzero)))
+      tracker = ` Id ̇ (` pr₁ ̇ (# zero)) ̇ (` f~ ̇ (` pr₂ ̇ (# zero))) ̇ (` g~ ̇ (` pr₂ ̇ (# zero)))
     return
       (λ* tracker ,
         λ { (inl x) r r⊩inl →
@@ -79,7 +77,7 @@ _⊕_ : {A B : Type ℓ} → Assembly A → Assembly B → Assembly (A ⊎ B)
                          (λ r → asmZ ._⊩_ r ([ f , g ] .map (inl x)))
                          (sym
                            (λ* tracker ⨾ r
-                             ≡⟨ λ*ComputationRule tracker (r ∷ []) ⟩
+                             ≡⟨ λ*ComputationRule tracker r ⟩
                             Id ⨾ (pr₁ ⨾ r) ⨾ (f~ ⨾ (pr₂ ⨾ r)) ⨾ (g~ ⨾ (pr₂ ⨾ r))
                              ≡⟨ cong (λ r → Id ⨾ (pr₁ ⨾ r) ⨾ (f~ ⨾ (pr₂ ⨾ r)) ⨾ (g~ ⨾ (pr₂ ⨾ r))) r≡pair⨾true⨾rₓ ⟩
                             Id ⨾ (pr₁ ⨾ (pair ⨾ true ⨾ rₓ)) ⨾ (f~ ⨾ (pr₂ ⨾ (pair ⨾ true ⨾ rₓ))) ⨾ (g~ ⨾ (pr₂ ⨾ (pair ⨾ true ⨾ rₓ)))
@@ -101,7 +99,7 @@ _⊕_ : {A B : Type ℓ} → Assembly A → Assembly B → Assembly (A ⊎ B)
                          (λ r → asmZ ._⊩_ r ([ f , g ] .map (inr y)))
                          (sym
                            ((λ* tracker ⨾ r
-                             ≡⟨ λ*ComputationRule tracker (r ∷ []) ⟩
+                             ≡⟨ λ*ComputationRule tracker r ⟩
                             Id ⨾ (pr₁ ⨾ r) ⨾ (f~ ⨾ (pr₂ ⨾ r)) ⨾ (g~ ⨾ (pr₂ ⨾ r))
                              ≡⟨ cong (λ r → Id ⨾ (pr₁ ⨾ r) ⨾ (f~ ⨾ (pr₂ ⨾ r)) ⨾ (g~ ⨾ (pr₂ ⨾ r))) r≡pair⨾false⨾yᵣ ⟩
                             Id ⨾ (pr₁ ⨾ (pair ⨾ false ⨾ yᵣ)) ⨾ (f~ ⨾ (pr₂ ⨾ (pair ⨾ false ⨾ yᵣ))) ⨾ (g~ ⨾ (pr₂ ⨾ (pair ⨾ false ⨾ yᵣ)))
@@ -126,6 +124,7 @@ BinCoproductsASM (X , asmX) (Y , asmY) .univProp {Z , asmZ} f g =
     (λ ! → isProp× (isSetAssemblyMorphism _ _ _ _) (isSetAssemblyMorphism _ _ _ _))
     λ ! (κ₁⊚!≡f , κ₂⊚!≡g) → AssemblyMorphism≡ _ _ (funExt λ { (inl x) i → κ₁⊚!≡f (~ i) .map x ; (inr y) i → κ₂⊚!≡g (~ i) .map y })
 
+-- I have no idea why I did these since this can be derived from the universal property of the coproduct anyway?
 module _
   {X Y : Type ℓ}
   (asmX : Assembly X)
@@ -142,7 +141,7 @@ module _
     do
       let
         tracker : Term as 1
-        tracker = ` Id ̇ (` pr₁ ̇ # fzero) ̇ (` pair ̇ ` false ̇ (` pr₂ ̇ # fzero)) ̇ (` pair ̇ ` true ̇ (` pr₂ ̇ # fzero))
+        tracker = ` Id ̇ (` pr₁ ̇ # zero) ̇ (` pair ̇ ` false ̇ (` pr₂ ̇ # zero)) ̇ (` pair ̇ ` true ̇ (` pr₂ ̇ # zero))
       return
         ((λ* tracker) ,
          (λ { (inl x) r r⊩inl →
@@ -154,7 +153,7 @@ module _
                          λ*trackerEq : λ* tracker ⨾ r ≡ pair ⨾ false ⨾ rₓ
                          λ*trackerEq =
                            λ* tracker ⨾ r
-                             ≡⟨ λ*ComputationRule tracker (r ∷ []) ⟩
+                             ≡⟨ λ*ComputationRule tracker r ⟩
                            Id ⨾ (pr₁ ⨾ r) ⨾ (pair ⨾ false ⨾ (pr₂ ⨾ r)) ⨾ (pair ⨾ true ⨾ (pr₂ ⨾ r))
                              ≡⟨ cong (λ r → Id ⨾ (pr₁ ⨾ r) ⨾ (pair ⨾ false ⨾ (pr₂ ⨾ r)) ⨾ (pair ⨾ true ⨾ (pr₂ ⨾ r))) r≡pair⨾true⨾rₓ ⟩
                            Id ⨾ (pr₁ ⨾ (pair ⨾ true ⨾ rₓ)) ⨾ (pair ⨾ false ⨾ (pr₂ ⨾ (pair ⨾ true ⨾ rₓ))) ⨾ (pair ⨾ true ⨾ (pr₂ ⨾ (pair ⨾ true ⨾ rₓ)))
@@ -175,7 +174,7 @@ module _
                          λ*trackerEq : λ* tracker ⨾ r ≡ pair ⨾ true ⨾ yᵣ
                          λ*trackerEq =
                            λ* tracker ⨾ r
-                             ≡⟨ λ*ComputationRule tracker (r ∷ []) ⟩
+                             ≡⟨ λ*ComputationRule tracker r ⟩
                            Id ⨾ (pr₁ ⨾ r) ⨾ (pair ⨾ false ⨾ (pr₂ ⨾ r)) ⨾ (pair ⨾ true ⨾ (pr₂ ⨾ r))
                              ≡⟨ cong (λ r → Id ⨾ (pr₁ ⨾ r) ⨾ (pair ⨾ false ⨾ (pr₂ ⨾ r)) ⨾ (pair ⨾ true ⨾ (pr₂ ⨾ r))) r≡pair⨾false⨾yᵣ ⟩
                            Id ⨾ (pr₁ ⨾ (pair ⨾ false ⨾ yᵣ)) ⨾ (pair ⨾ false ⨾ (pr₂ ⨾ (pair ⨾ false ⨾ yᵣ))) ⨾ (pair ⨾ true ⨾ (pr₂ ⨾ (pair ⨾ false ⨾ yᵣ)))
diff --git a/src/Realizability/Assembly/BinProducts.agda b/src/Realizability/Assembly/BinProducts.agda
index 36c7976..b076635 100644
--- a/src/Realizability/Assembly/BinProducts.agda
+++ b/src/Realizability/Assembly/BinProducts.agda
@@ -1,11 +1,13 @@
-{-# OPTIONS --cubical --allow-unsolved-metas #-}
+{-# OPTIONS --cubical #-}
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
 open import Cubical.Data.Sigma
+open import Cubical.Data.FinData
 open import Cubical.HITs.PropositionalTruncation hiding (map)
 open import Cubical.HITs.PropositionalTruncation.Monad
 open import Cubical.Categories.Limits.BinProduct
 open import Realizability.CombinatoryAlgebra
+open import Realizability.ApplicativeStructure
 
 module Realizability.Assembly.BinProducts {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
 
@@ -40,52 +42,19 @@ _⊗_ : {A B : Type ℓ} → Assembly A → Assembly B → Assembly (A × B)
         (g : AssemblyMorphism zs ws)
         → AssemblyMorphism (xs ⊗ zs) (ys ⊗ ws)
 ⟪ f , g ⟫ .map (x , z) = f .map x , g .map z
-⟪_,_⟫ {ys = ys} {ws = ws} f g .tracker = (do
-                      (f~ , f~tracks) ← f .tracker
-                      (g~ , g~tracks) ← g .tracker
-                      return (s ⨾ (s ⨾ (k ⨾ pair) ⨾ (s ⨾ (k ⨾ f~) ⨾ (s ⨾ (k ⨾ pr₁) ⨾ Id))) ⨾ (s ⨾ (k ⨾ g~) ⨾ (s ⨾ (k ⨾ pr₂) ⨾ Id))
-                             , λ xz r r⊩xz →
-                               ( subst (λ y → ys ._⊩_ y (f .map (xz .fst)))
-                                 (sym (subst _
-                                             (sym (t⨾r≡pair_fg f~ g~ r))
-                                             (pr₁pxy≡x (f~ ⨾ (pr₁ ⨾ r)) (g~ ⨾ (pr₂ ⨾ r)))))
-                                 (f~tracks (xz .fst) (pr₁ ⨾ r) (r⊩xz .fst)))
-                               , subst (λ y → ws ._⊩_ y (g .map (xz .snd)))
-                                 (sym (subst _
-                                             (sym (t⨾r≡pair_fg f~ g~ r))
-                                             (pr₂pxy≡y (f~ ⨾ (pr₁ ⨾ r)) (g~ ⨾ (pr₂ ⨾ r)))))
-                                 (g~tracks (xz .snd) (pr₂ ⨾ r) (r⊩xz .snd))))
-                               where
-                      module _ (f~ g~ r : A) where
-                        subf≡fprr : ∀ f pr → (s ⨾ (k ⨾ f) ⨾ (s ⨾ (k ⨾ pr) ⨾ Id) ⨾ r) ≡ (f ⨾ (pr ⨾ r))
-                        subf≡fprr f pr =
-                                    s ⨾ (k ⨾ f) ⨾ (s ⨾ (k ⨾ pr) ⨾ Id) ⨾ r
-                                      ≡⟨ sabc≡ac_bc _ _ _ ⟩
-                                    (k ⨾ f ⨾ r) ⨾ (s ⨾ (k ⨾ pr) ⨾ Id ⨾ r)
-                                      ≡⟨ cong (λ x → x ⨾ _) (kab≡a f r) ⟩
-                                    f ⨾ (s ⨾ (k ⨾ pr) ⨾ Id ⨾ r)
-                                      ≡⟨ cong (λ x → f ⨾ x) (sabc≡ac_bc _ _ _) ⟩
-                                    f ⨾ (k ⨾ pr ⨾ r ⨾ (Id ⨾ r))
-                                      ≡⟨ cong (λ x → f ⨾ (x ⨾ (Id ⨾ r))) (kab≡a _ _ ) ⟩
-                                    f ⨾ (pr ⨾ (Id ⨾ r))
-                                      ≡⟨ cong (λ x → f ⨾ (pr ⨾ x)) (Ida≡a r) ⟩
-                                    f ⨾ (pr ⨾ r)
-                                      ∎
-                        t⨾r≡pair_fg :
-                          s ⨾ (s ⨾ (k ⨾ pair) ⨾ (s ⨾ (k ⨾ f~) ⨾ (s ⨾ (k ⨾ pr₁) ⨾ Id))) ⨾ (s ⨾ (k ⨾ g~) ⨾ (s ⨾ (k ⨾ pr₂) ⨾ Id)) ⨾ r
-                          ≡ pair ⨾ (f~ ⨾ (pr₁ ⨾ r)) ⨾ (g~ ⨾ (pr₂ ⨾ r))
-                        t⨾r≡pair_fg =
-                          s ⨾ (s ⨾ (k ⨾ pair) ⨾ (s ⨾ (k ⨾ f~) ⨾ (s ⨾ (k ⨾ pr₁) ⨾ Id))) ⨾ (s ⨾ (k ⨾ g~) ⨾ (s ⨾ (k ⨾ pr₂) ⨾ Id)) ⨾ r
-                            ≡⟨ sabc≡ac_bc _ _ _ ⟩
-                          s ⨾ (k ⨾ pair) ⨾ (s ⨾ (k ⨾ f~) ⨾ (s ⨾ (k ⨾ pr₁) ⨾ Id)) ⨾ r ⨾ (s ⨾ (k ⨾ g~) ⨾ (s ⨾ (k ⨾ pr₂) ⨾ Id) ⨾ r)
-                            ≡⟨ cong (λ x → x ⨾ (s ⨾ (k ⨾ g~) ⨾ (s ⨾ (k ⨾ pr₂) ⨾ Id) ⨾ r)) (sabc≡ac_bc _ _ _) ⟩
-                          k ⨾ pair ⨾ r ⨾ (s ⨾ (k ⨾ f~) ⨾ (s ⨾ (k ⨾ pr₁) ⨾ Id) ⨾ r) ⨾ (s ⨾ (k ⨾ g~) ⨾ (s ⨾ (k ⨾ pr₂) ⨾ Id) ⨾ r)
-                            ≡⟨ cong (λ x → x ⨾ (s ⨾ (k ⨾ f~) ⨾ (s ⨾ (k ⨾ pr₁) ⨾ Id) ⨾ r) ⨾ (s ⨾ (k ⨾ g~) ⨾ (s ⨾ (k ⨾ pr₂) ⨾ Id) ⨾ r))
-                              (kab≡a pair r) ⟩
-                          pair ⨾ (s ⨾ (k ⨾ f~) ⨾ (s ⨾ (k ⨾ pr₁) ⨾ Id) ⨾ r) ⨾ (s ⨾ (k ⨾ g~) ⨾ (s ⨾ (k ⨾ pr₂) ⨾ Id) ⨾ r)
-                            ≡⟨ cong₂ (λ x y → pair ⨾ x ⨾ y) (subf≡fprr f~ pr₁) (subf≡fprr g~ pr₂) ⟩
-                          pair ⨾ (f~ ⨾ (pr₁ ⨾ r)) ⨾ (g~ ⨾ (pr₂ ⨾ r))
-                            ∎
+⟪_,_⟫ {ys = ys} {ws = ws} f g .tracker =
+  do
+    (f~ , f~⊩isTrackedF) ← f .tracker
+    (g~ , g~⊩isTrackedG) ← g .tracker
+    let
+      realizer : Term as 1
+      realizer = ` pair ̇ (` f~ ̇ (` pr₁ ̇ # zero)) ̇ (` g~ ̇ (` pr₂ ̇ # zero))
+    return
+      (λ* realizer ,
+      (λ { (x , z) r (pr₁r⊩x , pr₂r⊩z) →
+        subst (λ r' → r' ⊩[ ys ] (f .map x)) (sym (cong (λ x → pr₁ ⨾ x) (λ*ComputationRule realizer r) ∙ pr₁pxy≡x _ _)) (f~⊩isTrackedF x (pr₁ ⨾ r) pr₁r⊩x) ,
+        subst (λ r' → r' ⊩[ ws ] (g .map z)) (sym (cong (λ x → pr₂ ⨾ x) (λ*ComputationRule realizer r) ∙ pr₂pxy≡y _ _)) (g~⊩isTrackedG z (pr₂ ⨾ r) pr₂r⊩z) }))
+        
 π₁ : {A B : Type ℓ} {as : Assembly A} {bs : Assembly B} → AssemblyMorphism (as ⊗ bs) as
 π₁ .map (a , b) = a
 π₁ .tracker = ∣ pr₁ , (λ (a , b) p (goal , _) → goal) ∣₁
@@ -100,63 +69,19 @@ _⊗_ : {A B : Type ℓ} → Assembly A → Assembly B → Assembly (A × B)
       → AssemblyMorphism zs ys
       → AssemblyMorphism zs (xs ⊗ ys)
 ⟨ f , g ⟩ .map z = f .map z , g .map z
-⟨_,_⟩ {X} {Y} {Z} {xs} {ys} {zs} f g .tracker = map2 untruncated (f .tracker) (g .tracker) where
-  module _ 
-         ((f~ , f~tracks) : Σ[ f~ ∈ A ] tracks {xs = zs} {ys = xs}  f~ (f .map))
-         ((g~ , g~tracks) : Σ[ g~ ∈ A ] tracks {xs = zs} {ys = ys} g~ (g .map)) where
-           
-         _⊩X_ = xs ._⊩_
-         _⊩Y_ = ys ._⊩_
-         _⊩Z_ = zs ._⊩_
-             
-         t = s ⨾ (s ⨾ (k ⨾ pair) ⨾ (s ⨾ (k ⨾ f~) ⨾ Id)) ⨾ (s ⨾ (k ⨾ g~) ⨾ Id)
-         untruncated : Σ[ t ∈ A ] (∀ z zᵣ zᵣ⊩z → ((pr₁ ⨾ (t ⨾ zᵣ)) ⊩X (f .map z)) × ((pr₂ ⨾ (t ⨾ zᵣ)) ⊩Y (g .map z)))
-         untruncated = t , λ z zᵣ zᵣ⊩z → goal₁ z zᵣ zᵣ⊩z , goal₂ z zᵣ zᵣ⊩z where
-           module _ (z : Z) (zᵣ : A) (zᵣ⊩z : zᵣ ⊩Z z) where
-
-             pr₁⨾tracker⨾zᵣ≡f~⨾zᵣ : pr₁ ⨾ (t ⨾ zᵣ) ≡ f~ ⨾ zᵣ
-             pr₁⨾tracker⨾zᵣ≡f~⨾zᵣ =
-               pr₁ ⨾ (s ⨾ (s ⨾ (k ⨾ pair) ⨾ (s ⨾ (k ⨾ f~) ⨾ Id)) ⨾ (s ⨾ (k ⨾ g~) ⨾ Id) ⨾ zᵣ)
-                          ≡⟨ cong (λ x → pr₁ ⨾ x) (sabc≡ac_bc _ _ _) ⟩
-               pr₁ ⨾ (s ⨾ (k ⨾ pair) ⨾ (s ⨾ (k ⨾ f~) ⨾ Id) ⨾ zᵣ ⨾ (s ⨾ (k ⨾ g~) ⨾ Id ⨾ zᵣ))
-                          ≡⟨ cong (λ x → pr₁ ⨾ (x ⨾ (s ⨾ (k ⨾ g~) ⨾ Id ⨾ zᵣ))) (sabc≡ac_bc _ _ _) ⟩
-               pr₁ ⨾ (k ⨾ pair ⨾ zᵣ ⨾ (s ⨾ (k ⨾ f~) ⨾ Id ⨾ zᵣ) ⨾ (s ⨾ (k ⨾ g~) ⨾ Id ⨾ zᵣ))
-                          ≡⟨ cong (λ x → pr₁ ⨾ (x ⨾ (s ⨾ (k ⨾ f~) ⨾ Id ⨾ zᵣ) ⨾ (s ⨾ (k ⨾ g~) ⨾ Id ⨾ zᵣ))) (kab≡a _ _) ⟩
-               pr₁ ⨾ (pair ⨾ (s ⨾ (k ⨾ f~) ⨾ Id ⨾ zᵣ) ⨾ (s ⨾ (k ⨾ g~) ⨾ Id ⨾ zᵣ))
-                           ≡⟨ pr₁pxy≡x _ _ ⟩
-               s ⨾ (k ⨾ f~) ⨾ Id ⨾ zᵣ
-                            ≡⟨ sabc≡ac_bc _ _ _ ⟩
-               k ⨾ f~ ⨾ zᵣ ⨾ (Id ⨾ zᵣ)
-                           ≡⟨ cong (λ x → x ⨾ (Id ⨾ zᵣ)) (kab≡a _ _) ⟩
-               f~ ⨾ (Id ⨾ zᵣ)
-                          ≡⟨ cong (λ x → f~ ⨾ x) (Ida≡a _) ⟩
-               f~ ⨾ zᵣ
-                    ∎
-
-             pr₂⨾tracker⨾zᵣ≡g~⨾zᵣ : pr₂ ⨾ (t ⨾ zᵣ) ≡ g~ ⨾ zᵣ
-             pr₂⨾tracker⨾zᵣ≡g~⨾zᵣ =
-               pr₂ ⨾ (s ⨾ (s ⨾ (k ⨾ pair) ⨾ (s ⨾ (k ⨾ f~) ⨾ Id)) ⨾ (s ⨾ (k ⨾ g~) ⨾ Id) ⨾ zᵣ)
-                   ≡⟨ cong (λ x → pr₂ ⨾ x) (sabc≡ac_bc _ _ _) ⟩
-               pr₂ ⨾ (s ⨾ (k ⨾ pair) ⨾ (s ⨾ (k ⨾ f~) ⨾ Id) ⨾ zᵣ ⨾ (s ⨾ (k ⨾ g~) ⨾ Id ⨾ zᵣ))
-                   ≡⟨ cong (λ x → pr₂ ⨾ (x ⨾ (s ⨾ (k ⨾ g~) ⨾ Id ⨾ zᵣ))) (sabc≡ac_bc _ _ _) ⟩
-               pr₂ ⨾ (k ⨾ pair ⨾ zᵣ ⨾ (s ⨾ (k ⨾ f~) ⨾ Id ⨾ zᵣ) ⨾ (s ⨾ (k ⨾ g~) ⨾ Id ⨾ zᵣ))
-                   ≡⟨ cong (λ x → pr₂ ⨾ (x ⨾ (s ⨾ (k ⨾ f~) ⨾ Id ⨾ zᵣ) ⨾ (s ⨾ (k ⨾ g~) ⨾ Id ⨾ zᵣ))) (kab≡a _ _) ⟩
-               pr₂ ⨾ (pair ⨾ (s ⨾ (k ⨾ f~) ⨾ Id ⨾ zᵣ) ⨾ (s ⨾ (k ⨾ g~) ⨾ Id ⨾ zᵣ))
-                   ≡⟨ pr₂pxy≡y _ _ ⟩
-               s ⨾ (k ⨾ g~) ⨾ Id ⨾ zᵣ
-                   ≡⟨ sabc≡ac_bc _ _ _ ⟩
-               k ⨾ g~ ⨾ zᵣ ⨾ (Id ⨾ zᵣ)
-                   ≡⟨ cong (λ x → x ⨾ (Id ⨾ zᵣ)) (kab≡a _ _) ⟩
-               g~ ⨾ (Id ⨾ zᵣ)
-                  ≡⟨ cong (λ x → g~ ⨾ x) (Ida≡a _) ⟩
-               g~ ⨾ zᵣ
-                    ∎
-                  
-             goal₁ : (pr₁ ⨾ (t ⨾ zᵣ)) ⊩X (f .map z)
-             goal₁ = subst (λ y → y ⊩X (f .map z)) (sym pr₁⨾tracker⨾zᵣ≡f~⨾zᵣ) (f~tracks z zᵣ zᵣ⊩z)
+⟨_,_⟩ {X} {Y} {Z} {xs} {ys} {zs} f g .tracker =
+  do
+    (f~ , f~⊩isTrackedF) ← f .tracker
+    (g~ , g~⊩isTrackedG) ← g .tracker
+    let
+      realizer : Term as 1
+      realizer = ` pair ̇ (` f~ ̇ # zero) ̇ (` g~ ̇ # zero)
+    return
+      (λ* realizer ,
+      (λ z r r⊩z →
+        subst (λ r' → r' ⊩[ xs ] (f .map z)) (sym (cong (λ x → pr₁ ⨾ x) (λ*ComputationRule realizer r) ∙ pr₁pxy≡x _ _)) (f~⊩isTrackedF z r r⊩z) ,
+        subst (λ r' → r' ⊩[ ys ] (g .map z)) (sym (cong (λ x → pr₂ ⨾ x) (λ*ComputationRule realizer r) ∙ pr₂pxy≡y _ _)) (g~⊩isTrackedG z r r⊩z)))
   
-             goal₂ : (pr₂ ⨾ (t ⨾ zᵣ)) ⊩Y (g .map z)
-             goal₂ = subst (λ y → y ⊩Y (g .map z)) (sym pr₂⨾tracker⨾zᵣ≡g~⨾zᵣ) (g~tracks z zᵣ zᵣ⊩z)
 module _ {X Y : Type ℓ} (xs : Assembly X) (ys : Assembly Y) where
     theπ₁ = π₁ {A = X} {B = Y} {as = xs} {bs = ys}
     theπ₂ = π₂ {A = X} {B = Y} {as = xs} {bs = ys}
diff --git a/src/Realizability/Assembly/Coequalizers.agda b/src/Realizability/Assembly/Coequalizers.agda
index 1d7e0b8..c49ad62 100644
--- a/src/Realizability/Assembly/Coequalizers.agda
+++ b/src/Realizability/Assembly/Coequalizers.agda
@@ -5,11 +5,12 @@ open import Cubical.HITs.SetCoequalizer renaming (rec to setCoequalizerRec; elim
 open import Cubical.HITs.PropositionalTruncation hiding (map)
 open import Cubical.HITs.PropositionalTruncation.Monad
 open import Cubical.Data.Sigma
-open import Cubical.Categories.Limits.Coequalizers
 open import Realizability.CombinatoryAlgebra
+open import Realizability.ApplicativeStructure
 
 module Realizability.Assembly.Coequalizers {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
 
+open CombinatoryAlgebra ca
 open import Realizability.Assembly.Base ca
 open import Realizability.Assembly.Morphism ca
 open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a)
@@ -62,24 +63,28 @@ module _
                          → (f ⊚ ι' ≡ g ⊚ ι')
                          → ∃![ ! ∈ AssemblyMorphism coequalizer zs ] (ιcoequalizer ⊚ ! ≡ ι')
       coequalizerFactors (Z , zs) ι' f⊚ι'≡g⊚ι' =
+        uniqueExists
+          (let
+              map = (λ x → setCoequalizerRec (zs .isSetX) (ι' .map) (λ x i → f⊚ι'≡g⊚ι' i .map x) x)
+            in
+            makeAssemblyMorphism
+            map
+            (do
+              (ι'~ , ι'~⊩isTrackedι') ← ι' .tracker
+              return
+                (ι'~ ,
+                (λ x r r⊩x →  setCoequalizerElimProp {C = λ x → ∀ (r : A) → r ⊩[ coequalizer ] x → (ι'~ ⨾ r) ⊩[ zs ] (map x)} {!!} (λ y r r⊩y → {!!}) x r r⊩x))))
+          {!!}
+          {!!}
+          {!!}
+        {-
         uniqueExists (λ where
                         .map → setCoequalizerRec (zs .isSetX) (ι' .map) λ x → λ i → f⊚ι'≡g⊚ι' i .map x
-                        .tracker → {!!})
+                        .tracker → return ({!!} , (λ x r r⊩x → {!setCoequalizerElimProp {C = λ x → !})))
                         (AssemblyMorphism≡ _ _ (funExt λ x → refl))
                         (λ ! → isSetAssemblyMorphism ys zs (ιcoequalizer ⊚ !) ι')
                         λ ! ιcoequalizer⊚!≡ι' → AssemblyMorphism≡ _ _
                             (funExt λ x →
                               setCoequalizerElimProp
                               {C = λ x → setCoequalizerRec (zs .isSetX) (ι' .map) (λ x₁ i → f⊚ι'≡g⊚ι' i .map x₁) x ≡ ! .map x}
-                              (λ x → zs .isSetX _ _) (λ y → λ i → ιcoequalizer⊚!≡ι' (~ i) .map y) x)
-      open Coequalizer
-      open IsCoequalizer
-
-      ιIsCoequalizer : IsCoequalizer {C = ASM} f g ιcoequalizer
-      ιIsCoequalizer .glues = AssemblyMorphism≡ _ _ (funExt λ x → SetCoequalizer.coeq x)
-      ιIsCoequalizer .univProp q qGlues = coequalizerFactors _ q qGlues
-      
-      ASMCoequalizer : Coequalizer {C = ASM} f g
-      ASMCoequalizer .coapex = (SetCoequalizer (f .map) (g .map)) , coequalizer
-      Coequalizer.coeq ASMCoequalizer = ιcoequalizer
-      ASMCoequalizer .isCoequalizer = ιIsCoequalizer
+                              (λ x → zs .isSetX _ _) (λ y → λ i → ιcoequalizer⊚!≡ι' (~ i) .map y) x) -}
diff --git a/src/Realizability/Assembly/Equalizers.agda b/src/Realizability/Assembly/Equalizers.agda
index 3bee734..67e634e 100644
--- a/src/Realizability/Assembly/Equalizers.agda
+++ b/src/Realizability/Assembly/Equalizers.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --cubical --allow-unsolved-metas #-}
+{-# OPTIONS --cubical #-}
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
 open import Cubical.Data.Sigma
diff --git a/src/Realizability/Assembly/Everything.agda b/src/Realizability/Assembly/Everything.agda
index d91566f..549c4a2 100644
--- a/src/Realizability/Assembly/Everything.agda
+++ b/src/Realizability/Assembly/Everything.agda
@@ -7,4 +7,5 @@ open import Realizability.Assembly.Coequalizers
 open import Realizability.Assembly.Equalizers
 open import Realizability.Assembly.Exponentials
 open import Realizability.Assembly.Morphism
-open import Realizability.Assembly.Regular.Everything
+-- TODO : Fix regular structure modules
+-- open import Realizability.Assembly.Regular.Everything
diff --git a/src/Realizability/Assembly/Exponentials.agda b/src/Realizability/Assembly/Exponentials.agda
index 901ab18..114ed1a 100644
--- a/src/Realizability/Assembly/Exponentials.agda
+++ b/src/Realizability/Assembly/Exponentials.agda
@@ -1,9 +1,11 @@
 {-# OPTIONS --cubical --allow-unsolved-metas #-}
 open import Cubical.Foundations.Prelude
 open import Cubical.Data.Sigma
+open import Cubical.Data.FinData hiding (eq)
 open import Cubical.HITs.PropositionalTruncation hiding (map)
 open import Cubical.HITs.PropositionalTruncation.Monad
 open import Realizability.CombinatoryAlgebra
+open import Realizability.ApplicativeStructure
 
 module Realizability.Assembly.Exponentials {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
 
@@ -81,7 +83,20 @@ module _ {X Y Z : Type ℓ}
                                            .tracker → do
                                                        (f~ , f~tracker) ← f .tracker
                                                        -- λ* x. λ* y. f~ ⨾ (pair ⨾ x ⨾ y)
-                                                       return ({!!} , (λ z zᵣ zᵣ⊩z x xᵣ xᵣ⊩x → {!!})))
+                                                       let
+                                                         realizer : Term as 2
+                                                         realizer = ` f~ ̇ (` pair ̇ # one ̇ # zero)
+                                                       return
+                                                         (λ*2 realizer ,
+                                                         (λ z a a⊩z x b b⊩x →
+                                                           subst
+                                                             (λ r' → r' ⊩[ ys ] (f .map (z , x)))
+                                                             (sym (λ*2ComputationRule realizer a b))
+                                                             (f~tracker
+                                                               (z , x)
+                                                               (pair ⨾ a ⨾ b)
+                                                               ((subst (λ r' → r' ⊩[ zs ] z) (sym (pr₁pxy≡x _ _)) a⊩z) ,
+                                                                (subst (λ r' → r' ⊩[ xs ] x) (sym (pr₂pxy≡y _ _)) b⊩x))))))
                                         (AssemblyMorphism≡ _ _ (funExt (λ (z , x) → refl)))
                                         (λ g → isSetAssemblyMorphism _ _ (⟪ g , identityMorphism xs ⟫ ⊚ theEval) f)
                                         λ g g×id⊚eval≡f → AssemblyMorphism≡ _ _
diff --git a/src/Realizability/Assembly/Morphism.agda b/src/Realizability/Assembly/Morphism.agda
index bac0774..9cf92b7 100644
--- a/src/Realizability/Assembly/Morphism.agda
+++ b/src/Realizability/Assembly/Morphism.agda
@@ -3,11 +3,15 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Function
+open import Cubical.Foundations.Equiv
 open import Cubical.Data.Sigma
+open import Cubical.Data.FinData
 open import Cubical.HITs.PropositionalTruncation hiding (map)
+open import Cubical.HITs.PropositionalTruncation.Monad
 open import Cubical.Reflection.RecordEquiv
 open import Cubical.Categories.Category
 open import Realizability.CombinatoryAlgebra
+open import Realizability.ApplicativeStructure
 
 module Realizability.Assembly.Morphism {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
 
@@ -31,6 +35,8 @@ module _ {X Y : Type ℓ} {xs : Assembly X} {ys : Assembly Y} (t : A) (f : X →
                              ys .⊩isPropValued (t ⨾ aₓ) (f x)
     
 record AssemblyMorphism {X Y : Type ℓ} (as : Assembly X) (bs : Assembly Y) : Type ℓ where
+  no-eta-equality
+  constructor makeAssemblyMorphism
   open Assembly as renaming (_⊩_ to _⊩X_)
   open Assembly bs renaming (_⊩_ to _⊩Y_)
   field
@@ -55,6 +61,9 @@ module _ {X Y : Type ℓ} (xs : Assembly X) (ys : Assembly Y) where
   isSetAssemblyMorphism : isSet (AssemblyMorphism xs ys)
   isSetAssemblyMorphism = subst (λ t → isSet t) (sym AssemblyMorphism≡Σ) isSetAssemblyMorphismΣ
 
+AssemblyMorphism≡Equiv : ∀ {X Y : Type ℓ} {xs : Assembly X} {ys : Assembly Y} (f g : AssemblyMorphismΣ xs ys) → (f .fst ≡ g .fst) ≃ (f ≡ g)
+AssemblyMorphism≡Equiv {X} {Y} {xs} {ys} f g = Σ≡PropEquiv λ _ → isPropPropTrunc
+
 AssemblyMorphismΣ≡ : {X Y : Type ℓ}
                      {xs : Assembly X}
                      {ys : Assembly Y}
@@ -73,7 +82,11 @@ module _ {X Y : Type ℓ}
        thePath = AssemblyMorphismΣ≡ {X = X} {Y = Y} {xs = xs} {ys = ys}
        open Iso
        AssemblyMorphism≡ : (f .map ≡ g .map) → f ≡ g
-       AssemblyMorphism≡ fmap≡gmap i = theIso .inv (thePath (theIso .fun f) (theIso .fun g) (fmap≡gmap) i)
+       map (AssemblyMorphism≡ fmap≡gmap i) x = fmap≡gmap i x
+       tracker (AssemblyMorphism≡ fmap≡gmap i) =
+         isProp→PathP
+           (λ i → isPropPropTrunc {A = Σ[ t ∈ A ] (∀ x aₓ → aₓ ⊩[ xs ] x → (t ⨾ aₓ) ⊩[ ys ] (fmap≡gmap i x))})
+           (f .tracker) (g .tracker) i
 
 identityMorphism : {X : Type ℓ} (as : Assembly X) → AssemblyMorphism as as
 identityMorphism as .map x = x
@@ -84,34 +97,17 @@ compositeMorphism : {X Y Z : Type ℓ} {xs : Assembly X} {ys : Assembly Y} {zs :
                   → (g : AssemblyMorphism ys zs)
                   → AssemblyMorphism xs zs
 compositeMorphism f g .map x = g .map (f .map x)
-compositeMorphism {X} {Y} {Z} {xs} {ys} {zs} f g .tracker = map2 untruncated (f .tracker) (g .tracker) where
-                      open Assembly xs renaming (_⊩_ to _⊩X_)
-                      open Assembly ys renaming (_⊩_ to _⊩Y_)
-                      open Assembly zs renaming (_⊩_ to _⊩Z_)
-                      module _ (fTracker : Σ[ f~ ∈ A ] tracks {xs = xs} {ys = ys} f~ (f .map))
-                               (gTracker : Σ[ g~ ∈ A ] tracks {xs = ys} {ys = zs} g~ (g .map)) where
-                               
-                           f~ = fTracker .fst
-                           f~tracks = fTracker .snd
-
-                           g~ = gTracker .fst
-                           g~tracks = gTracker .snd
-
-                           easierVariant : ∀ x aₓ aₓ⊩x → (g~ ⨾ (f~ ⨾ aₓ)) ⊩Z g .map (f .map x)
-                           easierVariant x aₓ aₓ⊩x = g~tracks (f .map x) (f~ ⨾ aₓ) (f~tracks x aₓ aₓ⊩x)
-                             
-                           goal : ∀ (x : X) (aₓ : A) (aₓ⊩x : aₓ ⊩X x)
-                                  → (B g~ f~ ⨾ aₓ) ⊩Z (compositeMorphism f g .map x)
-                           goal x aₓ aₓ⊩x = subst (λ y → y ⊩Z g .map (f .map x))
-                                                  (sym (Ba≡gfa g~ f~ aₓ))
-                                                  (easierVariant x aₓ aₓ⊩x)
-
-                           untruncated : Σ[ t ∈ A ]
-                                         ((x : X) (aₓ : A)
-                                         → aₓ ⊩X x
-                                         → (t ⨾ aₓ) ⊩Z (compositeMorphism f g) .map x)
-                           untruncated = B g~ f~ , goal
-                             
+compositeMorphism {X} {Y} {Z} {xs} {ys} {zs} f g .tracker =
+  do
+    (f~ , isTrackedF) ← f .tracker
+    (g~ , isTrackedG) ← g .tracker
+    let
+      realizer : Term as 1
+      realizer = ` g~ ̇ (` f~ ̇ # zero)
+    return
+      (λ* realizer ,
+      (λ x aₓ aₓ⊩x → subst (λ r' → r' ⊩[ zs ] (g .map (f .map x))) (sym (λ*ComputationRule realizer aₓ)) (isTrackedG (f .map x) (f~ ⨾ aₓ) (isTrackedF x aₓ aₓ⊩x))))
+
 infixl 23 _⊚_
 _⊚_ : {X Y Z : Type ℓ} → {xs : Assembly X} {ys : Assembly Y} {zs : Assembly Z}
                        → AssemblyMorphism xs ys
diff --git a/src/Realizability/PERs/PER.agda b/src/Realizability/PERs/PER.agda
index a686f24..38bcb96 100644
--- a/src/Realizability/PERs/PER.agda
+++ b/src/Realizability/PERs/PER.agda
@@ -6,15 +6,28 @@ open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Structure using (⟨_⟩; str)
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Powerset
 open import Cubical.Functions.FunExtEquiv
 open import Cubical.Relation.Binary
 open import Cubical.Data.Sigma
+open import Cubical.Data.FinData
+open import Cubical.Reflection.RecordEquiv
+open import Cubical.HITs.PropositionalTruncation as PT hiding (map)
+open import Cubical.HITs.PropositionalTruncation.Monad
+open import Cubical.HITs.SetQuotients as SQ
+open import Cubical.Categories.Category
 
 module Realizability.PERs.PER
   {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
 
+open CombinatoryAlgebra ca
+open Combinators ca renaming (i to Id; ia≡a to Ida≡a)
+
+module BR = BinaryRelation
+
 isPartialEquivalenceRelation : PropRel A A ℓ → Type _
-isPartialEquivalenceRelation (rel , isPropValuedRel) = BinaryRelation.isSym rel × BinaryRelation.isTrans rel
+isPartialEquivalenceRelation (rel , isPropValuedRel) = BR.isSym rel × BR.isTrans rel
 
 isPropIsPartialEquivalenceRelation : ∀ r → isProp (isPartialEquivalenceRelation r)
 isPropIsPartialEquivalenceRelation (rel , isPropValuedRel) =
@@ -26,57 +39,122 @@ record PER : Type (ℓ-suc ℓ) where
   no-eta-equality
   constructor makePER
   field
-    relation : A → A → Type ℓ
-    isPropValuedRelation : ∀ x y → isProp (relation x y)
-    isPER : isPartialEquivalenceRelation (relation , isPropValuedRelation)
+    relation : PropRel A A ℓ
+    isPER : isPartialEquivalenceRelation relation
+  ∣_∣ = relation .fst
   isSymmetric = isPER .fst
   isTransitive = isPER .snd
+  isPropValued = relation .snd
 
 open PER
 
-PERΣ : Type (ℓ-suc ℓ)
-PERΣ = Σ[ relation ∈ (A → A → hProp ℓ) ] isPartialEquivalenceRelation ((λ a b → ⟨ relation a b ⟩) , λ a b → str (relation a b))
-
-IsoPERΣPER : Iso PERΣ PER
-PER.relation (Iso.fun IsoPERΣPER (relation , isPER)) x y = ⟨ relation x y ⟩
-PER.isPropValuedRelation (Iso.fun IsoPERΣPER (relation , isPER)) x y = str (relation x y)
-PER.isPER (Iso.fun IsoPERΣPER (relation , isPER)) = isPER
-Iso.inv IsoPERΣPER per = (λ x y → per .relation x y , per .isPropValuedRelation x y) , (isSymmetric per) , (isTransitive per)
--- refl does not work because of no-eta-equality maybe?
-relation (Iso.rightInv IsoPERΣPER per i) = λ a b → per .relation a b
-isPropValuedRelation (Iso.rightInv IsoPERΣPER per i) = λ a b → per .isPropValuedRelation a b
-isPER (Iso.rightInv IsoPERΣPER per i) = (isSymmetric per) , (isTransitive per)
-Iso.leftInv IsoPERΣPER perΣ =
-  Σ≡Prop
-    (λ x → isPropIsPartialEquivalenceRelation ((λ a b → ⟨ x a b ⟩) , (λ a b → str (x a b))))
-    (funExt₂ λ a b → Σ≡Prop (λ x → isPropIsProp) refl)
-
-PERΣ≃PER : PERΣ ≃ PER
-PERΣ≃PER = isoToEquiv IsoPERΣPER
-
-isSetPERΣ : isSet PERΣ
-isSetPERΣ = isSetΣ (isSet→ (isSet→ isSetHProp)) (λ rel → isProp→isSet (isPropIsPartialEquivalenceRelation ((λ a b → ⟨ rel a b ⟩) , (λ a b → str (rel a b)))))
-
-isSetPER : isSet PER
-isSetPER = isOfHLevelRespectEquiv 2 PERΣ≃PER isSetPERΣ
-
-module ResizedPER (resizing : hPropResizing ℓ) where
-  private
-    smallHProp = resizing .fst
-    hProp≃smallHProp = resizing .snd
-    smallHProp≃hProp = invEquiv hProp≃smallHProp
-
-  ResizedPER : Type ℓ
-  ResizedPER = Σ[ relation ∈ (A → A → smallHProp) ] isPartialEquivalenceRelation ((λ a b → ⟨ equivFun (smallHProp≃hProp) (relation a b) ⟩) , λ a b → str (equivFun (smallHProp≃hProp) (relation a b)))
-
-  PERΣ≃ResizedPER : PERΣ ≃ ResizedPER
-  PERΣ≃ResizedPER =
-    Σ-cong-equiv-prop
-      (equiv→ (idEquiv A) (equiv→ (idEquiv A) hProp≃smallHProp))
-      (λ relation → isPropIsPartialEquivalenceRelation ((λ a b → ⟨ relation a b ⟩) , (λ a b → str (relation a b))))
-      (λ resizedRelation → isPropIsPartialEquivalenceRelation ((λ a b → ⟨ equivFun (smallHProp≃hProp) (resizedRelation a b) ⟩) , λ a b → str (equivFun smallHProp≃hProp (resizedRelation a b))))
-      (λ relation isPERRelation → (λ a b aRb → {!!}) , λ a b c aRb bRc → {!!})
-      λ relation isPERRelation → {!!}
-
-  PER≃ResizedPER : PER ≃ ResizedPER
-  PER≃ResizedPER = compEquiv (invEquiv PERΣ≃PER) PERΣ≃ResizedPER
+module _ (R : PER) where
+  Quotient = A / ∣ R ∣
+
+  -- mimics the proof at Cubical.HITs.SetQuotients.Properties
+  effectiveOnDomain : ∀ a b → ∣ R ∣ a a → [ a ] ≡ [ b ] → ∣ R ∣ a b
+  effectiveOnDomain a b aRa [a]≡[b] = transport aRa≡aRb aRa where
+    helper : Quotient → hProp _
+    helper x =
+      SQ.rec
+        isSetHProp
+        (λ c → (∣ R ∣ a c) , (isPropValued R a c))
+        (λ c d cRd →
+          Σ≡Prop
+            (λ _ → isPropIsProp)
+            (hPropExt
+              (isPropValued R a c)
+              (isPropValued R a d)
+              (λ aRc → isTransitive R a c d aRc cRd)
+              (λ aRd → isTransitive R a d c aRd (isSymmetric R c d cRd))))
+        x
+
+    aRa≡aRb : ∣ R ∣ a a ≡ ∣ R ∣ a b
+    aRa≡aRb i = helper ([a]≡[b] i) .fst
+
+record PERMorphism (R S : PER) : Type ℓ where
+  no-eta-equality
+  constructor makePERMorphism
+  field
+    map : Quotient R → Quotient S
+    isTracked : ∃[ e ∈ A ] (∀ (a : A) → ∣ R ∣ a a → (map [ a ] ≡ [ e ⨾ a ]) × ∣ S ∣ (e ⨾ a) (e ⨾ a))
+
+open PERMorphism
+
+unquoteDecl PERMorphismIsoΣ = declareRecordIsoΣ PERMorphismIsoΣ (quote PERMorphism)
+
+PERMorphismΣ : PER → PER → Type ℓ
+PERMorphismΣ R S = Σ[ map ∈ (Quotient R → Quotient S) ] ∃[ e ∈ A ] (∀ (a : A) → ∣ R ∣ a a → (map [ a ] ≡ [ e ⨾ a ]) × ∣ S ∣ (e ⨾ a) (e ⨾ a))
+
+isSetPERMorphismΣ : ∀ {R S} → isSet (PERMorphismΣ R S)
+isSetPERMorphismΣ {R} {S} = isSetΣ (isSet→ squash/) (λ map → isProp→isSet isPropPropTrunc)
+
+isSetPERMorphism : ∀ {R S} → isSet (PERMorphism R S)
+isSetPERMorphism {R} {S} = subst (λ type → isSet type) (sym (isoToPath PERMorphismIsoΣ)) (isSetPERMorphismΣ {R = R} {S = S})
+
+PERMorphism≡Iso : ∀ {R S} → (f g : PERMorphism R S) → Iso (f ≡ g) (f .map ≡ g .map)
+Iso.fun (PERMorphism≡Iso {R} {S} f g) f≡g i = f≡g i .map
+map (Iso.inv (PERMorphism≡Iso {R} {S} f g) fMap≡gMap i) = fMap≡gMap i
+isTracked (Iso.inv (PERMorphism≡Iso {R} {S} f g) fMap≡gMap i) =
+  isProp→PathP
+    (λ i →
+      isPropPropTrunc
+      {A = Σ[ e ∈ A ] (∀ (a : A) → ∣ R ∣ a a → ((fMap≡gMap i) [ a ] ≡ [ e ⨾ a ]) × ∣ S ∣ (e ⨾ a) (e ⨾ a))})
+    (f .isTracked) (g .isTracked) i
+Iso.rightInv (PERMorphism≡Iso {R} {S} f g) fMap≡gMap = refl
+Iso.leftInv (PERMorphism≡Iso {R} {S} f g) f≡g = isSetPERMorphism f g (Iso.inv (PERMorphism≡Iso f g) (λ i → f≡g i .map)) f≡g
+
+PERMorphism≡ : ∀ {R S} → (f g : PERMorphism R S) → f .map ≡ g .map → f ≡ g
+PERMorphism≡ {R} {S} f g fMap≡gMap = Iso.inv (PERMorphism≡Iso f g) fMap≡gMap
+
+idPERMorphism : ∀ {R : PER} → PERMorphism R R
+map (idPERMorphism {R}) x = x
+isTracked (idPERMorphism {R}) =
+  return (Id , (λ a aRa → (subst (λ r → [ a ] ≡ [ r ]) (sym (Ida≡a a)) refl) , (subst (λ r → ∣ R ∣ r r) (sym (Ida≡a a)) aRa)))
+
+composePERMorphism : ∀ {R S T : PER} → PERMorphism R S → PERMorphism S T → PERMorphism R T
+map (composePERMorphism {R} {S} {T} f g) x = g .map (f .map x)
+isTracked (composePERMorphism {R} {S} {T} f g) =
+  do
+    (f~ , isTrackedF) ← f .isTracked
+    (g~ , isTrackedG) ← g .isTracked
+    let
+      realizer : Term as 1
+      realizer = ` g~ ̇ (` f~ ̇ # zero)
+    return
+      (λ* realizer ,
+      (λ a aRa →
+        (g .map (f .map [ a ])
+          ≡⟨ cong (g .map) (isTrackedF a aRa .fst) ⟩
+        g .map [ f~ ⨾ a ]
+          ≡⟨ isTrackedG (f~ ⨾ a) (isTrackedF a aRa .snd) .fst ⟩
+        [ g~ ⨾ (f~ ⨾ a) ]
+          ≡⟨ cong [_] (sym (λ*ComputationRule realizer a)) ⟩
+        [ λ* realizer ⨾ a ]
+          ∎) ,
+        (subst (λ r' → ∣ T ∣ r' r') (sym (λ*ComputationRule realizer a)) (isTrackedG (f~ ⨾ a) (isTrackedF a aRa .snd) .snd))))
+
+-- all definitional
+idLPERMorphism : ∀ {R S} → (f : PERMorphism R S) → composePERMorphism idPERMorphism f ≡ f
+idLPERMorphism {R} {S} f = PERMorphism≡ _ _ refl
+
+idRPERMorphism : ∀ {R S} → (f : PERMorphism R S) → composePERMorphism f idPERMorphism ≡ f
+idRPERMorphism {R} {S} f = PERMorphism≡ _ _ refl
+
+assocPERMorphism :
+  ∀ {R S T U}
+  → (f : PERMorphism R S)
+  → (g : PERMorphism S T)
+  → (h : PERMorphism T U)
+  → composePERMorphism (composePERMorphism f g) h ≡ composePERMorphism f (composePERMorphism g h)
+assocPERMorphism {R} {S} {T} {U} f g h = PERMorphism≡ _ _ refl
+
+PERCat : Category (ℓ-suc ℓ) ℓ
+Category.ob PERCat = PER
+Category.Hom[_,_] PERCat R S = PERMorphism R S
+Category.id PERCat {R} = idPERMorphism
+Category._⋆_ PERCat {R} {S} {T} f g = composePERMorphism f g
+Category.⋆IdL PERCat f = idLPERMorphism f
+Category.⋆IdR PERCat f = idRPERMorphism f
+Category.⋆Assoc PERCat f g h = assocPERMorphism f g h
+Category.isSetHom PERCat = isSetPERMorphism