(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


(*****************************************************************************)
(*          Projet Formel - Calculus of Inductive Constructions V5.10        *)
(*****************************************************************************)
(*									     *)
(*	                Adjunction Example : Cartesian         		     *)
(*									     *)
(*****************************************************************************)
(*									     *)
(*                     A. SAIBI	  May 95                  		     *)
(*									     *)
(*****************************************************************************)

Require Export Diagonal.
Require Export CCC.
Require Export Terminal1.

Set Implicit Arguments.
Unset Strict Implicit.

(* Diag(C) a un RAdj -> C admet les produits *)

Section diag_hasprod1.

Variable C : Category.

SubClass HasBinProd1 := RightAdj (Diag C).

Structure IsCartesian1 : Type := 
  {Car_terminal1 :> Terminal1 C; Car_BP1 :> HasBinProd1}.

Variable H : HasBinProd1.

 Section diag_prod1.

 Variable a b : C.

 Let ua' := CoUnit H (Build_POb a b).

 Definition Obj_prod1 := CoUA_ob ua'.

 Definition Proj1_prod1 := Hom_l (CoUA_mor ua').

 Definition Proj2_prod1 := Hom_r (CoUA_mor ua').

  Section together1_def.

  Variable c : C.

  Definition Together1 (f : c --> a) (g : c --> b) :=
    CoUA_diese ua' (Build_Pmor (u:=Build_POb c c) (t:=Build_POb a b) f g).

  Lemma Together1_l : Map2_congl_law Together1.
  Proof.
(* Goal: @Map2_congl_law (@Hom C c a) (@Hom C c b) (@Hom C c (@CoUA_ob C (PROD C C) (@Build_POb C C a b) (Diag C) ua')) Together1 *)
  unfold Map2_congl_law in |- *; intros f g g' H'.
(* Goal: @Equal (@Hom C c (@CoUA_ob C (PROD C C) (@Build_POb C C a b) (Diag C) ua')) (Together1 f g) (Together1 f' g) *)
  unfold Together1 in |- *.
(* Goal: @Equal (@Hom C c (@CoUA_ob C (PROD C C) (@Build_POb C C a b) (Diag C) ua')) (@CoUA_diese C (PROD C C) (@Build_POb C C a b) (Diag C) (@CoUA_ob C (PROD C C) (@Build_POb C C a b) (Diag C) ua') (@CoUA_mor C (PROD C C) (@Build_POb C C a b) (Diag C) ua') (@Prf_IsCoUA C (PROD C C) (@Build_POb C C a b) (Diag C) ua') c (@Build_Pmor C C (@Build_POb C C c c) (@Build_POb C C a b) f g)) (@CoUA_diese C (PROD C C) (@Build_POb C C a b) (Diag C) (@CoUA_ob C (PROD C C) (@Build_POb C C a b) (Diag C) ua') (@CoUA_mor C (PROD C C) (@Build_POb C C a b) (Diag C) ua') (@Prf_IsCoUA C (PROD C C) (@Build_POb C C a b) (Diag C) ua') c (@Build_Pmor C C (@Build_POb C C c c) (@Build_POb C C a b) f' g)) *)
  apply (Codiese_map ua' (a':=c)).
(* Goal: @Equal (@Hom (PROD C C) (@FOb C (PROD C C) (Diag C) c) (@Build_POb C C a b)) (@Build_Pmor C C (@Build_POb C C c c) (@Build_POb C C a b) f g) (@Build_Pmor C C (@Build_POb C C c c) (@Build_POb C C a b) f' g) *)
  simpl in |- *; unfold Equal_Pmor in |- *; simpl in |- *.
(* Goal: and (@Equal (@Hom C c a) f f') (@Equal (@Hom C c b) g g) *)
  split.
(* Goal: @Equal (@Hom C c b) (@Comp C c (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b)) b h (@Hom_r C C (@Diag_ob C (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b))) (@Build_POb C C a b) (@CoUnit_arrow (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b)))) (@Comp C c (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b)) b h Proj2_prod1) *)
  apply Refl.
(* Goal: @Equal (@Hom C c a) f f' *)
(* Goal: @Equal (@Hom C c b) g g *)
  trivial.
  Qed.
 
  Lemma Together1_r : Map2_congr_law Together1.
  Proof.
(* Goal: @Map2_congr_law (@Hom C c a) (@Hom C c b) (@Hom C c (@CoUA_ob C (PROD C C) (@Build_POb C C a b) (Diag C) ua')) Together1 *)
  unfold Map2_congr_law in |- *; intros f f' g H'.
(* Goal: @Equal (@Hom C c (@CoUA_ob C (PROD C C) (@Build_POb C C a b) (Diag C) ua')) (Together1 f g) (Together1 f' g) *)
  unfold Together1 in |- *.
(* Goal: @Equal (@Hom C c (@CoUA_ob C (PROD C C) (@Build_POb C C a b) (Diag C) ua')) (@CoUA_diese C (PROD C C) (@Build_POb C C a b) (Diag C) (@CoUA_ob C (PROD C C) (@Build_POb C C a b) (Diag C) ua') (@CoUA_mor C (PROD C C) (@Build_POb C C a b) (Diag C) ua') (@Prf_IsCoUA C (PROD C C) (@Build_POb C C a b) (Diag C) ua') c (@Build_Pmor C C (@Build_POb C C c c) (@Build_POb C C a b) f g)) (@CoUA_diese C (PROD C C) (@Build_POb C C a b) (Diag C) (@CoUA_ob C (PROD C C) (@Build_POb C C a b) (Diag C) ua') (@CoUA_mor C (PROD C C) (@Build_POb C C a b) (Diag C) ua') (@Prf_IsCoUA C (PROD C C) (@Build_POb C C a b) (Diag C) ua') c (@Build_Pmor C C (@Build_POb C C c c) (@Build_POb C C a b) f' g)) *)
  apply (Codiese_map ua' (a':=c)).
(* Goal: @Equal (@Hom (PROD C C) (@FOb C (PROD C C) (Diag C) c) (@Build_POb C C a b)) (@Build_Pmor C C (@Build_POb C C c c) (@Build_POb C C a b) f g) (@Build_Pmor C C (@Build_POb C C c c) (@Build_POb C C a b) f' g) *)
  simpl in |- *; unfold Equal_Pmor in |- *; simpl in |- *.
(* Goal: and (@Equal (@Hom C c a) f f') (@Equal (@Hom C c b) g g) *)
  split.
(* Goal: @Equal (@Hom C c a) f f' *)
(* Goal: @Equal (@Hom C c b) g g *)
  trivial.
(* Goal: @Equal (@Hom C c b) (@Comp C c (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b)) b h (@Hom_r C C (@Diag_ob C (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b))) (@Build_POb C C a b) (@CoUnit_arrow (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b)))) (@Comp C c (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b)) b h Proj2_prod1) *)
  apply Refl.
  Qed.

  Definition Op_together1 := Build_Map2 Together1_l Together1_r.

  End together1_def.

 Lemma Prf_eq1_prod1 : Eq1_prod_law Proj1_prod1 Op_together1. 
 Proof.
(* Goal: @Eq1_prod_law C (@Ob_l C C (@Build_POb C C a b)) b (@Ob_l C C (@FOb C (PROD C C) (Diag C) (@CoUA_ob C (PROD C C) (@Build_POb C C a b) (Diag C) ua'))) Proj1_prod1 Op_together1 *)
 unfold Eq1_prod_law in |- *; intros c f g.
 unfold Together_prod, Op_together1, Together1, Proj1_prod1, Ap2 in |- *;
  simpl in |- *.
 generalize
  (Prf_isCoUA_law1 ua' (Build_Pmor (u:=Build_POb c c) (t:=Build_POb a b) f g)).
(* Goal: @CoUA_eq C (PROD C C) (@Build_POb C C a b) (Diag C) (@CoUA_ob C (PROD C C) (@Build_POb C C a b) (Diag C) ua') (@CoUA_mor C (PROD C C) (@Build_POb C C a b) (Diag C) ua') c (@Build_Pmor C C (@Build_POb C C c c) (@Build_POb C C a b) (@Comp C c (@Ob_l C C (@FOb C (PROD C C) (Diag C) (@CoUA_ob C (PROD C C) (@Build_POb C C a b) (Diag C) ua'))) (@Ob_l C C (@Build_POb C C a b)) h Proj1_prod1) (@Comp C c (@Ob_l C C (@FOb C (PROD C C) (Diag C) (@CoUA_ob C (PROD C C) (@Build_POb C C a b) (Diag C) ua'))) (@Ob_r C C (@Build_POb C C a b)) h Proj2_prod1)) h *)
 unfold CoUA_eq in |- *; simpl in |- *.
(* Goal: forall _ : @Equal_Pmor C C (@Diag_ob C c) (@Build_POb C C a b) (@Comp (PROD C C) (@Diag_ob C c) (@Diag_ob C (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b))) (@Build_POb C C a b) (@FMor C (PROD C C) (Diag C) c (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b)) (@CoUnit_arrow_diese (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b) c (@Build_Pmor C C (@Build_POb C C c c) (@Build_POb C C a b) f g))) (@CoUnit_arrow (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b))) (@Build_Pmor C C (@Build_POb C C c c) (@Build_POb C C a b) f g), @Equal (@Hom C c b) (@Comp C c (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b)) b (@CoUnit_arrow_diese (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b) c (@Build_Pmor C C (@Build_POb C C c c) (@Build_POb C C a b) f g)) (@Hom_r C C (@Diag_ob C (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b))) (@Build_POb C C a b) (@CoUnit_arrow (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b)))) g *)
 unfold Equal_Pmor in |- *; simpl in |- *.
(* Goal: forall _ : and (@Equal (@Hom C c a) (@Comp C c (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b)) a (@CoUnit_arrow_diese (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b) c (@Build_Pmor C C (@Build_POb C C c c) (@Build_POb C C a b) f g)) (@Hom_l C C (@Diag_ob C (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b))) (@Build_POb C C a b) (@CoUnit_arrow (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b)))) f) (@Equal (@Hom C c b) (@Comp C c (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b)) b (@CoUnit_arrow_diese (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b) c (@Build_Pmor C C (@Build_POb C C c c) (@Build_POb C C a b) f g)) (@Hom_r C C (@Diag_ob C (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b))) (@Build_POb C C a b) (@CoUnit_arrow (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b)))) g), @Equal (@Hom C c b) (@Comp C c (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b)) b (@CoUnit_arrow_diese (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b) c (@Build_Pmor C C (@Build_POb C C c c) (@Build_POb C C a b) f g)) (@Hom_r C C (@Diag_ob C (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b))) (@Build_POb C C a b) (@CoUnit_arrow (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b)))) g *)
 simple induction 1.
(* Goal: forall (_ : @Equal (@Hom C c a) (@Comp C c (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b)) a (@CoUnit_arrow_diese (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b) c (@Build_Pmor C C (@Build_POb C C c c) (@Build_POb C C a b) f g)) (@Hom_l C C (@Diag_ob C (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b))) (@Build_POb C C a b) (@CoUnit_arrow (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b)))) f) (_ : @Equal (@Hom C c b) (@Comp C c (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b)) b (@CoUnit_arrow_diese (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b) c (@Build_Pmor C C (@Build_POb C C c c) (@Build_POb C C a b) f g)) (@Hom_r C C (@Diag_ob C (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b))) (@Build_POb C C a b) (@CoUnit_arrow (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b)))) g), @Equal (@Hom C c b) (@Comp C c (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b)) b (@CoUnit_arrow_diese (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b) c (@Build_Pmor C C (@Build_POb C C c c) (@Build_POb C C a b) f g)) (@Hom_r C C (@Diag_ob C (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b))) (@Build_POb C C a b) (@CoUnit_arrow (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b)))) g *)
 intros H2 H3.
(* Goal: @Equal (@Hom C c a) (@Comp C c (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b)) a (@CoUnit_arrow_diese (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b) c (@Build_Pmor C C (@Build_POb C C c c) (@Build_POb C C a b) f g)) (@Hom_l C C (@Diag_ob C (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b))) (@Build_POb C C a b) (@CoUnit_arrow (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b)))) f *)
 apply H2.
 Qed. 

 Lemma Prf_eq2_prod1 : Eq2_prod_law Proj2_prod1 Op_together1. 
 Proof.
