Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.
Require Import UniMath.CategoryTheory.DisplayedCats.Fiber.
Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseCoproducts.
Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine.
Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine.
Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERs.
Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERMorphisms.
Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERCategory.
Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.Logic.SubobjectDispCat.

Local Open Scope cat.
Local Open Scope hd.

Section Disjunction.
  Context (H : first_order_hyperdoctrine).

  Section Disjunction.
    Context {Γ : partial_setoid H}
            (ψ₁ ψ₂ : per_subobject Γ).

    Proposition per_subobject_disj_laws
      : per_subobject_laws (ψ₁ ∨ ψ₂).
    Proof.
      split.
      - use forall_intro.
        use impl_intro.
        use weaken_right.
        hypersimplify.
        use (disj_elim (hyperdoctrine_hyp _)).
        + use weaken_right.
          use (per_subobject_def ψ₁).
          apply hyperdoctrine_hyp.
        + use weaken_right.
          use (per_subobject_def ψ₂).
          apply hyperdoctrine_hyp.
      - do 2 use forall_intro.
        use impl_intro.
        use weaken_right.
        use impl_intro.
        use hyp_sym.
        hypersimplify.
        pose (γ₁ := π₂ (π₁ (tm_var ((𝟙 ×h Γ) ×h Γ)))).
        pose (γ₂ := π₂ (tm_var ((𝟙 ×h Γ) ×h Γ))).
        fold γ₁ γ₂.
        use (disj_elim (weaken_left (hyperdoctrine_hyp _) _)).
        + use hyp_ltrans.
          use weaken_right.
          use disj_intro_left.
          use (per_subobject_eq ψ₁).
          * exact γ₁.
          * use weaken_left.
            apply hyperdoctrine_hyp.
          * use weaken_right.
            apply hyperdoctrine_hyp.
        + use hyp_ltrans.
          use weaken_right.
          use disj_intro_right.
          use (per_subobject_eq ψ₂).
          * exact γ₁.
          * use weaken_left.
            apply hyperdoctrine_hyp.
          * use weaken_right.
            apply hyperdoctrine_hyp.
    Qed.

    Definition per_subobject_disj
      : per_subobject Γ.
    Proof.
      use make_per_subobject.
      - exact (ψ₁ ∨ ψ₂).
      - exact per_subobject_disj_laws.
    Defined.

    Proposition per_subobject_disj_intro_left
      : per_subobject_mor_law
          (id_partial_setoid_morphism Γ)
          ψ₁
          per_subobject_disj.
    Proof.
      do 2 use forall_intro.
      use impl_intro.
      use weaken_right.
      use impl_intro.
      cbn.
      hypersimplify.
      pose (γ₁ := π₂ (π₁ (tm_var ((𝟙 ×h Γ) ×h Γ)))).
      pose (γ₂ := π₂ (tm_var ((𝟙 ×h Γ) ×h Γ))).
      fold γ₁ γ₂.
      use disj_intro_left.
      use per_subobject_eq.
      - exact γ₁.
      - use weaken_left.
        apply hyperdoctrine_hyp.
      - use weaken_right.
        apply hyperdoctrine_hyp.
    Qed.

    Proposition per_subobject_disj_intro_right
      : per_subobject_mor_law
          (id_partial_setoid_morphism Γ)
          ψ₂
          per_subobject_disj.
    Proof.
      do 2 use forall_intro.
      use impl_intro.
      use weaken_right.
      use impl_intro.
      cbn.
      hypersimplify.
      pose (γ₁ := π₂ (π₁ (tm_var ((𝟙 ×h Γ) ×h Γ)))).
      pose (γ₂ := π₂ (tm_var ((𝟙 ×h Γ) ×h Γ))).
      fold γ₁ γ₂.
      use disj_intro_right.
      use per_subobject_eq.
      - exact γ₁.
      - use weaken_left.
        apply hyperdoctrine_hyp.
      - use weaken_right.
        apply hyperdoctrine_hyp.
    Qed.

    Context {χ : per_subobject Γ}
            (p : per_subobject_mor_law (id_partial_setoid_morphism Γ) ψ₁ χ)
            (q : per_subobject_mor_law (id_partial_setoid_morphism Γ) ψ₂ χ).

    Proposition per_subobject_disj_elim
      : per_subobject_mor_law
          (id_partial_setoid_morphism Γ)
          per_subobject_disj
          χ.
    Proof.
      do 2 use forall_intro.
      use impl_intro.
      use weaken_right.
      use impl_intro.
      cbn.
      hypersimplify.
      pose (γ₁ := π₂ (π₁ (tm_var ((𝟙 ×h Γ) ×h Γ)))).
      pose (γ₂ := π₂ (tm_var ((𝟙 ×h Γ) ×h Γ))).
      fold γ₁ γ₂.
      use hyp_sym.
      use (disj_elim (weaken_left (hyperdoctrine_hyp _) _)).
      - use hyp_ltrans.
        use weaken_right.
        use (per_subobject_mor p).
        + exact γ₁.
        + cbn.
          hypersimplify.
          use weaken_left.
          apply hyperdoctrine_hyp.
        + use weaken_right.
          apply hyperdoctrine_hyp.
      - use hyp_ltrans.
        use weaken_right.
        use (per_subobject_mor q).
        + exact γ₁.
        + cbn.
          hypersimplify.
          use weaken_left.
          apply hyperdoctrine_hyp.
        + use weaken_right.
          apply hyperdoctrine_hyp.
    Qed.
  End Disjunction.

  Proposition per_subobject_disj_subst
              {Γ₁ Γ₂ : partial_setoid H}
              (s : partial_setoid_morphism Γ₁ Γ₂)
              (ψ₁ ψ₂ : per_subobject Γ₂)
    : per_subobject_mor_law
        (id_partial_setoid_morphism Γ₁)
        (per_subobject_subst s (per_subobject_disj ψ₁ ψ₂))
        (per_subobject_disj (per_subobject_subst s ψ₁) (per_subobject_subst s ψ₂)).
  Proof.
    do 2 use forall_intro.
    use impl_intro.
    use weaken_right.
    use impl_intro.
    cbn.
    rewrite partial_setoid_subst.
    rewrite !exists_subst.
    use hyp_sym.
    use (exists_elim (weaken_left (hyperdoctrine_hyp _) _)).
    rewrite !conj_subst.
    use hyp_ltrans.
    use weaken_right.
    hypersimplify_form.
    hypersimplify.
    pose (γ₁ := π₂ (π₁ (π₁ (tm_var (((𝟙 ×h Γ₁) ×h Γ₁) ×h Γ₂))))).
    pose (γ₁' := π₂ (π₁ (tm_var (((𝟙 ×h Γ₁) ×h Γ₁) ×h Γ₂)))).
    pose (γ₂ := π₂ (tm_var (((𝟙 ×h Γ₁) ×h Γ₁) ×h Γ₂))).
    fold γ₁ γ₁' γ₂.
    use hyp_rtrans.
    use hyp_sym.
    use (disj_elim (weaken_left (hyperdoctrine_hyp _) _)).
    - use hyp_ltrans.
      use weaken_right.
      use disj_intro_left.
      use exists_intro.
      + exact γ₂.
      + hypersimplify.
        fold γ₁'.
        use conj_intro.
        * use weaken_left.
          use (partial_setoid_mor_eq_defined s).
          ** exact γ₁.
          ** exact γ₂.
          ** use weaken_left.
             apply hyperdoctrine_hyp.
          ** use weaken_right.
             exact (partial_setoid_mor_cod_defined s _ _ (hyperdoctrine_hyp _)).
          ** use weaken_right.
             apply hyperdoctrine_hyp.
        * use weaken_right.
          apply hyperdoctrine_hyp.
    - use hyp_ltrans.
      use weaken_right.
      use disj_intro_right.
      use exists_intro.
      + exact γ₂.
      + hypersimplify.
        fold γ₁'.
        use conj_intro.
        * use weaken_left.
          use (partial_setoid_mor_eq_defined s).
          ** exact γ₁.
          ** exact γ₂.
          ** use weaken_left.
             apply hyperdoctrine_hyp.
          ** use weaken_right.
             exact (partial_setoid_mor_cod_defined s _ _ (hyperdoctrine_hyp _)).
          ** use weaken_right.
             apply hyperdoctrine_hyp.
        * use weaken_right.
          apply hyperdoctrine_hyp.
  Qed.

  Definition fiberwise_bincoproducts_per_subobject
    : fiberwise_bincoproducts (disp_cat_per_subobject_cleaving H).
  Proof.
    use make_fiberwise_bincoproducts_locally_propositional.
    - apply locally_prop_disp_cat_per_subobject.
    - intros Γ ψ₁ ψ₂.
      exact (per_subobject_disj ψ₁ ψ₂).
    - intros Γ ψ₁ ψ₂.
      exact (per_subobject_disj_intro_left ψ₁ ψ₂).
    - intros Γ ψ₁ ψ₂.
      exact (per_subobject_disj_intro_right ψ₁ ψ₂).
    - intros Γ ψ₁ ψ₂ χ p q.
      exact (per_subobject_disj_elim ψ₁ ψ₂ p q).
    - intros Γ₁ Γ₂ s ψ₁ ψ₂.
      exact (per_subobject_disj_subst s ψ₁ ψ₂).
  Defined.
End Disjunction.