Library UniMath.CategoryTheory.DisplayedCats.Codomain.CodRegular

  revert H.
  use factor_through_squash.
  {
    apply isaprop_is_regular_epi.
  }
  intros H.
  induction H as ( w & g₁ & g₂ & p & H ).
  use hinhpr.
  simple refine (_ ,, _ ,, _ ,, _ ,, _).
  - exact (make_cod_fib_ob (g₁ · cod_mor yg₁)).
  - use make_cod_fib_mor.
    + exact g₁.
    + abstract
        (cbn ;
         apply idpath).
  - use make_cod_fib_mor.
    + exact g₂.
    + abstract
        (cbn ;
         rewrite <- (mor_eq hp) ; cbn ;
         rewrite !assoc ;
         apply maponpaths_2 ;
         exact (!p)).
  - abstract
      (use eq_mor_cod_fib ;
       rewrite !comp_in_cod_fib ; cbn ;
       exact p).
  - use is_coequalizer_cod_fib.
    + exact p.
    + exact H.

Definition from_regular_epi_in_slice
           {C : category}
           (PB : Pullbacks C)
           (EC : coeqs_of_kernel_pair C)
           (HC : regular_epi_pb_stable C)
           {x : C}
           {yg₁ zg₂ : C /x}
           {hp : yg₁ --> zg₂}
           (H : is_regular_epi hp)
  : is_regular_epi (dom_mor hp).