(* Goal: @Eq2_prod_law C a (@Ob_r C C (@Build_POb C C a b)) (@Ob_r C C (@FOb C (PROD C C) (Diag C) (@CoUA_ob C (PROD C C) (@Build_POb C C a b) (Diag C) ua'))) Proj2_prod1 Op_together1 *)
 unfold Eq2_prod_law in |- *; intros c f g.
 unfold Together_prod, Op_together1, Together1, Proj2_prod1, Ap2 in |- *;
  simpl in |- *.
 generalize
  (Prf_isCoUA_law1 ua' (Build_Pmor (u:=Build_POb c c) (t:=Build_POb a b) f g)).
(* Goal: @CoUA_eq C (PROD C C) (@Build_POb C C a b) (Diag C) (@CoUA_ob C (PROD C C) (@Build_POb C C a b) (Diag C) ua') (@CoUA_mor C (PROD C C) (@Build_POb C C a b) (Diag C) ua') c (@Build_Pmor C C (@Build_POb C C c c) (@Build_POb C C a b) (@Comp C c (@Ob_l C C (@FOb C (PROD C C) (Diag C) (@CoUA_ob C (PROD C C) (@Build_POb C C a b) (Diag C) ua'))) (@Ob_l C C (@Build_POb C C a b)) h Proj1_prod1) (@Comp C c (@Ob_l C C (@FOb C (PROD C C) (Diag C) (@CoUA_ob C (PROD C C) (@Build_POb C C a b) (Diag C) ua'))) (@Ob_r C C (@Build_POb C C a b)) h Proj2_prod1)) h *)
 unfold CoUA_eq in |- *; simpl in |- *.
(* Goal: forall _ : @Equal_Pmor C C (@Diag_ob C c) (@Build_POb C C a b) (@Comp (PROD C C) (@Diag_ob C c) (@Diag_ob C (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b))) (@Build_POb C C a b) (@FMor C (PROD C C) (Diag C) c (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b)) (@CoUnit_arrow_diese (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b) c (@Build_Pmor C C (@Build_POb C C c c) (@Build_POb C C a b) f g))) (@CoUnit_arrow (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b))) (@Build_Pmor C C (@Build_POb C C c c) (@Build_POb C C a b) f g), @Equal (@Hom C c b) (@Comp C c (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b)) b (@CoUnit_arrow_diese (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b) c (@Build_Pmor C C (@Build_POb C C c c) (@Build_POb C C a b) f g)) (@Hom_r C C (@Diag_ob C (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b))) (@Build_POb C C a b) (@CoUnit_arrow (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b)))) g *)
 unfold Equal_Pmor in |- *; simpl in |- *.
(* Goal: forall _ : and (@Equal (@Hom C c a) (@Comp C c (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b)) a (@CoUnit_arrow_diese (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b) c (@Build_Pmor C C (@Build_POb C C c c) (@Build_POb C C a b) f g)) (@Hom_l C C (@Diag_ob C (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b))) (@Build_POb C C a b) (@CoUnit_arrow (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b)))) f) (@Equal (@Hom C c b) (@Comp C c (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b)) b (@CoUnit_arrow_diese (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b) c (@Build_Pmor C C (@Build_POb C C c c) (@Build_POb C C a b) f g)) (@Hom_r C C (@Diag_ob C (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b))) (@Build_POb C C a b) (@CoUnit_arrow (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b)))) g), @Equal (@Hom C c b) (@Comp C c (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b)) b (@CoUnit_arrow_diese (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b) c (@Build_Pmor C C (@Build_POb C C c c) (@Build_POb C C a b) f g)) (@Hom_r C C (@Diag_ob C (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b))) (@Build_POb C C a b) (@CoUnit_arrow (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b)))) g *)
 simple induction 1.
