Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.

Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.Limits.Initial.
Require Import UniMath.CategoryTheory.Limits.StrictInitial.
Require Import UniMath.CategoryTheory.Limits.Terminal.
Require Import UniMath.CategoryTheory.Limits.BinProducts.
Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
Require Import UniMath.CategoryTheory.Limits.Pullbacks.
Require Import UniMath.CategoryTheory.Limits.Equalizers.
Require Import UniMath.CategoryTheory.Monics.
Require Import UniMath.CategoryTheory.SubobjectClassifier.SubobjectClassifier.
Require Import UniMath.CategoryTheory.RegularAndExact.RegularCategory.

Local Open Scope cat.

Section Operations.
  Context {E : category}
          {T : Terminal E}
          (Ω : subobject_classifier T).

  Section Falsity.
    Context (I : strict_initial_object E).

    Definition Monic_from_strict_initial
               (x : E)
      : Monic E I x.
    Proof.
      use make_Monic.
      - exact (InitialArrow I x).
      - abstract
          (intros w f g p ;
           apply (@InitialArrowEq
                    _
                    (make_Initial _ (is_initial_mor_to_strict_initial I _ f)))).
    Defined.

    Definition subobject_classifier_false
      : T --> Ω.
    Proof.
      use (characteristic_morphism Ω).
      - exact I.
      - exact (Monic_from_strict_initial T).
    Defined.
  End Falsity.

  Section Conjunction.
    Context (BP : BinProducts E).

    Let φ : BP T T --> BP Ω Ω := BinProductOfArrows _ _ _ (true Ω) (true Ω).

    Lemma isMonic_subobject_classifier_conj_mor
      : isMonic φ.
    Proof.
      intros x f g p.
      use BinProductArrowsEq.
      - apply TerminalArrowEq.
      - apply TerminalArrowEq.
    Qed.

    Definition subobject_classifier_conj_monic
      : Monic E (BP T T) (BP Ω Ω).
    Proof.
      use make_Monic.
      - exact φ.
      - exact isMonic_subobject_classifier_conj_mor.
    Defined.

    Definition subobject_classifier_conj
      : BP Ω Ω --> Ω.
    Proof.
      use (characteristic_morphism Ω).
      - exact (BP T T).
      - exact subobject_classifier_conj_monic.
    Defined.
  End Conjunction.

  Section Disjunction.
    Context (HC : is_regular_category E)
            (BP : BinProducts E)
            (BC : BinCoproducts E).

    Definition subobject_classifier_disj_mor
      : BC Ω Ω --> BP Ω Ω.
    Proof.
      use BinCoproductArrow.
      - use BinProductArrow.
        + apply identity.
        + exact (const_true Ω Ω).
      - use BinProductArrow.
        + exact (const_true Ω Ω).
        + apply identity.
    Defined.

    Definition subobject_classifier_disj
      : BP Ω Ω --> Ω.
    Proof.
      refine (characteristic_morphism Ω _).
      exact (regular_category_im_Monic HC subobject_classifier_disj_mor).
    Defined.
  End Disjunction.

  Section Implication.
    Context (BP : BinProducts E)
            (EE : Equalizers E).

    Definition subobject_classifier_impl_ob
      : Equalizer _ _
      := EE (BP Ω Ω) Ω (subobject_classifier_conj BP) (BinProductPr1 E (BP Ω Ω)).

    Definition subobject_classifier_impl
      : BP Ω Ω --> Ω.
    Proof.
      use (characteristic_morphism Ω).
      - exact subobject_classifier_impl_ob.
      - apply EqualizerArrowMonic.
    Defined.
  End Implication.
End Operations.