Regular monomorphisms are stable under pullbacks

src/Category/Limit.ard

@@ -736,7 +736,39 @@
 \lemma regularMono_Mono {C : Precat} {x y : C} {f : Hom x y} (reg : isRegularMono f) : Mono f \elim reg
   | inP (E : Equalizer) => \new Mono f E.eqMono
 
-\lemma regularMono_pullback (P : Pullback {}) (m : isRegularMono P.g) : isRegularMono P.pbProj1 => {?}
+\lemma mono_pullback (P : Pullback {}) (m : Mono P.g): Mono P.pbProj1 =>
+  \new Mono {
+    | isMono {_} {g} {h} p1 =>
+      \let p2 =>
+        inv o-assoc *> transport (\lam a => a ∘ g = a ∘ h) P.pbCoh (o-assoc *> pmap (o P.f) p1 <* inv o-assoc) <* o-assoc
+      \in
+        pbEta p1 (m.isMono p2)
+  }
+
+\lemma regularMono_pullback (P : Pullback {}) (m : isRegularMono P.g) : isRegularMono P.pbProj1 =>
+  \case m \with {
+    | inP (E : Equalizer) =>
+      inP (\new Equalizer {
+        | Y => E.Y
+        | f => o E.f P.f
+        | g => o E.g P.f
+        | equal =>
+          rewrite (o-assoc, o-assoc, P.pbCoh) $
+          rewriteI (o-assoc, o-assoc) $
+          rewrite E.equal idp
+        | isEqualizer _ =>
+          \new QEquiv {
+            | ret (z->Px, z->Px_proof) =>
+              pbMap
+                  z->Px
+                  (E.eqMap (o P.f z->Px) (inv o-assoc *> z->Px_proof *> o-assoc))
+                  (rewrite E.eqBeta idp)
+            | ret_f _ => isMono {mono_pullback P (regularMono_Mono m)} P.pbBeta1
+            | f_sec _ => ext P.pbBeta1
+          }
+      })
+  }
+
 
 {- | If both squares are pullbacks, then the outter rectangle is a pullback.
   Q  -->  P  --> P.y