Library Exercise_4_1_2_34


Require Import Utf8.
Require Import ProofIrrelevance FunctionalExtensionality.
Require Import Omega.
Require Import JMeq.
Require Import Category Functor DiscreteCategory NatCategory DiscreteCategoryFunctors.
Require Import Common FEqualDep.

Set Implicit Arguments.

Generalizable All Variables.

Exercise 4.1.2.34

Problem

(Terminal category). Let C be a category. How many functors are there C D_1, where D_1 := Disc( 1 ) is the discrete category on one element?
  Variable obj : Type.
  Variable C : @Category obj.

  Lemma proof_irrelevance_JMeq (A B : Prop) (a : A) (b : B) : A = Ba == b.
    intro; subst; apply eq_JMeq; apply proof_irrelevance.
  Qed.

  Definition FunctorToTerminal : Functor C (NatCategory 1).
    refine (Build_Functor C (NatCategory 1)
                          (fun _exist _ 0 (@le_n 1))
                          (fun _ _ _eq_refl)
                          _
                          _);
    abstract (
        intros; simpl; try apply proof_irrelevance
      ).
  Defined.

  Lemma FunctorToTerminalUnique : F, F = FunctorToTerminal.
    intro F.
    apply Functor_Eq; simpl_eq; intros;
    repeat match goal with
             | [ H : _ |- _ ] ⇒ clear H
             | [ m : Morphism ?C ?s ?d |- _ ] ⇒
               simpl; destruct (MorphismOf F m); clear m;
               apply proof_irrelevance_JMeq;
               apply f_equal2;
               simpl_eq
             | [ x : obj |- _ ] ⇒
               let x0 := fresh in
               let H := fresh in
               set (H := F x) in *;
                 destruct H as [ x0 ? ];
                 induction x0;
                 simpl;
                 omega
             | _simpl; apply ProofIrrelevance.proof_irrelevance
           end.
  Qed.
End Exercise_4_1_2_34.