# Duality between C and C^op

## Contents

• From C^op to C
• Monics and Epis
• Initial, Terminal, and Zero
• Equalizers and Coequalizers
• Kernels and Cokernels
• Pullbacks and Pushouts
• BinProducts and BinCoproducts
• From C to C^op
• Monics and Epis
• Initial, Terminal, and Zero
• Equalizers and Coequalizers
• Kernels and Cokernels
• Pullbacks and Pushouts
• BinProducts and BinCoproducts

# Translation of structures from C^op to C

Section def_opposites.

Variable C : precategory.
Hypothesis hs : has_homsets C.

## Monic and Epi

Definition opp_isMonic {a b : C} (f : a --> b) (H : @isMonic (C^op) _ _ f) : @isEpi C _ _ f := H.
Opaque opp_isMonic.

Definition opp_Monic {a b : C} (f : @Monic (C^op) a b) : @Epi C b a :=
@make_Epi C _ _ f (opp_isMonic f (pr2 f)).

Definition opp_isEpi {a b : C} (f : a --> b) (H : @isEpi (C^op) _ _ f) : @isMonic C _ _ f := H.
Opaque opp_isEpi.

Definition opp_Epi {a b : C} (f : @Epi (C^op) a b) : @Monic C b a :=
@make_Monic C _ _ f (opp_isEpi f (pr2 f)).

## Initial, Terminal, and Zero

Definition opp_isInitial {x : C} (H : @isInitial (C^op) x) : @isTerminal C x := H.

Definition opp_Initial (I : @Initial (C^op)) : @Terminal C :=
@make_Terminal C _ (opp_isInitial (pr2 I)).

Definition opp_isTerminal {x : C} (H : @isTerminal (C^op) x) : @isInitial C x := H.

Definition opp_Terminal (T : @Terminal (C^op)) : @Initial C :=
@make_Initial C _ (opp_isTerminal (pr2 T)).

Lemma opp_isZero {x : C} (H : @isZero (C^op) x) : @isZero C x.
Proof.
use make_isZero.
- intros a. exact (dirprod_pr2 H a).
- intros a. exact (dirprod_pr1 H a).
Qed.

Definition opp_Zero (Z : @Zero (C^op)) : @Zero C := @make_Zero C _ (opp_isZero (pr2 Z)).

## Equality on ZeroArrows

Lemma opp_ZeroArrowTo {x : C} (Z : @Zero (C^op)) :
@ZeroArrowTo (C^op) Z x = @ZeroArrowFrom C (opp_Zero Z) x.
Proof.
apply ArrowsToZero.
Qed.

Lemma opp_ZeroArrowFrom {x : C} (Z : @Zero (C^op)) :
@ZeroArrowFrom (C^op) Z x = @ZeroArrowTo C (opp_Zero Z) x.
Proof.
apply ArrowsFromZero.
Qed.

Lemma opp_ZeroArrow {x y : C} (Z : @Zero (C^op)) :
@ZeroArrow (C^op) Z x y = @ZeroArrow C (opp_Zero Z) y x.
Proof.
unfold ZeroArrow.
rewrite opp_ZeroArrowTo.
rewrite opp_ZeroArrowFrom.
apply idpath.
Qed.

Local Opaque ZeroArrow.

## Equalizers and Coequalizers