(* Goal: forall (_ : @Equal (@Hom C c a) (@Comp C c (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b)) a (@CoUnit_arrow_diese (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b) c (@Build_Pmor C C (@Build_POb C C c c) (@Build_POb C C a b) f g)) (@Hom_l C C (@Diag_ob C (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b))) (@Build_POb C C a b) (@CoUnit_arrow (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b)))) f) (_ : @Equal (@Hom C c b) (@Comp C c (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b)) b (@CoUnit_arrow_diese (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b) c (@Build_Pmor C C (@Build_POb C C c c) (@Build_POb C C a b) f g)) (@Hom_r C C (@Diag_ob C (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b))) (@Build_POb C C a b) (@CoUnit_arrow (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b)))) g), @Equal (@Hom C c b) (@Comp C c (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b)) b (@CoUnit_arrow_diese (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b) c (@Build_Pmor C C (@Build_POb C C c c) (@Build_POb C C a b) f g)) (@Hom_r C C (@Diag_ob C (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b))) (@Build_POb C C a b) (@CoUnit_arrow (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b)))) g *)
 intros H2 H3.
(* Goal: @Equal (@Hom C c b) (@Comp C c (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b)) b (@CoUnit_arrow_diese (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b) c (@Build_Pmor C C (@Build_POb C C c c) (@Build_POb C C a b) f g)) (@Hom_r C C (@Diag_ob C (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b))) (@Build_POb C C a b) (@CoUnit_arrow (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b)))) g *)
 apply H3.
 Qed.

 Lemma Prf_unique_together1 :
  Unique_together_law Proj1_prod1 Proj2_prod1 Op_together1.
 Proof.
