From Categories Require Import Essentials.Notations.
From Categories Require Import Essentials.Types.
From Categories Require Import Essentials.Facts_Tactics.
From Categories Require Import Category.Main.
From Categories Require Import Basic_Cons.PullBack Basic_Cons.Terminal.

(**
A subobject classifier Î© is the object that classifies subobjects of all
objects.That is, There is a one to one correspondence between sub-objects
of an object a i.e., monomorphisms to a, m : x â‰«â€“> a, and morphisms from
a to Î©. It is formally defined as follows:

Î© together with âŠ¤ : 1 â†’ Î© (1 is the terminal object) is a subobject
classifier if we have for any monomorphism m : a â‰«â€“> b there is a
unique morphism Ï‡â‚˜ : b â†’ Î© such that the following diagram is a pullback:
#
<pre>
                !
        a â€”â€”â€”â€”â€”â€”â€”â€”â€”â€”â€”â€”â€“> 1
        |__|             |
        |                |
     m  |                |âŠ¤
        |                |
        â†“                â†“
        b â€”â€”â€”â€”â€”â€”â€”â€”â€”â€”â€”â€”â€“> Î©
               Ï‡â‚˜  
</pre>
#

Where ! is the unique arrow to the terminal object.
*)
Section SubObject_Classifier.
  Context (C : Category) {term : (ð�Ÿ™_ C)%object}.

  Local Notation "1" := term.
  
  Record SubObject_Classifier : Type :=
    {
      SOC : C;
      SOC_morph : (1 â€“â‰» SOC)%morphism;
      SOC_char {a b : C} (m : (a â‰«â€“> b)%morphism) : (b â€“â‰» SOC)%morphism;
      SO_pulback {a b : C} (m : (a â‰«â€“> b)%morphism) :
        is_PullBack
          (mono_morphism m)
          (t_morph 1 a)
          (SOC_char m)
          SOC_morph;
      SOC_char_unique {a b : C} (m : (a â‰«â€“> b)%morphism)
                      (h h' : (b â€“â‰» SOC)%morphism) :
        is_PullBack
          (mono_morphism m)
          (t_morph 1 a)
          h
          SOC_morph
        â†’
        is_PullBack
          (mono_morphism m)
          (t_morph 1 a)
          h'
          SOC_morph
        â†’
        h = h'
    }.

  
End SubObject_Classifier.
