Show mere existence of equalisers

rahulc29 · Mar 6, 2024 · 6a7058d · 6a7058d
1 parent 18b9d94
commit 6a7058d
Showing 1 changed file with 12 additions and 2 deletions.
diff --git a/src/Realizability/Topos/Equalizer.agda b/src/Realizability/Topos/Equalizer.agda
@@ -535,8 +535,18 @@ module _
     equalizer =
       SQ.elimProp2
         {P = λ f g → ∃[ equalizerOb ∈ PartialEquivalenceRelation X ] ∃[ inc ∈ RTMorphism equalizerOb perX ] (equalizerUnivProp perX perY f g equalizerOb inc)}
-        {!!}
+        (λ f g → isPropPropTrunc)
         (λ F G →
-          {!!})
+          return
+            ((equalizerPer F G) ,
+            (return
+              ((equalizerMorphism F G) ,
+              (λ perZ h h⋆f≡h⋆g →
+                uniqueExists
+                  (UnivProp.mainMap F G perZ h h⋆f≡h⋆g .fst)
+                  (UnivProp.mainMap F G perZ h h⋆f≡h⋆g .snd .fst)
+                  (λ !' → squash/ _ _)
+                  λ !' !'⋆inc≡h →
+                    sym (UnivProp.mainMap F G perZ h h⋆f≡h⋆g .snd .snd !' !'⋆inc≡h))))))
         f g