Require Import Basics.Overture Basics.Tactics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import WildCat.Core WildCat.Opposite.
Require Import WildCat.Equiv.

(** A wild category is pointed if the initial and terminal object are the same. *)
Class IsPointedCat (A : Type) `{Is1Cat A} := {
  zero_object : A;
  isinitial_zero_object : IsInitial zero_object;
  isterminal_zero_object : IsTerminal zero_object;
}.

Global Existing Instance isinitial_zero_object.
Global Existing Instance isterminal_zero_object.

(** The zero morphism between objects [a] and [b] of a pointed category [A] is the unique morphism that factors throguh the zero object. *)
Definition zero_morphism {A : Type} `{IsPointedCat A} {a b : A} : a $-> b
  := (mor_initial _ b) $o (mor_terminal a _).

Section ZeroLaws.

  Context {A : Type} `{IsPointedCat A} {a b c : A}
    (f : a $-> b) (g : b $-> c).

  Definition cat_zero_source (h : zero_object $-> a) : h $== zero_morphism
    := (mor_initial_unique _ _ _)^$ $@ (mor_initial_unique _ _ _).

  Definition cat_zero_target (h : a $-> zero_object) : h $== zero_morphism
    := (mor_terminal_unique _ _ _)^$ $@ (mor_terminal_unique _ _ _).

  (** We show the last two arguments so that end pointes can easily be specified. *)
  Arguments zero_morphism {_ _ _ _ _ _} _ _.

  Definition cat_zero_l : zero_morphism b c $o f $== zero_morphism a c.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
a, b, c: A
f: a $-> b
g: b $-> c
zero_morphism b c $o f $== zero_morphism a c
  Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
a, b, c: A
f: a $-> b
g: b $-> c
zero_morphism b c $o f $== zero_morphism a c
    refine (cat_assoc _ _ _ $@ (_ $@L _^$)).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
a, b, c: A
f: a $-> b
g: b $-> c
mor_terminal a zero_object $->
mor_terminal b zero_object $o f
    apply mor_terminal_unique.
  Defined.

  Definition cat_zero_r : g $o zero_morphism a b $== zero_morphism a c.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
a, b, c: A
f: a $-> b
g: b $-> c
g $o zero_morphism a b $== zero_morphism a c
  Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
a, b, c: A
f: a $-> b
g: b $-> c
g $o zero_morphism a b $== zero_morphism a c
    refine ((_ $@R _) $@ cat_assoc _ _ _)^$.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
a, b, c: A
f: a $-> b
g: b $-> c
mor_initial zero_object c $==
g $o mor_initial zero_object b
    apply mor_initial_unique.
  Defined.

  (** Any morphism which factors through an object equivalent to the zero object is homotopic to the zero morphism. *)
  Definition cat_zero_m `{!HasEquivs A} (be : b $<~> zero_object)
    : g $o f $== zero_morphism a c.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
a, b, c: A
f: a $-> b
g: b $-> c
HasEquivs0: HasEquivs A
be: b $<~> zero_object
g $o f $== zero_morphism a c
  Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
a, b, c: A
f: a $-> b
g: b $-> c
HasEquivs0: HasEquivs A
be: b $<~> zero_object
g $o f $== zero_morphism a c
    refine (_ $@L (compose_V_hh be f)^$ $@ _).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
a, b, c: A
f: a $-> b
g: b $-> c
HasEquivs0: HasEquivs A
be: b $<~> zero_object
g $o (be^-1$ $o (be $o f)) $== zero_morphism a c
    refine (cat_assoc_opp _ _ _ $@ _).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
a, b, c: A
f: a $-> b
g: b $-> c
HasEquivs0: HasEquivs A
be: b $<~> zero_object
g $o be^-1$ $o (be $o f) $== zero_morphism a c
    refine (_ $@L (mor_terminal_unique a _ _)^$ $@ _).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
a, b, c: A
f: a $-> b
g: b $-> c
HasEquivs0: HasEquivs A
be: b $<~> zero_object
g $o be^-1$ $o mor_terminal a zero_object $==
zero_morphism a c
    exact ((mor_initial_unique _ _ _)^$ $@R _).
  Defined.

End ZeroLaws.

(** We make the last two arguments explicit so that end points can easily be specified. We had to do this again, since the section encapsulated the previous attempt. *)
Local Arguments zero_morphism {_ _ _ _ _ _} _ _.

