Library Exercise_4_1_2_33


Require Import Utf8.
Require Import Omega.
Require Import DiscreteCategory NatCategory DiscreteCategoryFunctors Functor.

Set Implicit Arguments.

Generalizable All Variables.

Exercise 4.1.2.33

Problem

Recall the definition of the set _n_ for any natural number n : , and let D_n := Disc( _n_ ) : Ob Cat. List all the morphisms in D_4. List all the functors D_3 D_2.

  Let D_3 := NatCategory 3.
  Let D_2 := NatCategory 2.

  Lemma OneLtTwo : 1 < 2. repeat constructor. Qed.
  Lemma ZeroLtTwo : 0 < 2. repeat constructor. Qed.
  Lemma ThreeNotLtThree n : S (S (S n)) < 3 → False. omega. Qed.

  Local Ltac mk_functor a b c :=
    apply FunctorFromDiscrete;
    refine (fun xmatch proj1_sig x as n return (n < 3 {k : | k < 2}) with
                       | 0 ⇒ fun _exist _ a _
                       | 1 ⇒ fun _exist _ b _
                       | 2 ⇒ fun _exist _ c _
                       | S (S (S n')) ⇒ fun pfmatch ThreeNotLtThree pf with end
                     end (proj2_sig x));
    try exact ZeroLtTwo;
    try exact OneLtTwo.

  Example E_4_1_2_33_Functor_1 : Functor D_3 D_2. mk_functor 0 0 0. Defined.
  Example E_4_1_2_33_Functor_2 : Functor D_3 D_2. mk_functor 0 0 1. Defined.
  Example E_4_1_2_33_Functor_3 : Functor D_3 D_2. mk_functor 0 1 0. Defined.
  Example E_4_1_2_33_Functor_4 : Functor D_3 D_2. mk_functor 0 1 1. Defined.
  Example E_4_1_2_33_Functor_5 : Functor D_3 D_2. mk_functor 1 0 0. Defined.
  Example E_4_1_2_33_Functor_6 : Functor D_3 D_2. mk_functor 1 0 1. Defined.
  Example E_4_1_2_33_Functor_7 : Functor D_3 D_2. mk_functor 1 1 0. Defined.
  Example E_4_1_2_33_Functor_8 : Functor D_3 D_2. mk_functor 1 1 1. Defined.
End Exercise_4_1_2_33.