Prove universal property of ASM

rahulc29 · Nov 10, 2023 · 2bd10d0 · 2bd10d0
1 parent 843daf0
commit 2bd10d0
Showing 1 changed file with 25 additions and 2 deletions.
diff --git a/src/Realizability/Assembly.agda b/src/Realizability/Assembly.agda
@@ -579,7 +579,7 @@ module Realizability.Assembly {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) w
       coequalizer .isSetX = squash
       coequalizer ._⊩_ a x = (a ⊩coeq x) .fst
       coequalizer .⊩isPropValued a x = (a ⊩coeq x) .snd
-      coequalizer .⊩surjective x = {!!}
+      coequalizer .⊩surjective x = ⊩coeqSurjective x
 
       ⊩coeqSurjective x =
         setCoequalizerElimProp
@@ -590,7 +590,30 @@ module Realizability.Assembly {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) w
                   return (b~ , b~⊩coeq_inc_b b b~ b~realizes))
           x where
             b~⊩coeq_inc_b : (b : Y) (b~ : A) (b~realizes : b~ ⊩Y b) → (b~ ⊩coeq inc b) .fst
-            b~⊩coeq_inc_b b b~ b~realizes = {!!}
+            b~⊩coeq_inc_b b b~ b~realizes = ∣ b , refl , b~realizes ∣₁
+      {-
+        Coequalziers have a map E ← Y ⇇ X
+      -}
+      ιcoequalizer : AssemblyMorphism ys coequalizer
+      ιcoequalizer .map = inc
+      ιcoequalizer .tracker = ∣ Id , (λ y yᵣ yᵣ⊩y → subst (λ r → (r ⊩coeq inc y) .fst) (sym (Ida≡a yᵣ)) ∣ y , refl , yᵣ⊩y ∣₁) ∣₁
+
+      coequalizerFactors : ((Z , zs) : Σ[ Z ∈ Type ℓ ] Assembly Z)
+                         → (ι' : AssemblyMorphism ys zs)
+                         → (f ⊚ ι' ≡ g ⊚ ι')
+                         → ∃![ ! ∈ AssemblyMorphism coequalizer zs ] (ιcoequalizer ⊚ ! ≡ ι')
+      coequalizerFactors (Z , zs) ι' f⊚ι'≡g⊚ι' =
+        uniqueExists (λ where
+                        .map → setCoequalizerRec (zs .isSetX) (ι' .map) λ x → λ i → f⊚ι'≡g⊚ι' i .map x
+                        .tracker → {!!})
+                        (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)
+
 
   -- ASM is regular
   module _