Library UniMath.CategoryTheory.SubobjectClassifier.Operations

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).

1. Falsity

  Section Falsity.
    Context (I : strict_initial_object E).

    Definition Monic_from_strict_initial
               (x : E)
      : Monic E I x.
    Show 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)))).

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

2. Conjunction

  Section Conjunction.
    Context (BP : BinProducts E).

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

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

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

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

3. Disjunction

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

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

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

4. Implication

  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 Ω Ω --> Ω.
    Show proof.
      use (characteristic_morphism Ω).
      - exact subobject_classifier_impl_ob.
      - apply EqualizerArrowMonic.
  End Implication.
End Operations.