Require Export Products1.
Require Export Equalizers1.
Require Export Single.

Set Implicit Arguments.
Unset Strict Implicit.

Section ssc1.

Variable D : Category.

Structure Cond1 (I : Type) (k : I → D) (d : D) : Type :=
  {Cond1_i : I; Cond1_f : k Cond1_i --> d}.

Structure SSC1 : Type :=
  {SSC1_I : Type;
   SSC1_k : SSC1_I → D;
   SSC1_p : ∀ d : D, Cond1 SSC1_k d}.

Definition SSC1_i (s : SSC1) (d : D) := Cond1_i (SSC1_p s d).

Definition SSC1_f (s : SSC1) (d : D) := Cond1_f (SSC1_p s d).

End ssc1.


Section thi1.

Variables (D : Category) (D_initial : Initial D).

Definition Thi1_d1 := Initial_ob D_initial.


Definition Thi1_I := UnitType.

Definition Thi1_k (i : Thi1_I) := match i with
                                  | Elt ⇒ Thi1_d1
                                  end.


Definition Thi1_verif_Cond1 (d : D) :=
  Build_Cond1 (k:=Thi1_k) (Cond1_i:=Elt) (MorI D_initial d).

Canonical Structure Thi1_SSC1 := Build_SSC1 Thi1_verif_Cond1.

End thi1.


Section thi2.

Variables (D : Category) (D_complete : Complete D) (SSC1_D : SSC1 D).


Definition Thi2_D_prod : Product1 (SSC1_k (s:=SSC1_D)) :=
  D_complete (FunDiscr (SSC1_k (s:=SSC1_D))).

Definition Thi2_w := Pi1 Thi2_D_prod.


Definition Thi2_D_E_hom :=
  Build_Equalizer2 (D_complete (F_hom Thi2_w Thi2_w)) (Id Thi2_w).

Definition Thi2_v := E1_ob Thi2_D_E_hom.

Definition Thi2_e := E1_mor Thi2_D_E_hom.


 Section thi2_mor_d_def.

 Variable d : D.

 Definition Thi2_p_i := Proj1 Thi2_D_prod (SSC1_i SSC1_D d).

 Definition Thi2_f_d := SSC1_f SSC1_D d.

 Definition Thi2_mor_d := (Thi2_e o Thi2_p_i) o Thi2_f_d.

 End thi2_mor_d_def.


 Section unique_mor_d.

 Variables (d : D) (f g : Thi2_v --> d).


 Definition Thi2_D_E_fg := Build_Equalizer2 (D_complete (F_fg f g)) Elt1.

 Definition Thi2_c := E1_ob Thi2_D_E_fg.

 Definition Thi2_e1 := E1_mor Thi2_D_E_fg.


 Definition Thi2_p_j := Proj1 Thi2_D_prod (SSC1_i SSC1_D Thi2_c).

 Definition Thi2_f_c := SSC1_f SSC1_D Thi2_c.

 Definition Thi2_s := Thi2_p_j o Thi2_f_c.



 Lemma Thi2_e1_RightInv : RIso_law Thi2_e1 (Thi2_e o Thi2_s).
 Proof.
 unfold RIso_law in |- *; simpl in |- ×.
apply Trans with (Thi2_e o Thi2_s o Thi2_e1).
 apply Ass1.
 apply (E_monic (f:=Thi2_D_E_hom)).
 simpl in |- ×.
apply Trans with (Thi2_e o (Thi2_s o Thi2_e1) o Thi2_e).
 apply Ass1.
apply Trans with (Thi2_e o Id Thi2_w).
 apply (Prf_E1_law1 Thi2_D_E_hom ((Thi2_s o Thi2_e1) o Thi2_e) (Id Thi2_w)).
apply Trans with Thi2_e.
 apply Idr1.
 apply Idl1.
 Qed.


 Lemma Eq_fg : f =_S g.
 Proof.
 generalize (Equalizer_iso (f:=Thi2_D_E_fg) Thi2_e1_RightInv).
 intro H; elim H.
 intros H2 H3.
apply
        Trans
         with
           ((E_diese Thi2_D_E_fg
               (Epic_Equalizer_id (f:=Thi2_D_E_fg) Thi2_e1_RightInv)
             o Thi2_e1) o f).
apply Trans with (Id Thi2_v o f).
 apply Idl1.
 apply Comp_r.
 apply Sym; apply H2.
apply
        Trans
         with
           ((E_diese Thi2_D_E_fg
               (Epic_Equalizer_id (f:=Thi2_D_E_fg) Thi2_e1_RightInv)
             o Thi2_e1) o g).
apply
        Trans
         with
           (E_diese Thi2_D_E_fg
              (Epic_Equalizer_id (f:=Thi2_D_E_fg) Thi2_e1_RightInv)
            o Thi2_e1 o f).
 apply Ass1.
apply
        Trans
         with
           (E_diese Thi2_D_E_fg
              (Epic_Equalizer_id (f:=Thi2_D_E_fg) Thi2_e1_RightInv)
            o Thi2_e1 o g).
 apply Comp_l.
 apply (Prf_E1_law1 Thi2_D_E_fg Elt1 Elt2).
 apply Ass.
apply Trans with (Id Thi2_v o g).
 apply Comp_r; apply H2.
 apply Idl.
 Qed.

End unique_mor_d.

Lemma Thi2_isInitial : IsInitial Thi2_mor_d.
Proof.
red in |- *; intros b f.
apply Eq_fg.
Defined.

Definition Thi2_initial : Initial D := Thi2_isInitial.

End thi2.