# 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.