diff --git a/src/Realizability/Modest/GenericUniformFamily.agda b/src/Realizability/Modest/GenericUniformFamily.agda
index 50388b7..27aa6e6 100644
--- a/src/Realizability/Modest/GenericUniformFamily.agda
+++ b/src/Realizability/Modest/GenericUniformFamily.agda
@@ -34,6 +34,7 @@ open import Realizability.Assembly.SetsReflectiveSubcategory ca
 open import Realizability.Modest.Base ca
 open import Realizability.Modest.UniformFamily ca
 open import Realizability.Modest.CanonicalPER ca
+open import Realizability.Modest.UnresizedGeneric ca
 open import Realizability.PERs.PER ca
 open import Realizability.PERs.ResizedPER ca resizing
 open import Realizability.PERs.SubQuotient ca
@@ -99,6 +100,7 @@ uniformFamilyCleavage {X , asmX} {Y , asmY} f N =
     cartfᴰ : isCartesian f fᴰ
     cartfᴰ = isCartesian'→isCartesian f fᴰ cart'fᴰ
 
+
 ∇PER = ∇ ⟅ ResizedPER , isSetResizedPER ⟆
 asm∇PER = ∇PER .snd
 
@@ -108,57 +110,36 @@ UniformFamily.carriers (GenericObject.displayed genericUniformFamily) per = subQ
 UniformFamily.assemblies (GenericObject.displayed genericUniformFamily) per = subQuotientAssembly (enlargePER per)
 UniformFamily.isModestFamily (GenericObject.displayed genericUniformFamily) per = isModestSubQuotientAssembly (enlargePER per)
 GenericObject.isGeneric genericUniformFamily {X , asmX} M =
-  f , fᴰ , {!!} where
+  f , fᴰ , isCartesian'→isCartesian f fᴰ cart' where
 
     f : AssemblyMorphism asmX asm∇PER
     AssemblyMorphism.map f x = shrinkPER (canonicalPER (M .assemblies x) (M .isModestFamily x))
     AssemblyMorphism.tracker f = return (k , (λ _ _ _ → tt*))
 
-    subQuotientTargetType : (x : X) → M .carriers x → Type ℓ
-    subQuotientTargetType x Mx = subQuotient (canonicalPER (M .assemblies x) (M .isModestFamily x))
+    subQuotientCod≡ : ∀ per → subQuotient (enlargePER (shrinkPER per)) ≡ subQuotient per
+    subQuotientCod≡ per = cong subQuotient (enlargePER⋆shrinkPER≡id per)
 
     fᴰ : DisplayedUFamMap asmX asm∇PER f M (genericUniformFamily .GenericObject.displayed)
     DisplayedUFamMap.fibrewiseMap fᴰ x Mx =