(** A functor is pointed if it preserves the zero object. *)
Class IsPointedFunctor {A B : Type} (F : A -> B) `{Is1Functor A B F} :=
{
  preservesinitial_pfunctor : PreservesInitial F ;
  preservesterminal_pfunctor : PreservesTerminal F ;
}.
Global Existing Instances preservesinitial_pfunctor preservesterminal_pfunctor.

(** Here is an alternative constructor using preservation of the zero object. This requires more structure on the categories however. *)
Definition Build_IsPointedFunctor' {A B : Type} (F : A -> B)
  `{Is1Cat A, Is1Cat B, !Is0Functor F, !Is1Functor F}
  `{!IsPointedCat A, !IsPointedCat B, !HasEquivs A, !HasEquivs B}
  (p : F zero_object $<~> zero_object)
  : IsPointedFunctor F.
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedCat0: IsPointedCat A
IsPointedCat1: IsPointedCat B
HasEquivs0: HasEquivs A
HasEquivs1: HasEquivs B
p: F zero_object $<~> zero_object
IsPointedFunctor F
Proof.
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedCat0: IsPointedCat A
IsPointedCat1: IsPointedCat B
HasEquivs0: HasEquivs A
HasEquivs1: HasEquivs B
p: F zero_object $<~> zero_object
IsPointedFunctor F
  apply Build_IsPointedFunctor.
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedCat0: IsPointedCat A
IsPointedCat1: IsPointedCat B
HasEquivs0: HasEquivs A
HasEquivs1: HasEquivs B
p: F zero_object $<~> zero_object
PreservesInitial F
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedCat0: IsPointedCat A
IsPointedCat1: IsPointedCat B
HasEquivs0: HasEquivs A
HasEquivs1: HasEquivs B
p: F zero_object $<~> zero_object
PreservesTerminal F
  +
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedCat0: IsPointedCat A
IsPointedCat1: IsPointedCat B
HasEquivs0: HasEquivs A
HasEquivs1: HasEquivs B
p: F zero_object $<~> zero_object
PreservesInitial F intros x inx.
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedCat0: IsPointedCat A
IsPointedCat1: IsPointedCat B
HasEquivs0: HasEquivs A
HasEquivs1: HasEquivs B
p: F zero_object $<~> zero_object
x: A
inx: IsInitial x
IsInitial (F x)
    rapply isinitial_cate.
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedCat0: IsPointedCat A
IsPointedCat1: IsPointedCat B
HasEquivs0: HasEquivs A
HasEquivs1: HasEquivs B
p: F zero_object $<~> zero_object
x: A
inx: IsInitial x
zero_object $<~> F x
    symmetry.
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedCat0: IsPointedCat A
IsPointedCat1: IsPointedCat B
HasEquivs0: HasEquivs A
HasEquivs1: HasEquivs B
p: F zero_object $<~> zero_object
x: A
inx: IsInitial x
F x $<~> zero_object
    refine (p $oE _).
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedCat0: IsPointedCat A
IsPointedCat1: IsPointedCat B
HasEquivs0: HasEquivs A
HasEquivs1: HasEquivs B
p: F zero_object $<~> zero_object
x: A
inx: IsInitial x
F x $<~> F zero_object
    rapply (emap F _).
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedCat0: IsPointedCat A
IsPointedCat1: IsPointedCat B
HasEquivs0: HasEquivs A
HasEquivs1: HasEquivs B
p: F zero_object $<~> zero_object
x: A
inx: IsInitial x
x $<~> zero_object
    rapply cate_isinitial.
  +
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedCat0: IsPointedCat A
IsPointedCat1: IsPointedCat B
HasEquivs0: HasEquivs A
HasEquivs1: HasEquivs B
p: F zero_object $<~> zero_object
PreservesTerminal F intros x tex.
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedCat0: IsPointedCat A
IsPointedCat1: IsPointedCat B
HasEquivs0: HasEquivs A
HasEquivs1: HasEquivs B
p: F zero_object $<~> zero_object
x: A
tex: IsTerminal x
IsTerminal (F x)
    rapply isterminal_cate.
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedCat0: IsPointedCat A
IsPointedCat1: IsPointedCat B
HasEquivs0: HasEquivs A
HasEquivs1: HasEquivs B
p: F zero_object $<~> zero_object
x: A
tex: IsTerminal x
F x $<~> zero_object
    refine (p $oE _).
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedCat0: IsPointedCat A
IsPointedCat1: IsPointedCat B
HasEquivs0: HasEquivs A
HasEquivs1: HasEquivs B
p: F zero_object $<~> zero_object
x: A
tex: IsTerminal x
F x $<~> F zero_object
    rapply (emap F _).
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedCat0: IsPointedCat A
IsPointedCat1: IsPointedCat B
HasEquivs0: HasEquivs A
HasEquivs1: HasEquivs B
p: F zero_object $<~> zero_object
x: A
tex: IsTerminal x
x $<~> zero_object
    rapply cate_isterminal.
Defined.

(** Pointed functors preserve the zero object upto isomorphism. *)
Lemma pfunctor_zero {A B : Type} (F : A -> B)
  `{IsPointedCat A, IsPointedCat B, !HasEquivs B,
    !Is0Functor F, !Is1Functor F, !IsPointedFunctor F}
  : F zero_object $<~> zero_object.
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: IsPointedCat B
HasEquivs0: HasEquivs B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedFunctor0: IsPointedFunctor F
F zero_object $<~> zero_object
Proof.
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: IsPointedCat B
HasEquivs0: HasEquivs B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedFunctor0: IsPointedFunctor F
F zero_object $<~> zero_object
  rapply cate_isinitial.
