Require Export Setoid_dup2.

Set Implicit Arguments.
Unset Strict Implicit.


Section composition_to_operator''.

Variables (A : Type) (H : A → A → Setoid'')
  (Cfun : ∀ a b c : A, H a b → H b c → H a c).

Definition Congl_law'' :=
  ∀ (a b c : A) (f g : H b c) (h : H a b),
  f =_S'' g → Cfun h f =_S'' Cfun h g.

Definition Congr_law'' :=
  ∀ (a b c : A) (f g : H a b) (h : H b c),
  f =_S'' g → Cfun f h =_S'' Cfun g h.

Definition Cong_law'' :=
  ∀ (a b c : A) (f f' : H a b) (g g' : H b c),
  f =_S'' f' → g =_S'' g' → Cfun f g =_S'' Cfun f' g'.

Hypothesis pcgl : Congl_law''.
Hypothesis pcgr : Congr_law''.

Variable a b c : A.

Definition Build_Comp'' :=
  Build_Map2'' (pcgl (a:=a) (b:=b) (c:=c)) (pcgr (a:=a) (b:=b) (c:=c)).

End composition_to_operator''.


Section cat''.

Variables (Ob'' : Type) (Hom'' : Ob'' → Ob'' → Setoid'').

Variable
  Op_comp'' : ∀ a b c : Ob'', Map2'' (Hom'' a b) (Hom'' b c) (Hom'' a c).

Definition Cat_comp'' (a b c : Ob'') (f : Hom'' a b)
  (g : Hom'' b c) := Op_comp'' a b c f g.

Definition Assoc_law'' :=
  ∀ (a b c d : Ob'') (f : Hom'' a b) (g : Hom'' b c) (h : Hom'' c d),
  Cat_comp'' f (Cat_comp'' g h) =_S'' Cat_comp'' (Cat_comp'' f g) h.

Variable Id'' : ∀ a : Ob'', Hom'' a a.

Definition Idl_law'' :=
  ∀ (a b : Ob'') (f : Hom'' a b), Cat_comp'' (Id'' _) f =_S'' f.

Definition Idr_law'' :=
  ∀ (a b : Ob'') (f : Hom'' b a), f =_S'' Cat_comp'' f (Id'' _).

End cat''.

Structure Category'' : Type :=
  {Ob'' :> Type;
   Hom'' : Ob'' → Ob'' → Setoid'';
   Op_comp'' :
    ∀ a b c : Ob'', Map2'' (Hom'' a b) (Hom'' b c) (Hom'' a c);
   Id'' : ∀ a : Ob'', Hom'' a a;
   Prf_ass'' : Assoc_law'' Op_comp'';
   Prf_idl'' : Idl_law'' Op_comp'' Id'';
   Prf_idr'' : Idr_law'' Op_comp'' Id''}.

Definition Comp'' (C : Category'') := Cat_comp'' (Op_comp'' (c:=C)).

Infix "o''" := Comp'' (at level 20, right associativity).