Lemma opp_isEqualizer {x y z : C} (f g : (C^op)⟦y, z) (e : (C^op)⟦x, y) (H : e · f = e · g)
(H' : @isEqualizer (C^op) _ _ _ f g e H) : @isCoequalizer C _ _ _ f g e H.
Proof.
exact H'.
Qed.

Lemma opp_isCoequalizer {x y z : C} (f g : (C^op)⟦x, y) (e : (C^op)⟦y, z)
(H : f · e = g · e) (H' : @isCoequalizer (C^op) _ _ _ f g e H) :
@isEqualizer C _ _ _ f g e H.
Proof.
exact H'.
Qed.

Definition opp_Equalizer {y z : C} (f g : (C^op)⟦y, z) (E : @Equalizer (C^op) y z f g) :
@Coequalizer C z y f g := @make_Coequalizer C _ _ _ f g (EqualizerArrow E) (EqualizerEqAr E)
(opp_isEqualizer f g (EqualizerArrow E)
(EqualizerEqAr E)
(isEqualizer_Equalizer E)).

Definition opp_Coequalizer {y z : C} (f g : (C^op)⟦y, z) (E : @Coequalizer (C^op) y z f g) :
@Equalizer C z y f g := @make_Equalizer C _ _ _ f g (CoequalizerArrow E) (CoequalizerEqAr E)
(opp_isCoequalizer f g (CoequalizerArrow E)
(CoequalizerEqAr E)
(isCoequalizer_Coequalizer E)).

Definition opp_Equalizers (E : @Equalizers (C^op)) : @Coequalizers C.
Proof.
intros x y f g.
use opp_Equalizer.
exact (E y x f g).
Defined.

Definition opp_Coequalizers (E : @Coequalizers (C^op)) : @Equalizers C.
Proof.
intros x y f g.
use opp_Coequalizer.
exact (E y x f g).
Defined.

## Kernels and Cokernels

Local Lemma opp_isCokernel_eq {x y z : C^op} (f : (C^op)⟦x, y) (g : C^opy, z) (Z : Zero (C^op))
(H : f · g = ZeroArrow Z _ _) (Z' : Zero C) :
(g : Cz, y) · (f : Cy, x) = ZeroArrow Z' _ _.
Proof.
cbn in ×. rewrite H. rewrite opp_ZeroArrow.
exact (ZerosArrowEq C (opp_Zero Z) Z' z x).
Qed.

Lemma opp_isCokernel {x y z : C^op} {f : (C^op)⟦x, y} {g : C^opy, z} {Z : Zero (C^op)}
{H : f · g = ZeroArrow Z _ _} (K' : isKernel Z f g H) {Z' : Zero C} :
isCokernel Z' (g : Cz, y) (f : Cy, x) (opp_isCokernel_eq f g Z H Z').
Proof.
set (K := make_Kernel _ _ _ _ K').
use make_isCokernel.
- exact hs.
- intros w h H'.
rewrite <- (ZerosArrowEq C (opp_Zero Z) Z' z w) in H'.
rewrite <- opp_ZeroArrow in H'.
use unique_exists.
+ exact (KernelIn Z K w h H').
+ use (KernelCommutes Z K).
+ intros y0. apply hs.
+ cbn. intros y0 X. use (KernelInsEq Z K). rewrite (KernelCommutes Z K). cbn. rewrite X.
apply idpath.
Qed.

Local Lemma opp_Kernel_eq {y z : C} (f : (C^op)⟦y, z) (Z : Zero (C^op))
(K : @Kernel (C^op) Z y z f) :
@compose C^op _ _ _ (KernelArrow K) f = ZeroArrow (opp_Zero Z) z K.
Proof.
cbn. rewrite <- opp_ZeroArrow. apply (KernelCompZero Z K).
Qed.

Lemma opp_Kernel_isCokernel {y z : C} (f : (C^op)⟦y, z) (Z : Zero (C^op))
(K : @Kernel (C^op) Z y z f) :
isCokernel (opp_Zero Z) f (KernelArrow K) (opp_Kernel_eq f Z K).
Proof.
use make_isCokernel.
- exact hs.
- intros w h H'. rewrite <- opp_ZeroArrow in H'.
use unique_exists.
+ exact (KernelIn Z K w h H').
+ use (KernelCommutes Z K).
+ intros y0. apply hs.
+ cbn. intros y0 X. use (@KernelInsEq C^op). rewrite (KernelCommutes Z K). cbn. rewrite X.
apply idpath.
Qed.

Definition opp_Kernel {y z : C} (f : (C^op)⟦y, z) (Z : Zero (C^op))
(K : @Kernel (C^op) Z y z f) : @Cokernel C (opp_Zero Z) z y f.
Proof.
use make_Cokernel.
- exact K.
- exact (KernelArrow K).
- exact (opp_Kernel_eq f Z K).
- exact (opp_Kernel_isCokernel f Z K).
Defined.

Lemma opp_isKernel {x y z : C^op} {f : (C^op)⟦x, y} {g : C^opy, z} {Z : Zero (C^op)}
{H : f · g = ZeroArrow Z _ _} (CK' : isCokernel Z f g H) {Z' : Zero C} :
isKernel Z' (g : Cz, y) (f : Cy, x) (opp_isCokernel_eq f g Z H Z').
Proof.
set (CK := make_Cokernel _ _ _ _ CK').
use make_isKernel.
- exact hs.
- intros w h H'.
rewrite <- (ZerosArrowEq C (opp_Zero Z) Z' w x) in H'.
rewrite <- opp_ZeroArrow in H'.
use unique_exists.
+ exact (CokernelOut Z CK w h H').
+ use (CokernelCommutes Z CK).
+ intros y0. apply hs.
+ cbn. intros y0 X. use (CokernelOutsEq _ CK). rewrite (CokernelCommutes Z CK). cbn. rewrite X.
apply idpath.
Qed.

Local Lemma opp_Cokernel_eq {y z : C} (f : (C^op)⟦y, z) (Z : Zero (C^op))
(CK : @Cokernel (C^op) Z y z f) :
@compose (C^op) _ _ _ f (CokernelArrow CK) = ZeroArrow (opp_Zero Z) CK y.
Proof.
cbn. rewrite <- opp_ZeroArrow. apply (CokernelCompZero Z CK).
Qed.

Lemma opp_Cokernel_isKernel {y z : C} (f : (C^op)⟦y, z) (Z : Zero (C^op))
(CK : @Cokernel (C^op) Z y z f) :
isKernel (opp_Zero Z) (CokernelArrow CK) f (opp_Cokernel_eq f Z CK).
Proof.
use make_isKernel.
- exact hs.
- intros w h H'. rewrite <- opp_ZeroArrow in H'.
use unique_exists.
+ exact (CokernelOut Z CK w h H').
+ use (CokernelCommutes Z CK).
+ intros y0. apply hs.
+ cbn. intros y0 X. use (@CokernelOutsEq C^op). rewrite (CokernelCommutes Z CK). cbn. rewrite X.
apply idpath.
Qed.

Definition opp_Cokernel {y z : C} (f : (C^op)⟦y, z) (Z : Zero (C^op))
(CK : @Cokernel (C^op) Z y z f) : @Kernel C (opp_Zero Z) z y f.
Proof.
use make_Kernel.
- exact CK.
- exact (CokernelArrow CK).
- exact (opp_Cokernel_eq f Z CK).
- exact (opp_Cokernel_isKernel f Z CK).
Defined.

Definition opp_Kernels (Z : Zero (C^op)) (K : @Kernels (C^op) Z) : @Cokernels C (opp_Zero Z).
Proof.
intros x y f.
use opp_Kernel.
apply (K y x f).
Defined.

Definition opp_Cokernels (Z : Zero (C^op)) (CK : @Cokernels (C^op) Z) : @Kernels C (opp_Zero Z).
Proof.
intros x y f.
use opp_Cokernel.
apply (CK y x f).
Defined.

## Pushouts and pullbacks

Lemma opp_isPushout {a b c d : C} (f : (C^op)⟦a, b) (g : (C^op)⟦a, c)
(in1 : (C^op)⟦b, d) (in2 : (C^op)⟦c, d) (H : f · in1 = g · in2)
(iPo : @isPushout (C^op) a b c d f g in1 in2 H) : @isPullback C a b c d f g in1 in2 H.
Proof.
exact iPo.
Qed.

Lemma opp_isPullback {a b c d : C} (f : (C^op)⟦b, a) (g : (C^op)⟦c, a)
(p1 : (C^op)⟦d, b) (p2 : (C^op)⟦d, c) (H : p1 · f = p2 · g)
(iPb : @isPullback (C^op) a b c d f g p1 p2 H) : @isPushout C a b c d f g p1 p2 H.
Proof.
exact iPb.
Qed.

Definition opp_Pushout {a b c : C} (f : (C^op)⟦a, b) (g : (C^op)⟦a, c)
(Po : @Pushout (C^op) a b c f g) : @Pullback C a b c f g.
Proof.
exact Po.
Defined.

Definition opp_Pullback {a b c : C} (f : (C^op)⟦b, a) (g : (C^op)⟦c, a)
(Pb : @Pullback (C^op) a b c f g) : @Pushout C a b c f g.
Proof.
exact Pb.
Defined.

Definition opp_Pushouts (Pos : @Pushouts (C^op)) : @Pullbacks C.
Proof.
exact Pos.
Defined.

Definition opp_Pullbacks (Pbs : @Pushouts (C^op)) : @Pullbacks C.
Proof.
exact Pbs.
Defined.

## BinProducts and BinCoproducts

Definition opp_isBinProduct (c d p : C) (p1 : (C^op)⟦p, c) (p2 : (C^op)⟦p, d)
(iBPC : @isBinProduct (C^op) c d p p1 p2) : @isBinCoproduct C c d p p1 p2 :=
iBPC.

Definition opp_isBinCoproduct (a b co : C) (ia : (C^op)⟦a, co) (ib : (C^op)⟦b, co)
(iBCC : @isBinCoproduct (C^op) a b co ia ib) :
@isBinProduct C a b co ia ib := iBCC.

Definition opp_BinProduct (c d : C) (BPC : @BinProduct (C^op) c d) :
@BinCoproduct C c d := BPC.

Definition opp_BinCoproduct (c d : C) (BCC : @BinCoproduct (C^op) c d) :
@BinProduct C c d := BCC.

Definition opp_BinProducts (BP : @BinProducts (C^op)) : @BinCoproducts C := BP.

Definition opp_BinCoproducts (BC : @BinCoproducts (C^op)) : @BinProducts C := BC.

End def_opposites.

# Translation of structures from C to C^op

Section def_opposites'.

Variable C : precategory.
Hypothesis hs : has_homsets C.

## Monic and Epi

Definition isMonic_opp {a b : C} {f : Ca, b} (H : @isMonic C a b f) : @isEpi (C^op) b a f := H.
Opaque isMonic_opp.

Definition Monic_opp {a b : C} (f : @Monic C a b) : @Epi (C^op) b a :=
@make_Epi (C^op) b a f (isMonic_opp (pr2 f)).

Definition isEpi_opp {a b : C} {f : Ca, b} (H : @isEpi C a b f) : @isMonic (C^op) b a f := H.
Opaque isEpi_opp.

Definition Epi_opp {a b : C} (f : @Epi C a b) : @Monic (C^op) b a :=
@make_Monic (C^op) b a f (isEpi_opp (pr2 f)).

## Initial, Terminal, and Zero

Definition isInitial_opp {x : C} (H : @isInitial C x) : @isTerminal (C^op) x := H.

Definition Initial_opp (I : @Initial C) : @Terminal (C^op) :=
@make_Terminal (C^op) _ (isInitial_opp (pr2 I)).

Definition isTerminal_opp {x : C} (H : @isTerminal C x) : @isInitial (C^op) x := H.

Definition Terminal_opp (T : @Terminal C) : @Initial (C^op) :=
@make_Initial (C^op) _ (isTerminal_opp (pr2 T)).

Lemma isZero_opp {x : C} (H : @isZero C x) : @isZero (C^op) x.
Proof.
use make_isZero.
- intros a. apply (pr2 H a).
- intros a. apply (pr1 H a).
Defined.

Definition Zero_opp (T : @Zero C) : @Zero (C^op) := @make_Zero (C^op) _ (isZero_opp (pr2 T)).

## Equality on ZeroArrows

Lemma ZeroArrowTo_opp {x : C} (Z : @Zero C) :
@ZeroArrowTo C Z x = @ZeroArrowFrom (C^op) (Zero_opp Z) x.
Proof.
apply ArrowsToZero.
Qed.

Lemma ZeroArrowFrom_opp {x : C} (Z : @Zero C) :
@ZeroArrowFrom C Z x = @ZeroArrowTo (C^op) (Zero_opp Z) x.
Proof.
apply ArrowsFromZero.
Qed.

Lemma ZeroArrow_opp {x y : C} (Z : @Zero C) :
@ZeroArrow C Z x y = @ZeroArrow (C^op) (Zero_opp Z) y x.
Proof.
unfold ZeroArrow.
rewrite ZeroArrowTo_opp.
rewrite ZeroArrowFrom_opp.
apply idpath.
Qed.

Local Opaque ZeroArrow.

## Equalizers and Coequalizers

Definition isEqualizer_opp {x y z : C} (f g : Cy, z) (e : Cx, y) (H : e · f = e · g)
(isE : @isEqualizer C _ _ _ f g e H) : @isCoequalizer (C^op) _ _ _ f g e H := isE.

Definition isCoequalizer_opp {x y z : C} (f g : Cx, y) (e : Cy, z) (H : f · e = g · e)
(isC : @isCoequalizer C _ _ _ f g e H) : @isEqualizer (C^op) _ _ _ f g e H := isC.

Definition Equalizer_opp {y z : C} (f g : Cy, z) (E : @Equalizer C y z f g) :
@Coequalizer (C^op) z y f g := @make_Coequalizer (C^op) _ _ _ f g (EqualizerArrow E)
(EqualizerEqAr E)
(isEqualizer_opp f g (EqualizerArrow E)
(EqualizerEqAr E)
(isEqualizer_Equalizer E)).

Definition Coequalizer_opp {y z : C} (f g : Cy, z) (CE : @Coequalizer C y z f g) :
@Equalizer (C^op) z y f g := @make_Equalizer (C^op) _ _ _ f g (CoequalizerArrow CE)
(CoequalizerEqAr CE)
(isCoequalizer_opp f g (CoequalizerArrow CE)
(CoequalizerEqAr CE)
(isCoequalizer_Coequalizer CE)).

Definition Equalizers_opp (E : @Equalizers C) : @Coequalizers (C^op).
Proof.
intros x y f g.
use Equalizer_opp.
exact (E y x f g).
Defined.

Definition Coequalizers_opp (CE : @Coequalizers C) : @Equalizers (C^op).
Proof.
intros x y f g.
use Coequalizer_opp.
exact (CE y x f g).
Defined.

## Kernels and Cokernels

Local Lemma isCokernel_opp_eq {x y z : C} (f : Cx, y) (g : Cy, z) (Z : Zero C)
(H : f · g = ZeroArrow Z _ _) (Z' : Zero C^op) :
(g : C^opz, y) · (f : C^opy, x) = ZeroArrow Z' _ _.
Proof.
cbn in ×. rewrite H. rewrite ZeroArrow_opp.
exact (ZerosArrowEq C^op (Zero_opp Z) Z' z x).
Qed.

Lemma isCokernel_opp {x y z : C} {f : Cx, y} {g : Cy, z} {Z : Zero C}
{H : f · g = ZeroArrow Z _ _} (K' : isKernel Z f g H) {Z' : Zero C^op} :
isCokernel Z' (g : C^opz, y) (f : C^opy, x) (isCokernel_opp_eq f g Z H Z').
Proof.
set (K := make_Kernel _ _ _ _ K').
use make_isCokernel.
- exact (has_homsets_opp hs).
- intros w h H'. cbn in H'. rewrite <- (ZerosArrowEq C^op (Zero_opp Z) Z' z w) in H'.
use unique_exists.
+ rewrite <- ZeroArrow_opp in H'. exact (KernelIn Z K w h H').
+ cbn. use (KernelCommutes Z K).
+ intros y0. apply (has_homsets_opp hs).
+ cbn. intros y0 X. use (KernelInsEq Z K). rewrite KernelCommutes. exact X.
Qed.

Local Lemma Kernel_opp_eq {y z : C} (f : Cy, z) (Z : Zero C) (K : @Kernel C Z y z f) :
@compose C^op _ _ _ f (KernelArrow K) = ZeroArrow (Zero_opp Z) z K.
Proof.
cbn. rewrite (KernelCompZero Z K). apply ZeroArrow_opp.
Qed.

Lemma Kernel_opp_isCokernel {y z : C} (f : Cy, z) (Z : Zero C) (K : @Kernel C Z y z f) :
isCokernel (Zero_opp Z) f (KernelArrow K) (Kernel_opp_eq f Z K).
Proof.
use make_isCokernel.
- exact (has_homsets_opp hs).
- intros w h H'. cbn in H'.
use unique_exists.
+ rewrite <- ZeroArrow_opp in H'. exact (KernelIn Z K w h H').
+ cbn. use KernelCommutes.
+ intros y0. apply (has_homsets_opp hs).
+ cbn. intros y0 X. use KernelInsEq. rewrite KernelCommutes. exact X.
Qed.

Definition Kernel_opp {y z : C} (f : Cy, z) (Z : Zero C) (K : @Kernel C Z y z f) :
@Cokernel (C^op) (Zero_opp Z) z y f.
Proof.
use make_Cokernel.
- exact K.
- exact (KernelArrow K).
- exact (Kernel_opp_eq f Z K).
- exact (Kernel_opp_isCokernel f Z K).
Defined.

Lemma isKernel_opp {x y z : C^op} {f : Cx, y} {g : Cy, z} {Z : Zero C}
{H : f · g = ZeroArrow Z _ _} (CK' : isCokernel Z f g H) {Z' : Zero C^op} :
isKernel Z' (g : C^opz, y) (f : C^opy, x) (isCokernel_opp_eq f g Z H Z').
Proof.
set (CK := make_Cokernel _ _ _ _ CK').
use make_isKernel.
- exact (has_homsets_opp hs).
- intros w h H'.
rewrite <- (ZerosArrowEq C^op (Zero_opp Z) Z' w x) in H'.
rewrite <- ZeroArrow_opp in H'.
use unique_exists.
+ exact (CokernelOut Z CK w h H').
+ use (CokernelCommutes Z CK).
+ intros y0. apply hs.
+ cbn. intros y0 X. use (CokernelOutsEq _ CK). rewrite (CokernelCommutes Z CK). cbn. rewrite X.
apply idpath.
Qed.

Local Lemma Cokernel_opp_eq {y z : C} (f : Cy, z) (Z : Zero C) (CK : @Cokernel C Z y z f) :
@compose C^op _ _ _ (CokernelArrow CK) f = ZeroArrow (Zero_opp Z) CK y.
Proof.
cbn. rewrite (CokernelCompZero Z CK). apply ZeroArrow_opp.
Qed.

Lemma Cokernel_opp_isKernel {y z : C} (f : Cy, z) (Z : Zero C)
(CK : @Cokernel C Z y z f) :
isKernel (Zero_opp Z) (CokernelArrow CK) f (Cokernel_opp_eq f Z CK).
Proof.
use make_isKernel.
- exact (has_homsets_opp hs).
- intros w h H'. cbn in H'.
use unique_exists.
+ rewrite <- ZeroArrow_opp in H'. exact (CokernelOut Z CK w h H').
+ cbn. use CokernelCommutes.
+ intros y0. apply (has_homsets_opp hs).
+ cbn. intros y0 X. use CokernelOutsEq. rewrite CokernelCommutes. exact X.
Qed.

Definition Cokernel_opp {y z : C} (f : Cy, z) (Z : Zero C) (CK : @Cokernel C Z y z f) :
@Kernel (C^op) (Zero_opp Z) z y f.
Proof.
use make_Kernel.
- exact CK.
- exact (CokernelArrow CK).
- exact (Cokernel_opp_eq f Z CK).
- exact (Cokernel_opp_isKernel f Z CK).
Defined.

Definition Kernels_opp (Z : Zero C) (K : @Kernels C Z) : @Cokernels (C^op) (Zero_opp Z).
Proof.
intros x y f.
use Kernel_opp.
apply (K y x f).
Defined.

Definition Cokernels_opp (Z : Zero C) (CK : @Cokernels C Z) : @Kernels (C^op) (Zero_opp Z).
Proof.
intros x y f.
use Cokernel_opp.
apply (CK y x f).
Defined.

## Pushouts and pullbacks

Definition isPushout_opp {a b c d : C} (f : Ca, b) (g : Ca, c) (in1 : Cb, d) (in2 : Cc, d)
(H : f · in1 = g · in2) (iPo : @isPushout C a b c d f g in1 in2 H) :
@isPullback (C^op) a b c d f g in1 in2 H := iPo.

Definition isPullback_opp {a b c d : C} (f : Cb, a) (g : Cc, a) (p1 : Cd, b) (p2 : Cd, c)
(H : p1 · f = p2 · g) (iPb : @isPullback C a b c d f g p1 p2 H) :
@isPushout (C^op) a b c d f g p1 p2 H := iPb.

Definition Pushout_opp {a b c : C} (f : Ca, b) (g : Ca, c) (Po : @Pushout C a b c f g) :
@Pullback (C^op) a b c f g := Po.

Definition Pullback_opp {a b c : C} (f : Cb, a) (g : Cc, a) (Pb : @Pullback C a b c f g) :
@Pushout (C^op) a b c f g := Pb.

Definition Pushouts_opp (Pos : @Pushouts C) : @Pullbacks (C^op) := Pos.

Definition Pullbacks_opp (Pbs : @Pushouts C) : @Pullbacks (C^op) := Pbs.

## BinProducts and BinCoproducts

Definition isBinProduct_opp (c d p : C) (p1 : Cp, c) (p2 : Cp, d)
(iBPC : @isBinProduct C c d p p1 p2) :
@isBinCoproduct (C^op) c d p p1 p2 := iBPC.

Definition isBinCoproduct_opp (a b co : C) (ia : Ca, co) (ib : Cb, co)
(iBCC : @isBinCoproduct C a b co ia ib) :
@isBinProduct (C^op) a b co ia ib := iBCC.

Definition BinProduct_opp (c d : C) (iBPC : @BinProduct C c d) :
@BinCoproduct (C^op) c d := iBPC.

Definition BinCoproduct_opp (c d : C) (iBCC : @BinCoproduct C c d) :
@BinProduct (C^op) c d := iBCC.

Definition BinProducts_opp (BP : @BinProducts C) : @BinCoproducts (C^op) := BP.

Definition BinCoproducts_opp (BC : @BinCoproducts C) : @BinProducts (C^op) := BC.

End def_opposites'.

Definition opp_zero_lifts {C:precategory} {X:Type} (j : X ob C) :
zero_lifts C j zero_lifts (opp_precat C) j.
Proof.
apply hinhfun; intros [z iz]. z. exact (isZero_opp C iz).
Defined.