(* Goal: @Unique_together_law C (@Ob_l C C (@Build_POb C C a b)) (@Ob_r C C (@Build_POb C C a b)) (@Ob_l C C (@FOb C (PROD C C) (Diag C) (@CoUA_ob C (PROD C C) (@Build_POb C C a b) (Diag C) ua'))) Proj1_prod1 Proj2_prod1 Op_together1 *)
 unfold Unique_together_law in |- *; intros c h.
(* Goal: @Equal (@Hom C c (@CoUA_ob C (PROD C C) (@Build_POb C C a b) (Diag C) ua')) (Together1 f g) (Together1 f' g) *)
 unfold Together_prod, Ap2 in |- *; simpl in |- *; unfold Together1 in |- *.
(* Goal: @Equal (@Hom C c (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b))) (@CoUA_diese C (PROD C C) (@Build_POb C C a b) (Diag C) (@CoUA_ob C (PROD C C) (@Build_POb C C a b) (Diag C) ua') (@CoUA_mor C (PROD C C) (@Build_POb C C a b) (Diag C) ua') (@Prf_IsCoUA C (PROD C C) (@Build_POb C C a b) (Diag C) ua') c (@Build_Pmor C C (@Build_POb C C c c) (@Build_POb C C a b) (@Comp C c (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b)) a h Proj1_prod1) (@Comp C c (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b)) b h Proj2_prod1))) h *)
 apply Sym.
 apply
  (Prf_isCoUA_law2 ua'
     (f:=Build_Pmor (u:=Build_POb c c) (t:=Build_POb a b) 
           (h o Proj1_prod1) (h o Proj2_prod1)) (g:=h)).
(* Goal: @CoUA_eq C (PROD C C) (@Build_POb C C a b) (Diag C) (@CoUA_ob C (PROD C C) (@Build_POb C C a b) (Diag C) ua') (@CoUA_mor C (PROD C C) (@Build_POb C C a b) (Diag C) ua') c (@Build_Pmor C C (@Build_POb C C c c) (@Build_POb C C a b) (@Comp C c (@Ob_l C C (@FOb C (PROD C C) (Diag C) (@CoUA_ob C (PROD C C) (@Build_POb C C a b) (Diag C) ua'))) (@Ob_l C C (@Build_POb C C a b)) h Proj1_prod1) (@Comp C c (@Ob_l C C (@FOb C (PROD C C) (Diag C) (@CoUA_ob C (PROD C C) (@Build_POb C C a b) (Diag C) ua'))) (@Ob_r C C (@Build_POb C C a b)) h Proj2_prod1)) h *)
 unfold CoUA_eq in |- *; simpl in |- *.
(* Goal: and (@Equal (@Hom C c a) f f') (@Equal (@Hom C c b) g g) *)
 unfold Equal_Pmor in |- *; simpl in |- *; split.
(* Goal: @Equal (@Hom C c b) (@Comp C c (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b)) b h (@Hom_r C C (@Diag_ob C (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b))) (@Build_POb C C a b) (@CoUnit_arrow (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b)))) (@Comp C c (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b)) b h Proj2_prod1) *)
 apply Refl.
(* Goal: @Equal (@Hom C c b) (@Comp C c (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b)) b h (@Hom_r C C (@Diag_ob C (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b))) (@Build_POb C C a b) (@CoUnit_arrow (PROD C C) C (Diag C) (@CoAdjoint (PROD C C) C (Diag C) H) (@Adj_r (PROD C C) C (Diag C) H) (@Build_POb C C a b)))) (@Comp C c (@FOb (PROD C C) C (@CoAdjoint (PROD C C) C (Diag C) H) (@Build_POb C C a b)) b h Proj2_prod1) *)
 apply Refl.
 Qed.

 End diag_prod1.

 Definition BP1_to_BP : HasBinProd C :=
   fun a b : C =>
   Build_BinProd (Prf_eq1_prod1 (a:=a) (b:=b)) (Prf_eq2_prod1 (a:=a) (b:=b))
     (Prf_unique_together1 (a:=a) (b:=b)).

End diag_hasprod1.

Coercion BP1_to_BP : HasBinProd1 >-> HasBinProd.

Coercion Car1_to_Car (C : Category) (H : IsCartesian1 C) :=
  Build_IsCartesian H H.