Defined.

(** Pointed functors preserve the zero morphism upto homotopy *)
Lemma fmap_zero_morphism {A B : Type} (F : A -> B)
  `{IsPointedCat A, IsPointedCat B, !HasEquivs B,
    !Is0Functor F, !Is1Functor F, !IsPointedFunctor F} {a b : A}
  : fmap F (zero_morphism a b) $== zero_morphism (F a) (F b).
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: IsPointedCat B
HasEquivs0: HasEquivs B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedFunctor0: IsPointedFunctor F
a, b: A
fmap F (zero_morphism a b) $==
zero_morphism (F a) (F b)
Proof.
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: IsPointedCat B
HasEquivs0: HasEquivs B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedFunctor0: IsPointedFunctor F
a, b: A
fmap F (zero_morphism a b) $==
zero_morphism (F a) (F b)
  refine (fmap_comp F _ _ $@ _).
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: IsPointedCat B
HasEquivs0: HasEquivs B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedFunctor0: IsPointedFunctor F
a, b: A
fmap F (mor_initial zero_object b) $o
fmap F (mor_terminal a zero_object) $==
zero_morphism (F a) (F b)
  refine (_ $@R _ $@ _).
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: IsPointedCat B
HasEquivs0: HasEquivs B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedFunctor0: IsPointedFunctor F
a, b: A
fmap F (mor_initial zero_object b) $== ?Goal
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: IsPointedCat B
HasEquivs0: HasEquivs B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedFunctor0: IsPointedFunctor F
a, b: A
?Goal $o fmap F (mor_terminal a zero_object) $==
zero_morphism (F a) (F b)
  1: nrapply fmap_initial; [exact _].
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: IsPointedCat B
HasEquivs0: HasEquivs B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedFunctor0: IsPointedFunctor F
a, b: A
mor_initial (F zero_object) (F b) $o
fmap F (mor_terminal a zero_object) $==
zero_morphism (F a) (F b)
  refine (_ $@L _ $@ _).
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: IsPointedCat B
HasEquivs0: HasEquivs B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedFunctor0: IsPointedFunctor F
a, b: A
fmap F (mor_terminal a zero_object) $== ?Goal
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: IsPointedCat B
HasEquivs0: HasEquivs B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedFunctor0: IsPointedFunctor F
a, b: A
mor_initial (F zero_object) (F b) $o ?Goal $==
zero_morphism (F a) (F b)
  1: nrapply fmap_terminal; [exact _].
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: IsPointedCat B
HasEquivs0: HasEquivs B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedFunctor0: IsPointedFunctor F
a, b: A
mor_initial (F zero_object) (F b) $o
mor_terminal (F a) (F zero_object) $==
zero_morphism (F a) (F b)
  rapply cat_zero_m.
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: IsPointedCat B
HasEquivs0: HasEquivs B
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
IsPointedFunctor0: IsPointedFunctor F
a, b: A
F zero_object $<~> zero_object
  rapply pfunctor_zero.
Defined.

(** Opposite category of a pointed category is also pointed. *)
Global Instance ispointedcat_op {A : Type} `{IsPointedCat A} : IsPointedCat A^op.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
IsPointedCat A^op
Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
IsPointedCat A^op
  snrapply Build_IsPointedCat.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
A^op
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
IsInitial ?zero_object
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
IsTerminal ?zero_object
  1: unfold op; exact zero_object.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
IsInitial (zero_object : A^op)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: IsPointedCat A
IsTerminal (zero_object : A^op)
  1,2: exact _.
Defined.