Show proof.

  apply (is_regular_epi_strong_epi PB EC HC).
  apply (is_strong_epi_extremal_epi PB).
  intros z f g p Hg.
  pose (wh := (make_cod_fib_ob (g · cod_mor zg₂)) : C/x).
  assert (f · (g · cod_mor zg₂) = cod_mor yg₁) as q₁.
  {
    rewrite assoc.
    rewrite <- p.
    exact (mor_eq hp).
  }
  pose (φ := @make_cod_fib_mor _ _ yg₁ wh f q₁).
  assert (g · cod_mor zg₂ = cod_mor wh) as q₂.
  {
    apply idpath.
  }
  pose (ψ := @make_cod_fib_mor _ _ wh zg₂ g q₂).
  assert (hp = φ · ψ) as q₃.
  {
    use eq_mor_cod_fib.
    rewrite comp_in_cod_fib.
    cbn.
    exact p.
  }
  assert (isMonic ψ) as Hψ.
  {
    use is_monic_cod_fib.
    exact Hg.
  }
  pose (is_extremal_epi_strong_epi (is_strong_epi_regular_epi H) wh φ ψ q₃ Hψ) as H'.
  use make_is_z_isomorphism.
  - exact (pr11 H').
  - split.
    + refine (_ @ maponpaths dom_mor (pr12 H')).
      rewrite comp_in_cod_fib.
      apply idpath.
    + refine (_ @ maponpaths dom_mor (pr22 H')).
      rewrite comp_in_cod_fib.
      apply idpath.

Definition regular_epi_in_slice_weq
           {C : category}
           (PB : Pullbacks C)
           (EC : coeqs_of_kernel_pair C)
           (HC : regular_epi_pb_stable C)
           {x : C}
           {yg₁ zg₂ : C /x}
           (hp : yg₁ --> zg₂)
  : is_regular_epi hp ≃ is_regular_epi (pr1 hp).
Show proof.

  use weqimplimpl.
  - apply (from_regular_epi_in_slice PB EC HC).
  - apply to_regular_epi_in_slice.
  - apply isaprop_is_regular_epi.
  - apply isaprop_is_regular_epi.

      refine (_ @ maponpaths dom_mor (PullbackSqrCommutes K) @ _).
      - rewrite comp_in_cod_fib.
        apply idpath.
      - rewrite comp_in_cod_fib.
        apply idpath.

    Definition to_kernel_pair_slice
      : kernel_pair h.
    Show proof.

      use make_Pullback.
      - exact p.
      - exact π ₁.
      - exact π ₂.
      - exact to_kernel_pair_slice_eq.
      - use from_is_pullback_slice.
        + abstract
            (exact (PullbackSqrCommutes K)).
        + exact (isPullback_Pullback K).

    Let Coeq : Coequalizer π ₁ π ₂ := EC y z h to_kernel_pair_slice.

    Definition coeq_of_kernel_pair_slice_ob_mor
      : Coeq --> x.
    Show proof.

      use CoequalizerOut.
      - exact f.
      - abstract
          (exact (mor_eq q π ₁ @ !(mor_eq q π ₂ ))).

    Definition coeq_of_kernel_pair_slice_ob
      : C /x.
    Show proof.

      use make_cod_fib_ob.
      - exact Coeq.
      - exact coeq_of_kernel_pair_slice_ob_mor.

    Definition coeq_of_kernel_pair_slice_coeq_arr
      : yf --> coeq_of_kernel_pair_slice_ob.
    Show proof.

      use make_cod_fib_mor.
      - apply CoequalizerArrow.
      - abstract
          (cbn ; unfold coeq_of_kernel_pair_slice_ob_mor ;
           rewrite CoequalizerCommutes ;
           apply idpath ).

    Proposition coeq_of_kernel_pair_slice_coeq_arr_eq
      : PullbackPr1 K · coeq_of_kernel_pair_slice_coeq_arr
        =
        PullbackPr2 K · coeq_of_kernel_pair_slice_coeq_arr.
    Show proof.

      use eq_mor_cod_fib.
      rewrite !comp_in_cod_fib.
      apply CoequalizerEqAr.

    Definition coeq_of_kernel_pair_slice
      : Coequalizer (PullbackPr1 K) (PullbackPr2 K).
    Show proof.

      use make_Coequalizer.
      - exact coeq_of_kernel_pair_slice_ob.
      - exact coeq_of_kernel_pair_slice_coeq_arr.
      - exact coeq_of_kernel_pair_slice_coeq_arr_eq.
      - use is_coequalizer_cod_fib.
        + apply (CoequalizerEqAr Coeq).
        + exact (isCoequalizer_Coequalizer Coeq).

  End CoeqSlice.

  Definition cod_fib_coeqs_of_kernel_pair
    : coeqs_of_kernel_pair (C /x)
    := λ yf zg hp K , coeq_of_kernel_pair_slice hp K.

  Definition cod_fib_regular_epi_pb_stable
    : regular_epi_pb_stable (C /x).
  Show proof.

    intros a b c d f g π₁ π₂ p H Hf.
    use to_regular_epi_in_slice.
    apply (from_regular_epi_in_slice PB EC HC) in Hf.
    assert (dom_mor π₁ · dom_mor f = dom_mor π₂ · dom_mor g) as q.
    {
      rewrite <- !comp_in_cod_fib.
      apply maponpaths.
      exact p.
    }
    pose (from_is_pullback_slice _ _ _ _ q _ H) as H'.
    use (HC _ _ _ _ _ _ _ _ _ H').
    exact Hf.

  Definition is_regular_category_cod_fib
    : is_regular_category (C /x).
  Show proof.

    repeat split.
    - apply codomain_fib_terminal.
    - apply codomain_fiberwise_pullbacks.
      exact PB.
    - exact cod_fib_coeqs_of_kernel_pair.
    - exact cod_fib_regular_epi_pb_stable.

End SliceRegular.

3. Preservation of regular epimorphisms by the pullback functor

Section PullbackStable.
  Context {C : category}
          (PB : Pullbacks C)
          (EC : coeqs_of_kernel_pair C)
          (HC : regular_epi_pb_stable C).

  Section PreservesFromStable.
    Context {x y : C}
            (f : x --> y)
            {zg₁ zg₂ : C /y}
            (hp : zg₁ --> zg₂).

    Let z₁ : C := cod_dom zg₁.
    Let z₂ : C := cod_dom zg₂.
    Let g₁ : z₁ --> y := cod_mor zg₁.
    Let g₂ : z₂ --> y := cod_mor zg₂.
    Let h : z₁ --> z₂ := dom_mor hp.

    Let P₁ : Pullback g₁ f := PB _ _ _ g₁ f.
    Let π ₁ : P₁ --> z₁ := PullbackPr1 P₁.
    Let π ₂ : P₁ --> x := PullbackPr2 P₁.

    Let P₂ : Pullback g₂ f := PB _ _ _ g₂ f.
    Let ρ ₁ : P₂ --> z₂ := PullbackPr1 P₂.
    Let ρ ₂ : P₂ --> x := PullbackPr2 P₂.

    Context (r : π ₁ · h · g₂ = π ₂ · f).

    Let k : P₁ --> P₂
      := PullbackArrow P₂ P₁ (π ₁ · h) π ₂ r.

    Lemma regular_epi_pb_stable_to_pb_preserves_pb_sqr_eq
      : π ₁ · h = k · ρ ₁.
    Show proof.

refine (!_).
apply PullbackArrow_PullbackPr1.

    Lemma regular_epi_pb_stable_to_pb_preserves_pb_sqr
      : isPullback regular_epi_pb_stable_to_pb_preserves_pb_sqr_eq.
    Show proof.

      intros w l l' q.
      use iscontraprop1.
      - use invproofirrelevance.
        intros ζ₁ ζ₂.
        use subtypePath.
        {
          intro.
          apply isapropdirprod ; apply homset_property.
        }
        use (MorphismsIntoPullbackEqual (isPullback_Pullback P₁)).
        + exact (pr12 ζ₁ @ !(pr12 ζ₂)).
        + pose (maponpaths (λ z , z · PullbackPr2 P₂) (pr22 ζ₁ @ !(pr22 ζ₂))) as qr.
          cbn in qr.
          rewrite !assoc' in qr.
          unfold k in qr.
          rewrite !PullbackArrow_PullbackPr2 in qr.
          exact qr.
      - simple refine (_ ,, _ ,, _).
        + use PullbackArrow.
          * exact l.
          * exact (l' · ρ ₂).
          * refine (maponpaths (λ z , _ · z) (!(mor_eq hp )) @ _).
            rewrite !assoc.
            refine (maponpaths (λ z , z · _) q @ _).
            rewrite !assoc'.
            apply maponpaths.
            apply PullbackSqrCommutes.
        + apply PullbackArrow_PullbackPr1.
        + use (MorphismsIntoPullbackEqual (isPullback_Pullback P₂)).
          * unfold k.
            refine (assoc' _ _ _ @ _).
            rewrite PullbackArrow_PullbackPr1.
            refine (assoc _ _ _ @ _).
            rewrite PullbackArrow_PullbackPr1.
            exact q.
          * unfold k.
            refine (assoc' _ _ _ @ _).
            rewrite !PullbackArrow_PullbackPr2.
            apply idpath.

    Let HP' := regular_epi_pb_stable_to_pb_preserves_pb_sqr.
    Let P' := make_Pullback _ HP'.

    Lemma regular_epi_pb_stable_to_pb_preserves_lem
          (Hp : is_regular_epi hp)
      : is_regular_epi k.
    Show proof.

      use (HC _ _ _ _ _ _ _ _ _ HP').
      apply (from_regular_epi_in_slice PB EC HC).
      exact Hp.

  End PreservesFromStable.

  Definition regular_epi_pb_stable_to_pb_preserves
             {x y : C}
             (f : x --> y)
    : preserves_regular_epi (cod_pb PB f).
  Show proof.

    intros g h p Hp.
    use to_regular_epi_in_slice.
    rewrite cod_fiber_functor_on_mor.
    exact (regular_epi_pb_stable_to_pb_preserves_lem f p _ Hp).

End PullbackStable.

4. Preservation of regular epimorphisms by the codomain functor

Definition preserves_regular_epi_fiber_disp_cod
           {C₁ C₂ : category}
           (PB : Pullbacks C₁)
           (EC : coeqs_of_kernel_pair C₁)
           (HC : regular_epi_pb_stable C₁)
           (F : C₁ ⟶ C₂)
           (HF : preserves_regular_epi F)
           (x : C₁)
  : preserves_regular_epi (fiber_functor (disp_codomain_functor F) x).
Show proof.

  intros fy gz hp Hf.
  use to_regular_epi_in_slice.
  rewrite disp_codomain_fiber_functor_mor.
  apply HF.
  exact (from_regular_epi_in_slice PB EC HC Hf).

  use (maponpaths
         dom_mor
         (@internal_relation_monic
             _ _
             R
             (make_cod_fib_ob (f · cod_mor R))
             (make_cod_fib_mor _ _)
             (make_cod_fib_mor _ _)
             _ _)).
  - apply idpath.
  - cbn.
    rewrite <- !(mor_eq (internal_relation_src R)).
    rewrite !assoc.
    apply maponpaths_2.
    exact (!p).
  - use eq_mor_cod_fib.
    rewrite !comp_in_cod_fib.
    cbn.
    exact p.
  - use eq_mor_cod_fib.
    rewrite !comp_in_cod_fib.
    cbn.
    exact q.

Definition from_internal_relation_slice
           {C : category}
           {x : C}
           {zf : C /x}
           (R : internal_relation zf)
  : internal_relation (cod_dom zf).
Show proof.

  use make_internal_relation.
  - exact (cod_dom R).
  - exact (dom_mor (internal_relation_src R)).
  - exact (dom_mor (internal_relation_tar R)).
  - exact (from_internal_relation_slice_monic R).

Proposition isrefl_from_internal_is_eqrel_slice
            {C : category}
            {x : C}
            {zf : C /x}
            (R : internal_eqrel zf)
  : internal_isrefl (from_internal_relation_slice R).
Show proof.

  intros w g.
  pose (w' := make_cod_fib_ob (g · cod_mor zf)).
  assert (g · cod_mor zf = cod_mor w') as p.
  {
    apply idpath.
  }
  pose (g' := @make_cod_fib_mor _ _ w' zf g p).
  pose (r := isrefl_internal_eqrel R w' g' : internal_relation_to_arr_relation _ _ _).
  use make_internal_relation_to_arr_relation.
  - exact (dom_mor r).
  - refine (!(comp_in_cod_fib r _) @ _).
    rewrite (internal_relation_to_arr_relation_src r).
    apply idpath.
  - refine (!(comp_in_cod_fib r _) @ _).
    rewrite (internal_relation_to_arr_relation_tar r).
    apply idpath.

Proposition issymm_from_internal_is_eqrel_slice
            {C : category}
            {x : C}
            {zf : C /x}
            (R : internal_eqrel zf)
  : internal_issymm (from_internal_relation_slice R).
Show proof.

  intros w g₁ g₂ p.
  pose (w' := make_cod_fib_ob (g₁ · cod_mor zf)).
  induction p as [ h [ p₁ p₂ ]].
  cbn in h, p₁, p₂.
  assert (g₁ · cod_mor zf = cod_mor w') as q₁.
  {
    apply idpath.
  }
  pose (g₁' := @make_cod_fib_mor _ _ w' zf g₁ q₁).
  assert (g₂ · cod_mor zf = cod_mor w') as q₂.
  {
    cbn.
    rewrite <- p₁, <- p₂.
    rewrite !assoc'.
    rewrite (mor_eq (internal_relation_src R)).
    rewrite (mor_eq (internal_relation_tar R)).
    apply idpath.
  }
  pose (g₂' := @make_cod_fib_mor _ _ w' zf g₂ q₂).
  assert (internal_relation_to_arr_hrel R w' g₁' g₂') as H.
  {
    use make_internal_relation_to_arr_relation.
    - use make_cod_fib_mor.
      + exact h.
      + cbn.
        rewrite <- p₁.
        rewrite !assoc'.
        rewrite (mor_eq (internal_relation_src R)).
        apply idpath.
    - use eq_mor_cod_fib.
      rewrite comp_in_cod_fib.
      cbn.
      exact p₁.
    - use eq_mor_cod_fib.
      rewrite comp_in_cod_fib.
      cbn.
      exact p₂.
  }
  pose (r := issymm_internal_eqrel R w' g₁' g₂' H : internal_relation_to_arr_relation _ _ _).
  use make_internal_relation_to_arr_relation.
  - exact (dom_mor r).
  - refine (!(comp_in_cod_fib r _) @ _).
    rewrite (internal_relation_to_arr_relation_src r).
    apply idpath.
  - refine (!(comp_in_cod_fib r _) @ _).
    rewrite (internal_relation_to_arr_relation_tar r).
    apply idpath.

Proposition istrans_from_internal_is_eqrel_slice
            {C : category}
            {x : C}
            {zf : C /x}
            (R : internal_eqrel zf)
  : internal_istrans (from_internal_relation_slice R).
Show proof.

  intros w g₁ g₂ g₃ p q.
  pose (w' := make_cod_fib_ob (g₁ · cod_mor zf)).
  induction p as [ h [ p₁ p₂ ]].
  induction q as [ k [ q₁ q₂ ]].
  cbn in h, p₁, p₂, k, q₁, q₂.
  assert (g₁ · cod_mor zf = cod_mor w') as r₁.
  {
    apply idpath.
  }
  pose (g₁' := @make_cod_fib_mor _ _ w' zf g₁ r₁).
  assert (g₂ · cod_mor zf = cod_mor w') as r₂.
  {
    cbn.
    rewrite <- p₁, <- p₂.
    rewrite !assoc'.
    rewrite (mor_eq (internal_relation_src R)).
    rewrite (mor_eq (internal_relation_tar R)).
    apply idpath.
  }
  pose (g₂' := @make_cod_fib_mor _ _ w' zf g₂ r₂).
  assert (k · cod_mor R = h · cod_mor R) as lem.
  {
    etrans.
    {
      rewrite <- (mor_eq (internal_relation_src R)).
      rewrite !assoc.
      rewrite q₁.
      apply idpath.
    }
    rewrite <- (mor_eq (internal_relation_tar R)).
    rewrite !assoc.
    rewrite p₂.
    apply idpath.
  }
  assert (g₃ · cod_mor zf = cod_mor w') as r₃.
  {
    cbn.
    rewrite <- p₁, <- q₂.
    rewrite !assoc'.
    rewrite (mor_eq (internal_relation_src R)).
    rewrite (mor_eq (internal_relation_tar R)).
    exact lem.
  }
  pose (g₃' := @make_cod_fib_mor _ _ w' zf g₃ r₃).
  assert (internal_relation_to_arr_hrel R w' g₁' g₂') as H₁.
  {
    use make_internal_relation_to_arr_relation.
    - use make_cod_fib_mor.
      + exact h.
      + cbn.
        rewrite <- p₁.
        rewrite !assoc'.
        rewrite (mor_eq (internal_relation_src R)).
        apply idpath.
    - use eq_mor_cod_fib.
      rewrite comp_in_cod_fib ; cbn.
      exact p₁.
    - use eq_mor_cod_fib.
      rewrite comp_in_cod_fib ; cbn.
      exact p₂.
  }
  assert (internal_relation_to_arr_hrel R w' g₂' g₃') as H₂.
  {
    use make_internal_relation_to_arr_relation.
    - use make_cod_fib_mor.
      + exact k.
      + cbn.
        rewrite <- p₁.
        rewrite !assoc'.
        rewrite (mor_eq (internal_relation_src R)).
        exact lem.
    - use eq_mor_cod_fib.
      rewrite comp_in_cod_fib ; cbn.
      exact q₁.
    - use eq_mor_cod_fib.
      rewrite comp_in_cod_fib ; cbn.
      exact q₂.
  }
  pose (r := istrans_internal_eqrel R w' g₁' g₂' g₃' H₁ H₂).
  cbn in r.
  use make_internal_relation_to_arr_relation.
  - exact (dom_mor r).
  - refine (!(comp_in_cod_fib r _) @ _).
    rewrite (internal_relation_to_arr_relation_src r).
    apply idpath.
  - refine (!(comp_in_cod_fib r _) @ _).
    rewrite (internal_relation_to_arr_relation_tar r).
    apply idpath.

Proposition from_internal_is_eqrel_slice
            {C : category}
            {x : C}
            {zf : C /x}
            (R : internal_eqrel zf)
  : internal_iseqrel (from_internal_relation_slice R).
Show proof.

  repeat split.
  - exact (isrefl_from_internal_is_eqrel_slice R).
  - exact (issymm_from_internal_is_eqrel_slice R).
  - exact (istrans_from_internal_is_eqrel_slice R).

Definition from_internal_eqrel_slice
           {C : category}
           {x : C}
           {zf : C /x}
           (R : internal_eqrel zf)
  : internal_eqrel (cod_dom zf).
Show proof.

  use make_internal_eqrel.
  - exact (from_internal_relation_slice R).
  - exact (from_internal_is_eqrel_slice R).

Section Exactness.
  Context {C : category}
          {x : C}
          {zf : C /x}
          (R : internal_eqrel zf)
          (Coeq : Coequalizer
                    (dom_mor (internal_relation_src R))
                    (dom_mor (internal_relation_tar R))).

  Definition internal_eqrel_coequalizer_ob
    : C /x.
  Show proof.

    use make_cod_fib_ob.
    - exact Coeq.
    - use CoequalizerOut.
      + exact (cod_mor zf).
      + abstract
          (rewrite (mor_eq (internal_relation_src R)) ;
           rewrite (mor_eq (internal_relation_tar R)) ;
           apply idpath).

  Definition internal_eqrel_coequalizer_arr
    : zf --> internal_eqrel_coequalizer_ob.
  Show proof.

    use make_cod_fib_mor.
    - exact (CoequalizerArrow Coeq).
    - abstract
        (cbn ;
         rewrite CoequalizerCommutes ;
         apply idpath).

  Proposition internal_eqrel_coequalizer_eq
    : internal_relation_src R · internal_eqrel_coequalizer_arr
      =
      internal_relation_tar R · internal_eqrel_coequalizer_arr.
  Show proof.

    use eq_mor_cod_fib.
    rewrite !comp_in_cod_fib.
    apply CoequalizerEqAr.

  Definition internal_eqrel_coequalizer
    : Coequalizer (internal_relation_src R) (internal_relation_tar R).
  Show proof.

    use make_Coequalizer.
    - exact internal_eqrel_coequalizer_ob.
    - exact internal_eqrel_coequalizer_arr.
    - exact internal_eqrel_coequalizer_eq.
    - use is_coequalizer_cod_fib.
      + apply CoequalizerEqAr.
      + exact (isCoequalizer_Coequalizer Coeq).

End Exactness.

Definition all_internal_eqrel_effective_fiber_disp_cod
           {C : category}
           (H : all_internal_eqrel_effective C)
           (x : C)
  : all_internal_eqrel_effective (C /x).
Show proof.

  intros zf R.
  pose (HE := H _ (from_internal_eqrel_slice R)).
  pose (Coeq := pr1 HE).
  simple refine (_ ,, _).
  - exact (internal_eqrel_coequalizer R Coeq).
  - abstract
      (use to_is_pullback_slice ; [ | apply HE ]).

Definition is_exact_disp_cod
           {C : category}
           (H : is_exact C)
           (x : C)
  : is_exact (C /x).
Show proof.

  pose (H' := is_exact_to_is_regular H).
  split.
  - use is_regular_category_cod_fib.
    + exact (is_regular_category_pullbacks H').
    + exact (is_regular_category_coeqs_of_kernel_pair H').
    + exact (is_regular_category_regular_epi_pb_stable H').
  - use all_internal_eqrel_effective_fiber_disp_cod.
    exact (is_exact_to_all_internal_eqrel_effective H).

Library UniMath.CategoryTheory.DisplayedCats.Codomain.CodRegular

1. Regular epimorphisms in the slice category

2. Regular categories are closed under slicing

3. Preservation of regular epimorphisms by the pullback functor

4. Preservation of regular epimorphisms by the codomain functor

5. Exactness of the slice category