-      subst (λ x → subQuotient x) (sym equation) target module CartesianMapDefinition where
-        targetType : Type ℓ
-        targetType = subQuotient (canonicalPER (M .assemblies x) (M .isModestFamily x))
-
-        opaque
-          equation : enlargePER (shrinkPER (canonicalPER (M .assemblies x) (M .isModestFamily x))) ≡ canonicalPER (M .assemblies x) (M .isModestFamily x)
-          equation = enlargePER⋆shrinkPER≡id (canonicalPER (M .assemblies x) (M .isModestFamily x))
-
-        mainMap : Σ[ a ∈ A ] (a ⊩[ M .assemblies x ] Mx) → subQuotient (canonicalPER (M .assemblies x) (M .isModestFamily x))
-        mainMap (a , a⊩Mx) = [ a ]
-
-        mainMap2Constant : 2-Constant mainMap
-        mainMap2Constant (a , a⊩Mx) (b , b⊩Mx) = eq/ a b (return (Mx , a⊩Mx , b⊩Mx))
-
-        opaque
-          target : targetType
-          target =
-            PT.rec→Set
-              squash/
-              mainMap
-              mainMap2Constant
-              (M .assemblies x .⊩surjective Mx)
-
-        opaque
-          isTrackedCartesianMap :
-            ∀ (a : A)
-            → a ⊩[ asmX ] x
-            → (b : A)
-            → b ⊩[ M .assemblies x ] Mx
-            → ⟨
-              subQuotientRealizability
-                (enlargePER (shrinkPER (canonicalPER (M .assemblies x) (M .isModestFamily x))))
-                (λ*2 (# one) ⨾ a ⨾ b)
-                (subst subQuotient (sym equation) target)
-              ⟩
-          isTrackedCartesianMap a a⊩x b b⊩Mx =
-            {!!}
+      subst
+        subQuotient
+        (sym
+          (enlargePER⋆shrinkPER≡id
+            (canonicalPER (M .assemblies x) (M .isModestFamily x))))
+        (Unresized.mainMap resizing asmX M x Mx)
     DisplayedUFamMap.isTracked fᴰ =
       do
         return
           (λ*2 (# one) ,
-           λ x a a⊩x Mx b b⊩Mx → {!CartesianMapDefinition.isTrackedCartesianMap x Mx a a⊩x b b⊩Mx!})
+          (λ x a a⊩x Mx b b⊩Mx →
+            equivFun
+              (propTruncIdempotent≃ {!!})
+              (do
+                (r , r⊩mainMap) ← Unresized.isTrackedMainMap resizing asmX M
+                return {!!})))
+
+    opaque
+      unfolding isCartesian'
+      cart' : isCartesian' f fᴰ
+      cart' {Y , asmY} {N} g hᴰ = {!!}
     
diff --git a/src/Realizability/Modest/SubQuotientCanonicalPERToOriginal.agda b/src/Realizability/Modest/SubQuotientCanonicalPERToOriginal.agda
new file mode 100644
index 0000000..319a0ad
--- /dev/null
+++ b/src/Realizability/Modest/SubQuotientCanonicalPERToOriginal.agda
@@ -0,0 +1,79 @@
+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.Foundations.Powerset
+open import Cubical.Foundations.Path
+open import Cubical.Foundations.Structure using (⟨_⟩; str)
+open import Cubical.Data.Sigma
+open import Cubical.Data.FinData
+open import Cubical.Data.Unit
+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.Reflection.RecordEquiv
+open import Cubical.Categories.Category
+open import Cubical.Categories.Displayed.Base
+open import Cubical.Categories.Displayed.Reasoning
+open import Cubical.Categories.Limits.Pullback
+open import Cubical.Categories.Functor hiding (Id)
+open import Cubical.Categories.Constructions.Slice
+open import Categories.CartesianMorphism
+open import Categories.GenericObject
+open import Realizability.CombinatoryAlgebra
+open import Realizability.ApplicativeStructure
+open import Realizability.PropResizing
+
+module Realizability.Modest.SubQuotientCanonicalPERToOriginal {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
+
+open import Realizability.Assembly.Base ca
+open import Realizability.Assembly.Morphism ca
+open import Realizability.Assembly.Terminal ca
+open import Realizability.Assembly.SetsReflectiveSubcategory ca
+open import Realizability.Modest.Base ca
+open import Realizability.Modest.UniformFamily ca
+open import Realizability.Modest.CanonicalPER ca
+open import Realizability.PERs.PER ca
+open import Realizability.PERs.SubQuotient ca
+
+open Assembly
+open CombinatoryAlgebra ca
+open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a)
+open Contravariant UNIMOD
+open UniformFamily
+open DisplayedUFamMap
+
+module
+  _ {X : Type ℓ}
+  (asmX : Assembly X)
+  (isModestAsmX : isModest asmX) where
+
+  theCanonicalPER : PER
+  theCanonicalPER = canonicalPER asmX isModestAsmX
+
+  theSubQuotient : Assembly (subQuotient theCanonicalPER)
+  theSubQuotient = subQuotientAssembly theCanonicalPER
+
+  invert : AssemblyMorphism theSubQuotient asmX
+  AssemblyMorphism.map invert sq = SQ.rec (asmX .isSetX) mainMap mainMapCoh sq where
+
+    mainMap : Σ[ a ∈ A ] (theCanonicalPER .PER.relation a a) → X
+    mainMap (a , a~a) = PT.rec→Set (asmX .isSetX) action 2ConstantAction a~a where
+      action : Σ[ x ∈ X ] ((a ⊩[ asmX ] x) × (a ⊩[ asmX ] x)) → X
+      action (x , _ , _) = x
+
+      2ConstantAction : 2-Constant action
+      2ConstantAction (x , a⊩x , _) (x' , a⊩x' , _) = isModestAsmX x x' a a⊩x a⊩x'
+
+    mainMapCoh : ∀ a b a~b → mainMap a ≡ mainMap b
+    mainMapCoh (a , a~a) (b , b~b) a~b =
+      PT.elim3
+        {P = λ a~a b~b a~b → mainMap (a , a~a) ≡ mainMap (b , b~b)}
+        (λ _ _ _ → asmX .isSetX _ _)
+        (λ { (x , a⊩x , _) (x' , b⊩x' , _) (x'' , a⊩x'' , b⊩x'') →
+          {!isModestAsmX x x' !} })
+        a~a
+        b~b
+        a~b
+  AssemblyMorphism.tracker invert = {!!}
diff --git a/src/Realizability/Modest/UnresizedGeneric.agda b/src/Realizability/Modest/UnresizedGeneric.agda
new file mode 100644
index 0000000..3ab06c1
--- /dev/null
+++ b/src/Realizability/Modest/UnresizedGeneric.agda
@@ -0,0 +1,88 @@
+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.Foundations.Powerset
+open import Cubical.Foundations.Path
+open import Cubical.Foundations.Structure using (⟨_⟩; str)
+open import Cubical.Data.Sigma
+open import Cubical.Data.FinData
+open import Cubical.Data.Unit
+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.Reflection.RecordEquiv
+open import Cubical.Categories.Category
+open import Cubical.Categories.Displayed.Base
+open import Cubical.Categories.Displayed.Reasoning
+open import Cubical.Categories.Limits.Pullback
+open import Cubical.Categories.Functor hiding (Id)
+open import Cubical.Categories.Constructions.Slice
+open import Categories.CartesianMorphism
+open import Categories.GenericObject
+open import Realizability.CombinatoryAlgebra
+open import Realizability.ApplicativeStructure
+open import Realizability.PropResizing
+
+module Realizability.Modest.UnresizedGeneric {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) (resizing : hPropResizing ℓ) where
+
+open import Realizability.Assembly.Base ca
+open import Realizability.Assembly.Morphism ca
+open import Realizability.Assembly.Terminal ca
+open import Realizability.Assembly.SetsReflectiveSubcategory ca
+open import Realizability.Modest.Base ca
+open import Realizability.Modest.UniformFamily ca
+open import Realizability.Modest.CanonicalPER ca
+open import Realizability.PERs.PER ca
+open import Realizability.PERs.ResizedPER ca resizing
+open import Realizability.PERs.SubQuotient ca
+
+open Assembly
+open CombinatoryAlgebra ca
+open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a)
+open Contravariant UNIMOD
+open UniformFamily
+open DisplayedUFamMap
+
+module Unresized
+  {X : Type ℓ}
+  (asmX : Assembly X)
+  (M : UniformFamily asmX) where
+
+  theCanonicalPER : ∀ x → PER
+  theCanonicalPER x = canonicalPER (M . assemblies x) (M .isModestFamily x)
+
+  elimRealizerForMx : ∀ {x : X} {Mx : M .carriers x} → Σ[ a ∈ A ] (a ⊩[ M .assemblies x ] Mx) → subQuotient (canonicalPER (M .assemblies x) (M .isModestFamily x))
+  elimRealizerForMx {x} {Mx} (a , a⊩Mx) = [ a , (return (Mx , a⊩Mx , a⊩Mx)) ]
+  
+  elimRealizerForMx2Constant : ∀ {x Mx} → 2-Constant (elimRealizerForMx {x} {Mx})
+  elimRealizerForMx2Constant {x} {Mx} (a , a⊩Mx) (b , b⊩Mx) =
+    eq/
+      (a , (return (Mx , a⊩Mx , a⊩Mx)))
+      (b , return (Mx , b⊩Mx , b⊩Mx))
+      (return (Mx , a⊩Mx , b⊩Mx))
+
+  mainMap : (x : X) (Mx : M .carriers x) → subQuotient (canonicalPER (M .assemblies x) (M .isModestFamily x))
+  mainMap x Mx =
+    PT.rec→Set
+      squash/
+      (elimRealizerForMx {x = x} {Mx = Mx})
+      (elimRealizerForMx2Constant {x = x} {Mx = Mx})
+      (M .assemblies x .⊩surjective Mx)
+      
+  opaque
+    isTrackedMainMap : ∃[ r ∈ A ] (∀ (x : X) (a : A) → a ⊩[ asmX ] x → (Mx : M .carriers x) → (b : A) → b ⊩[ M .assemblies x ] Mx → (r ⨾ a ⨾ b) ⊩[ subQuotientAssembly (theCanonicalPER x) ] (mainMap x Mx))
+    isTrackedMainMap =
+      return
+        ((λ*2 (# zero)) ,
+        (λ x a a⊩x Mx b b⊩Mx →
+           PT.elim
+             {P = λ MxRealizer → (λ*2 (# zero) ⨾ a ⨾ b) ⊩[ subQuotientAssembly (theCanonicalPER x) ] (PT.rec→Set squash/ (elimRealizerForMx {x = x} {Mx = Mx}) (elimRealizerForMx2Constant {x = x} {Mx = Mx}) MxRealizer)}
+             (λ ⊩Mx → subQuotientAssembly (theCanonicalPER x) .⊩isPropValued (λ*2 (# zero) ⨾ a ⨾ b) (rec→Set squash/ elimRealizerForMx elimRealizerForMx2Constant ⊩Mx))
+             (λ { (c , c⊩Mx) →
+               subst
+                 (_⊩[ subQuotientAssembly (theCanonicalPER x) ] (elimRealizerForMx (c , c⊩Mx)))
+                 (sym (λ*2ComputationRule (# zero) a b))
+                 (return (Mx , b⊩Mx , c⊩Mx))})
+             (M .assemblies x .⊩surjective Mx)))
diff --git a/src/Realizability/PERs/SubQuotient.agda b/src/Realizability/PERs/SubQuotient.agda
index e28420a..0c12f24 100644
--- a/src/Realizability/PERs/SubQuotient.agda
+++ b/src/Realizability/PERs/SubQuotient.agda
@@ -35,48 +35,51 @@ open Combinators ca renaming (i to Id; ia≡a to Ida≡a)
 module _
   (per : PER) where
 
+  domain : Type ℓ
+  domain = Σ[ a ∈ A ] (per .PER.relation a a)
+
   subQuotient : Type ℓ
-  subQuotient = A / per .PER.relation
+  subQuotient = domain / λ { (a , _) (b , _) → per .PER.relation a b }
 
   subQuotientRealizability : A → subQuotient → hProp ℓ
   subQuotientRealizability r [a] =
     SQ.rec
       isSetHProp
-      (λ a → ([ a ] ≡ [ r ]) , squash/ [ a ] [ r ])
-      (λ a b a~b →
+      (λ { (a , a~a) → r ~[ per ] a , isProp~ r per a })
+      (λ { (a , a~a) (b , b~b) a~b →
         Σ≡Prop
-          (λ _ → isPropIsProp)
-          (hPropExt (squash/ [ a ] [ r ]) (squash/ [ b ] [ r ]) (λ [a]≡[r] → sym (eq/ a b a~b) ∙ [a]≡[r]) λ [b]≡[r] → sym (eq/ b a (per .PER.isPER .fst a b a~b)) ∙ [b]≡[r]))
+          (λ x → isPropIsProp)
+          (hPropExt
+            (isProp~ r per a)
+            (isProp~ r per b)
+            (λ r~a → PER.isTransitive per r a b r~a a~b)
+            (λ r~b → PER.isTransitive per r b a r~b (PER.isSymmetric per a b a~b))) })
       [a]
-
+      
+  
   subQuotientAssembly : Assembly subQuotient
   Assembly._⊩_ subQuotientAssembly r [a] = ⟨ subQuotientRealizability r [a] ⟩
   Assembly.isSetX subQuotientAssembly = squash/
   Assembly.⊩isPropValued subQuotientAssembly r [a] = str (subQuotientRealizability r [a])
   Assembly.⊩surjective subQuotientAssembly [a] =
-    do
-      (a , [a]≡[a]) ← []surjective [a]
-      return
-        (a , (subst (λ [a] → ⟨ subQuotientRealizability a [a] ⟩) [a]≡[a] refl))
+    SQ.elimProp
+      {P = λ [a] → ∃[ r ∈ A ] ⟨ subQuotientRealizability r [a] ⟩}
+      (λ [a] → isPropPropTrunc)
+      (λ { (a , a~a) → return (a , a~a) })
+      [a]
 
+  
   isModestSubQuotientAssembly : isModest subQuotientAssembly
   isModestSubQuotientAssembly x y a a⊩x a⊩y =
     SQ.elimProp2
-      {P = motive}
+      {P = λ x y → motive x y}
       isPropMotive
-      coreMap
-      x y a a⊩x a⊩y where
-        motive : subQuotient → subQuotient → Type ℓ
-        motive x y = (a : A) → a ⊩[ subQuotientAssembly ] x → a ⊩[ subQuotientAssembly ] y → x ≡ y
+      (λ { (x , x~x) (y , y~y) a a~x a~y →
+        eq/ (x , x~x) (y , y~y) (PER.isTransitive per x a y (PER.isSymmetric per a x a~x) a~y) })
+      x y
+      a a⊩x a⊩y where
+        motive : ∀ (x y : subQuotient) → Type ℓ
+        motive x y = ∀ (a : A) (a⊩x : a ⊩[ subQuotientAssembly ] x) (a⊩y : a ⊩[ subQuotientAssembly ] y) → x ≡ y
 
         isPropMotive : ∀ x y → isProp (motive x y)
         isPropMotive x y = isPropΠ3 λ _ _ _ → squash/ x y
-
-        coreMap : (r s : A) → motive [ r ] [ s ]
-        coreMap r s a a⊩[r] a⊩[s] =
-          [ r ]
-            ≡⟨ a⊩[r] ⟩
-          [ a ]
-            ≡⟨ sym a⊩[s] ⟩
-          [ s ]
-            ∎