Library UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.AugmentedSimplexCategory
Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.NaturalNumbers.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.Combinatorics.StandardFiniteSets.
Require Import UniMath.Combinatorics.FiniteSets.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored.
Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored.
Require Import UniMath.CategoryTheory.SimplicialSets.
Definition fincard_has_homsets (n m : nat) : isaset ((⟦ n ⟧)%stn -> (⟦ m ⟧)%stn) :=
(Propositions.funspace_isaset (isasetstn m)).
Proposition iscontr_inequal (n m : nat) : iscontr ((n > m) ⨿ (n ≤ m)).
Show proof.
Local Proposition iscontr_inequal' (n m : nat) : iscontr ((n < m) ⨿ (n ≥ m)).
Show proof.
Local Proposition fincard_hom_extensionality { n m : nat } { f g : (⟦ n ⟧)%stn → (⟦ m ⟧)%stn } : (∏ x : (⟦ n ⟧)%stn, (pr1 (f x)= pr1 (g x))) -> f=g.
Show proof.
Definition ordconstr {n : nat} (k : nat) (bd : k < n) : stn n := k,,bd.
Definition precat_Delta_precategory_data : precategory_data.
Show proof.
Definition precat_Delta_is_precategory : is_precategory precat_Delta_precategory_data.
Show proof.
Definition precat_Delta : precategory :=
(precat_Delta_precategory_data,, precat_Delta_is_precategory).
Notation "C ⊠ D" := (precategory_binproduct C D) (at level 38).
Definition precat_fincard_data : precategory_data.
Show proof.
Proposition precat_fincard_is_precategory : is_precategory precat_fincard_data.
Show proof.
Definition precat_fincard : precategory := (precat_fincard_data,, precat_fincard_is_precategory).
Proposition Delta_has_homsets : has_homsets precat_Delta.
Show proof.
Definition category_Delta : category := (precat_Delta,, Delta_has_homsets).
Definition category_fincard : category := (precat_fincard,, fincard_has_homsets).
Notation Δ_sdg := category_fincard.
Notation Δ := category_Delta.
Notation Δ_sd := category_Delta.
Definition Δ_ob_constr ( n : nat) : Δ := n.
Definition Δ_sdg_ob_constr ( n : nat) : Δ_sdg := n.
Open Scope cat.
Definition Δ_mor_constr { n m : nat } ( f : (⟦ n ⟧)%stn -> (⟦ m ⟧)%stn )
( pk : ∏ x y : (⟦ n ⟧)%stn, x ≤ y -> f x ≤ f y) : (Δ_ob_constr n) --> (Δ_ob_constr m)
:= (make_monfunstn f pk).
Definition Δ_sdg_mor_constr { n m : nat } ( f : (⟦ n ⟧)%stn -> (⟦ m ⟧)%stn ) :
Δ_sdg_ob_constr n --> Δ_sdg_ob_constr m := f.
Definition fget_monoton_functor_data : functor_data category_Delta category_fincard.
Show proof.
Proposition fget_monoton_is_functor : is_functor fget_monoton_functor_data.
Show proof.
Definition fget_monoton_functor : functor category_Delta category_fincard :=
(fget_monoton_functor_data,, fget_monoton_is_functor).
Local Notation U := fget_monoton_functor.
Local Proposition U_faithful { a b : Δ } (f g : a --> b) : (# U f = # U g) -> f = g.
Show proof.
Local Proposition morphism_extensionality { a b : Δ } (f g : a --> b) :
(∏ x, (# U f) x = (# U g) x) -> f = g.
Show proof.
Lemma mon_iso_mon_inv {n m : Δ} {f : n --> m} (I : is_z_isomorphism ((# U) f)) :
∏ x y : (⟦m⟧)%stn, x ≤ y -> (is_z_isomorphism_mor I) x ≤ (is_z_isomorphism_mor I) y.
Show proof.
Lemma fincard_inv_is_inverse_in_precat (n m : Δ) (f : n --> m ) (I : is_z_isomorphism ((# U) f)):
is_inverse_in_precat f (is_z_isomorphism_mor I,, mon_iso_mon_inv I).
Show proof.
Lemma U_reflects_isos (n m : Δ) ( f : n --> m ) : (is_z_isomorphism ((# U) f)) -> (is_z_isomorphism f).
Show proof.
Local Proposition U_reflects_id (a : Δ) (f : a --> a) :
(# U f) = id (U a) -> f = id a.
Show proof.
Local Definition ordinal_addition : (Δ ⊠ Δ) → Δ.
Show proof.
Arguments ordinal_addition /.
Local Definition pr_n_m_l { n m : nat} ( x : (⟦ n + m⟧)%stn ) (s : x < n) : (⟦ n ⟧)%stn.
Show proof.
Local Definition pr_n_m_r { n m : nat} ( x : (⟦ n + m⟧)%stn ) (s : x ≥ n) : (⟦ m ⟧)%stn.
Show proof.
Local Definition sumfn {n n' m m' : nat} (f : (⟦ n ⟧)%stn → (⟦ m ⟧)%stn) ( g : (⟦ n' ⟧)%stn → (⟦ m' ⟧)%stn) : (⟦ n + n' ⟧)%stn → (⟦ m + m'⟧)%stn.
Show proof.
Local Proposition pr_n_m_l_compute { n m : nat}
( x : (⟦ n + m⟧)%stn ) (s : x < n) : stntonat _ (pr_n_m_l x s) = stntonat _ x.
Show proof.
Local Proposition pr_n_m_r_compute { n m : nat}
( x : (⟦ n + m⟧)%stn ) (s : x ≥ n) : stntonat _ (pr_n_m_r x s) = (stntonat _ x) - n.
Show proof.
Local Proposition proj_incl_l { n m : nat } ( x : (⟦ n + m⟧)%stn ) (s : x < n) :
(stn_left n m) (pr_n_m_l x s) = x.
Show proof.
Local Proposition proj_incl_r { n m : nat } ( x : (⟦ n + m⟧)%stn ) (s : x ≥ n) :
(stn_right n m) (pr_n_m_r x s) = x.
Show proof.
Definition natlthorgeh_left_branch {n m : nat} (s : n < m) (j : (n < m) ⨿ (n ≥ m)) : j = inl s
:= (proofirrelevancecontr (iscontr_inequal m n) j (inl s)).
Definition natlthorgeh_right_branch {n m : nat} (s : n ≥ m) (j : (n < m) ⨿ (n ≥ m)) : j = inr s
:= (proofirrelevancecontr (iscontr_inequal m n) j (inr s)).
Local Proposition sumfn_l { n n' m m' : nat}
(f : (⟦ n ⟧)%stn -> (⟦ m ⟧)%stn) ( g : (⟦ n' ⟧)%stn -> (⟦ m' ⟧)%stn)
(x : (⟦ n + n' ⟧)%stn) ( s : x < n) : (sumfn f g) x < m.
Show proof.
Local Proposition sumfn_r { n n' m m' : nat }
(f : (⟦ n ⟧)%stn -> (⟦ m ⟧)%stn) (g : (⟦ n' ⟧)%stn -> (⟦ m' ⟧)%stn)
(x : (⟦ n + n' ⟧)%stn) ( s : x ≥ n) : (sumfn f g) x ≥ m.
Show proof.
Local Proposition sumfn_l1 { n n' m m' : nat}
(f : (⟦ n ⟧)%stn -> (⟦ m ⟧)%stn) ( g : (⟦ n' ⟧)%stn -> (⟦ m' ⟧)%stn)
(x : (⟦ n + n' ⟧)%stn) ( s : x < n) :
f (pr_n_m_l x s) = pr_n_m_l ((sumfn f g) x) (sumfn_l f g x s).
Show proof.
Local Proposition sumfn_r1 { n n' m m' : nat}
(f : (⟦ n ⟧)%stn -> (⟦ m ⟧)%stn) (g : (⟦ n' ⟧)%stn -> (⟦ m' ⟧)%stn)
(x : (⟦ n + n' ⟧)%stn) ( s :x ≥ n) :
g (pr_n_m_r x s) = pr_n_m_r ((sumfn f g) x) (sumfn_r f g x s).
Show proof.
Local Proposition sumfn_l2 { n n' m m' : nat}
(f : (⟦ n ⟧)%stn -> (⟦ m ⟧)%stn) ( g : (⟦ n' ⟧)%stn -> (⟦ m' ⟧)%stn)
(x : (⟦ n + n' ⟧)%stn) ( s : x < n) :
(stn_left m m') (f (pr_n_m_l x s)) = (sumfn f g) x.
Show proof.
Local Proposition sumfn_r2 { n n' m m' : nat}
(f : (⟦ n ⟧)%stn -> (⟦ m ⟧)%stn) ( g : (⟦ n' ⟧)%stn -> (⟦ m' ⟧)%stn)
(x : (⟦ n + n' ⟧)%stn) ( s : x ≥ n) :
(stn_right m m') (g (pr_n_m_r x s)) = (sumfn f g) x.
Show proof.
Local Proposition stn_left_monotonic ( n m : nat ) :
∏ x y : (⟦ n ⟧)%stn, (x ≤ y) -> ( stn_left n m x ) ≤ ( stn_left n m y).
Show proof.
Local Proposition stn_right_monotonic ( n m : nat ) :
∏ x y : (⟦ m ⟧)%stn, (x ≤ y) -> ( stn_right n m x ) ≤ ( stn_right n m y).
Show proof.
Definition monfunmonprop { n m : nat } (f : monfunstn n m) := pr2 f.
Local Arguments precategory_binproduct_mor /.
Local Definition ordinal_hom :
∏ a b : ob (Δ ⊠ Δ), a --> b -> (ordinal_addition a) --> (ordinal_addition b).
Show proof.
Local Definition tensor_data_card : (functor_data (Δ_sdg ⊠ Δ_sdg) Δ_sdg).
Show proof.
Local Definition tensor_data_ord : (functor_data (Δ ⊠ Δ) Δ).
Show proof.
Local Proposition tensor_id_card : (functor_idax tensor_data_card).
Show proof.
Local Proposition tensor_id_ord : (functor_idax tensor_data_ord).
Show proof.
Local Proposition tensor_comp_card : (functor_compax tensor_data_card).
Show proof.
Local Proposition tensor_comp_ord : (functor_compax tensor_data_ord).
Show proof.
Local Proposition tensor_card_is_functor : is_functor tensor_data_card.
Show proof.
Local Proposition tensor_ord_is_functor : is_functor tensor_data_ord.
Show proof.
Local Definition tensor_functor_card : functor (Δ_sdg ⊠ Δ_sdg) Δ_sdg.
Show proof.
Local Definition tensor_functor_ord : functor (Δ ⊠ Δ) Δ.
Show proof.
Local Definition tensor_unit : Δ :=0.
Arguments tensor_unit /.
Local Definition tensor_left_unitor_card : left_unitor tensor_functor_card tensor_unit.
Show proof.
Local Definition tensor_left_unitor_ord : left_unitor tensor_functor_ord tensor_unit.
Show proof.
Local Definition tensor_right_unitor_card_nt_data : nat_trans_data (I_posttensor tensor_functor_card tensor_unit) (functor_identity Δ_sdg).
Show proof.
Local Definition tensor_right_unitor_card_is_nat_trans : is_nat_trans (I_posttensor tensor_functor_card tensor_unit) (functor_identity Δ_sdg) tensor_right_unitor_card_nt_data.
Show proof.
Local Definition tensor_right_unitor_card : right_unitor tensor_functor_card tensor_unit.
Show proof.
Local Definition tensor_right_unitor_ord_nt_data : nat_trans_data (I_posttensor tensor_functor_ord tensor_unit) (functor_identity Δ_sd).
Show proof.
Arguments tensor_right_unitor_ord_nt_data /.
Local Definition tensor_right_unitor_ord_is_nat_trans : is_nat_trans (I_posttensor tensor_functor_ord tensor_unit) (functor_identity Δ_sd) tensor_right_unitor_ord_nt_data.
Show proof.
Local Proposition tensor_right_unitor_ord : right_unitor tensor_functor_ord tensor_unit.
Show proof.
Definition tensor_associator_card_nat_trans_data : nat_trans_data (assoc_left tensor_functor_card) (assoc_right tensor_functor_card).
Show proof.
Arguments tensor_associator_card_nat_trans_data /.
Definition tensor_associator_card_is_nat_trans : is_nat_trans _ _ tensor_associator_card_nat_trans_data.
Show proof.
Definition tensor_associator_card_nat_trans : nat_trans (assoc_left tensor_functor_card) (assoc_right tensor_functor_card)
:= (tensor_associator_card_nat_trans_data,,tensor_associator_card_is_nat_trans).
Definition tensor_associator_ord_nat_trans_data :
nat_trans_data (assoc_left tensor_functor_ord) (assoc_right tensor_functor_ord).
Show proof.
Arguments tensor_associator_ord_nat_trans_data /.
Definition tensor_associator_ord_is_nat_trans : is_nat_trans _ _ tensor_associator_ord_nat_trans_data.
Show proof.
Definition tensor_associator_ord_nat_trans :
nat_trans (assoc_left tensor_functor_ord) (assoc_right tensor_functor_ord):=
(tensor_associator_ord_nat_trans_data,, tensor_associator_ord_is_nat_trans).
Definition tensor_associator_card : associator tensor_functor_card.
Show proof.
Definition tensor_associator_ord : associator tensor_functor_ord.
unfold associator, nat_z_iso.
exists tensor_associator_ord_nat_trans.
unfold is_nat_z_iso.
intro c. induction c as [nm k]. induction nm as [n m].
unfold is_z_isomorphism.
use tpair. {
simpl. rewrite natplusassoc. exact (monfunstnid _).
}
{ abstract(cbv beta;
unfold is_inverse_in_precat, tensor_associator_ord_nat_trans,
tensor_associator_ord_nat_trans_data;
split;
simpl; induction (natplusassoc n m k); simpl;
apply morphism_extensionality; reflexivity;
simpl; induction (pathsinv0 (natplusassoc n m k));
simpl; induction (natplusassoc n m k); simpl; apply morphism_extensionality;
reflexivity).
}
Defined.
Proposition triangle_eq_holds_card : triangle_eq tensor_functor_card tensor_unit tensor_left_unitor_card tensor_right_unitor_card tensor_associator_card.
Show proof.
Proposition triangle_eq_holds_ord : triangle_eq tensor_functor_ord tensor_unit tensor_left_unitor_ord tensor_right_unitor_ord tensor_associator_ord.
Show proof.
Proposition pentagon_eq_holds_card : pentagon_eq tensor_functor_card tensor_associator_card.
Show proof.
Proposition pentagon_eq_holds_ord : pentagon_eq tensor_functor_ord tensor_associator_ord.
Show proof.
Definition AugmentedSimplexCategory : monoidal_cat.
Show proof.
Definition FinCard : monoidal_cat.
Show proof.
Definition U_ε : (monoidal_cat_unit FinCard) --> U (monoidal_cat_unit AugmentedSimplexCategory).
Show proof.
Definition U_μ : monoidal_functor_map AugmentedSimplexCategory FinCard U.
Show proof.
Definition U_α : monoidal_functor_associativity AugmentedSimplexCategory FinCard U U_μ.
Show proof.
Local Proposition U_unitality : monoidal_functor_unitality AugmentedSimplexCategory FinCard U U_ε U_μ.
Show proof.
Definition U_Mon_Lax : lax_monoidal_functor AugmentedSimplexCategory FinCard.
Show proof.
Definition U_Mon_Strong : strong_monoidal_functor AugmentedSimplexCategory FinCard.
Show proof.
Local Lemma functor_eq_to_object_eq_on_homs
(C D : precategory) (F G : functor C D) ( p : F = G) (c : C) (d : D) ( f : d --> G c) :
internal_paths_rew_r (C ⟶ D) F G (λ H : C ⟶ D, D ⟦ d , H c⟧) f p =
internal_paths_rew_r D (F c) (G c) (λ d' : D, D ⟦ d , d' ⟧) f
(maponpaths (λ H : C ⟶ D, H c) p).
Show proof.
Local Proposition tensor_card_is_strict_left_iso_id :
∏ eq_λ : I_pretensor (monoidal_cat_tensor FinCard)
(monoidal_cat_unit FinCard) = functor_identity (pr1 FinCard),
(is_nat_z_iso_id eq_λ (monoidal_cat_left_unitor FinCard)).
Show proof.
Local Arguments monoidal_cat_tensor /.
Local Arguments monoidal_cat_unit /.
Local Arguments functor_fix_fst_arg /.
Local Arguments functor_fix_snd_arg /.
Local Arguments functor_fix_fst_arg_ob /.
Local Arguments functor_fix_snd_arg_ob /.
Local Definition right_unitor_id (c : Δ_sdg) :
I_posttensor (monoidal_cat_tensor FinCard)
(monoidal_cat_unit FinCard) c = functor_identity (pr1 FinCard) c.
Show proof.
Local Proposition tensor_card_is_strict_right_iso_id : ∏ eq_ρ : I_posttensor (monoidal_cat_tensor FinCard)
(monoidal_cat_unit FinCard) = functor_identity (pr1 FinCard),
is_nat_z_iso_id eq_ρ (monoidal_cat_right_unitor FinCard).
Show proof.
Local Proposition tensor_card_is_strict_associator_id :
∏ eq_α : assoc_left tensor_functor_card = assoc_right tensor_functor_card,
is_nat_z_iso_id eq_α (monoidal_cat_associator FinCard).
Show proof.
Definition FinCardStrict : strict_monoidal_cat.
Show proof.
Local Proposition tensor_Δ_left_unitor_is_id :
∏ eq_λ : I_pretensor (monoidal_cat_tensor AugmentedSimplexCategory)
(monoidal_cat_unit AugmentedSimplexCategory) = functor_identity (pr1 AugmentedSimplexCategory), (is_nat_z_iso_id eq_λ (monoidal_cat_left_unitor AugmentedSimplexCategory)).
Show proof.
Local Proposition tensor_Δ_right_unitor_is_id :
∏ eq_ρ : I_posttensor (monoidal_cat_tensor AugmentedSimplexCategory)
(monoidal_cat_unit AugmentedSimplexCategory) =
functor_identity (pr1 AugmentedSimplexCategory),
is_nat_z_iso_id eq_ρ (monoidal_cat_right_unitor AugmentedSimplexCategory).
Show proof.
Local Proposition tensor_ord_is_strict_associator_id :
∏ eq_α : assoc_left tensor_functor_ord = assoc_right tensor_functor_ord,
is_nat_z_iso_id eq_α (monoidal_cat_associator AugmentedSimplexCategory).
Show proof.
Definition FinOrdStrict : strict_monoidal_cat.
Show proof.
Require Import UniMath.Foundations.NaturalNumbers.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.Combinatorics.StandardFiniteSets.
Require Import UniMath.Combinatorics.FiniteSets.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored.
Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored.
Require Import UniMath.CategoryTheory.SimplicialSets.
Definition fincard_has_homsets (n m : nat) : isaset ((⟦ n ⟧)%stn -> (⟦ m ⟧)%stn) :=
(Propositions.funspace_isaset (isasetstn m)).
Proposition iscontr_inequal (n m : nat) : iscontr ((n > m) ⨿ (n ≤ m)).
Show proof.
unfold iscontr.
exists (natgthorleh n m). intro t.
induction t.
- unfold natgthorleh.
induction (isdecrelnatgth n m).
+ simpl. apply maponpaths. apply (pr2 (n > m)).
+ contradiction.
- unfold natgthorleh.
induction (isdecrelnatgth n m).
+ simpl. assert (¬ (n > m)). { apply natlehtonegnatgth. assumption. } contradiction.
+ simpl. apply maponpaths. apply (pr2 (n ≤ m)).
exists (natgthorleh n m). intro t.
induction t.
- unfold natgthorleh.
induction (isdecrelnatgth n m).
+ simpl. apply maponpaths. apply (pr2 (n > m)).
+ contradiction.
- unfold natgthorleh.
induction (isdecrelnatgth n m).
+ simpl. assert (¬ (n > m)). { apply natlehtonegnatgth. assumption. } contradiction.
+ simpl. apply maponpaths. apply (pr2 (n ≤ m)).
Local Proposition iscontr_inequal' (n m : nat) : iscontr ((n < m) ⨿ (n ≥ m)).
Show proof.
Local Proposition fincard_hom_extensionality { n m : nat } { f g : (⟦ n ⟧)%stn → (⟦ m ⟧)%stn } : (∏ x : (⟦ n ⟧)%stn, (pr1 (f x)= pr1 (g x))) -> f=g.
Show proof.
Definition ordconstr {n : nat} (k : nat) (bd : k < n) : stn n := k,,bd.
Definition precat_Delta_precategory_data : precategory_data.
Show proof.
use make_precategory_data.
- exact (make_precategory_ob_mor nat monfunstn).
- intros m. apply monfunstnid. - intros l m n f g. exact (monfunstncomp f g).
- exact (make_precategory_ob_mor nat monfunstn).
- intros m. apply monfunstnid. - intros l m n f g. exact (monfunstncomp f g).
Definition precat_Delta_is_precategory : is_precategory precat_Delta_precategory_data.
Show proof.
unfold precat_Delta_precategory_data.
unfold is_precategory. split. {
split.
- intros a b f. unfold "id". simpl in *. reflexivity.
- intros a b f. unfold "id". simpl in *. reflexivity.
} {
split.
- reflexivity.
- reflexivity.
}
unfold is_precategory. split. {
split.
- intros a b f. unfold "id". simpl in *. reflexivity.
- intros a b f. unfold "id". simpl in *. reflexivity.
} {
split.
- reflexivity.
- reflexivity.
}
Definition precat_Delta : precategory :=
(precat_Delta_precategory_data,, precat_Delta_is_precategory).
Notation "C ⊠ D" := (precategory_binproduct C D) (at level 38).
Definition precat_fincard_data : precategory_data.
Show proof.
unshelve eapply (make_precategory_data _).
- unshelve eapply (make_precategory_ob_mor _ _).
* exact nat.
* exact (λ n, λ m, (⟦n⟧%stn → ⟦m⟧%stn)). - intro c. exact (idfun (⟦c⟧)%stn). - intros n m k f g. exact (g∘f).
- unshelve eapply (make_precategory_ob_mor _ _).
* exact nat.
* exact (λ n, λ m, (⟦n⟧%stn → ⟦m⟧%stn)). - intro c. exact (idfun (⟦c⟧)%stn). - intros n m k f g. exact (g∘f).
Proposition precat_fincard_is_precategory : is_precategory precat_fincard_data.
Show proof.
unfold precat_Delta_precategory_data.
unfold is_precategory. split. {
split.
- intros a b f. unfold "id". simpl in *. reflexivity.
- intros a b f. unfold "id". simpl in *. reflexivity.
} {
split.
- reflexivity.
- reflexivity.
}
unfold is_precategory. split. {
split.
- intros a b f. unfold "id". simpl in *. reflexivity.
- intros a b f. unfold "id". simpl in *. reflexivity.
} {
split.
- reflexivity.
- reflexivity.
}
Definition precat_fincard : precategory := (precat_fincard_data,, precat_fincard_is_precategory).
Proposition Delta_has_homsets : has_homsets precat_Delta.
Show proof.
unfold has_homsets. simpl. intros a b.
apply isaset_total2.
- exact (fincard_has_homsets a b).
- intro f. apply impred_isaset. intro x. apply impred_isaset. intro y. apply impred_isaset.
intro. exact (isasetaprop (propproperty (f x ≤ f y))).
apply isaset_total2.
- exact (fincard_has_homsets a b).
- intro f. apply impred_isaset. intro x. apply impred_isaset. intro y. apply impred_isaset.
intro. exact (isasetaprop (propproperty (f x ≤ f y))).
Definition category_Delta : category := (precat_Delta,, Delta_has_homsets).
Definition category_fincard : category := (precat_fincard,, fincard_has_homsets).
Notation Δ_sdg := category_fincard.
Notation Δ := category_Delta.
Notation Δ_sd := category_Delta.
Definition Δ_ob_constr ( n : nat) : Δ := n.
Definition Δ_sdg_ob_constr ( n : nat) : Δ_sdg := n.
Open Scope cat.
Definition Δ_mor_constr { n m : nat } ( f : (⟦ n ⟧)%stn -> (⟦ m ⟧)%stn )
( pk : ∏ x y : (⟦ n ⟧)%stn, x ≤ y -> f x ≤ f y) : (Δ_ob_constr n) --> (Δ_ob_constr m)
:= (make_monfunstn f pk).
Definition Δ_sdg_mor_constr { n m : nat } ( f : (⟦ n ⟧)%stn -> (⟦ m ⟧)%stn ) :
Δ_sdg_ob_constr n --> Δ_sdg_ob_constr m := f.
Definition fget_monoton_functor_data : functor_data category_Delta category_fincard.
Show proof.
Proposition fget_monoton_is_functor : is_functor fget_monoton_functor_data.
Show proof.
Definition fget_monoton_functor : functor category_Delta category_fincard :=
(fget_monoton_functor_data,, fget_monoton_is_functor).
Local Notation U := fget_monoton_functor.
Local Proposition U_faithful { a b : Δ } (f g : a --> b) : (# U f = # U g) -> f = g.
Show proof.
apply subtypeInjectivity. unfold isPredicate.
intro. apply impred_isaprop.
intro. apply impred_isaprop.
intro. apply impred_isaprop.
intro. apply propproperty.
intro. apply impred_isaprop.
intro. apply impred_isaprop.
intro. apply impred_isaprop.
intro. apply propproperty.
Local Proposition morphism_extensionality { a b : Δ } (f g : a --> b) :
(∏ x, (# U f) x = (# U g) x) -> f = g.
Show proof.
intro ext_hypothesis.
simpl in ext_hypothesis. apply U_faithful. simpl.
apply fincard_hom_extensionality. intro x. apply maponpaths. exact (ext_hypothesis x).
simpl in ext_hypothesis. apply U_faithful. simpl.
apply fincard_hom_extensionality. intro x. apply maponpaths. exact (ext_hypothesis x).
Lemma mon_iso_mon_inv {n m : Δ} {f : n --> m} (I : is_z_isomorphism ((# U) f)) :
∏ x y : (⟦m⟧)%stn, x ≤ y -> (is_z_isomorphism_mor I) x ≤ (is_z_isomorphism_mor I) y.
Show proof.
intros x y l.
unfold is_z_isomorphism in I. simpl in I.
induction I as [I_fn I_is_inverse_in_preord], f as [f_fn f_guarantee].
induction (natlehchoice x y l) as [a | a'].
- induction (natgthorleh (I_fn x) (I_fn y)).
+
contradiction (natlthtonegnatgeh x y a).
assert (∏ z , f_fn (I_fn z) = z) as X. {
intro z. change (f_fn (I_fn z)) with (compose (C:=Δ_sdg) I_fn f_fn z).
simpl. set (j := (pr2 I_is_inverse_in_preord)). simpl in j.
rewrite j. reflexivity.
}
rewrite <- (X x), <- (X y); apply f_guarantee. exact (natlthtoleh _ _ a0).
+ exact b.
- simpl is_z_isomorphism_mor. apply subtypeInjectivity_prop in a'.
induction a'. exact (isreflnatleh (I_fn x)).
unfold is_z_isomorphism in I. simpl in I.
induction I as [I_fn I_is_inverse_in_preord], f as [f_fn f_guarantee].
induction (natlehchoice x y l) as [a | a'].
- induction (natgthorleh (I_fn x) (I_fn y)).
+
contradiction (natlthtonegnatgeh x y a).
assert (∏ z , f_fn (I_fn z) = z) as X. {
intro z. change (f_fn (I_fn z)) with (compose (C:=Δ_sdg) I_fn f_fn z).
simpl. set (j := (pr2 I_is_inverse_in_preord)). simpl in j.
rewrite j. reflexivity.
}
rewrite <- (X x), <- (X y); apply f_guarantee. exact (natlthtoleh _ _ a0).
+ exact b.
- simpl is_z_isomorphism_mor. apply subtypeInjectivity_prop in a'.
induction a'. exact (isreflnatleh (I_fn x)).
Lemma fincard_inv_is_inverse_in_precat (n m : Δ) (f : n --> m ) (I : is_z_isomorphism ((# U) f)):
is_inverse_in_precat f (is_z_isomorphism_mor I,, mon_iso_mon_inv I).
Show proof.
unfold is_z_isomorphism in I. simpl in I.
induction I as [g is_inverse], f as [ffun fguarantee].
simpl in is_inverse. induction is_inverse as [l r].
split.
- apply morphism_extensionality. simpl. intro x.
change ((@compose precat_fincard _ _ _ ffun g) x = x). simpl. rewrite l. reflexivity.
- apply morphism_extensionality. intro x. simpl.
change (ffun (g x)) with (compose (C:=Δ_sdg) g ffun x).
simpl. rewrite r. unfold "id". reflexivity.
induction I as [g is_inverse], f as [ffun fguarantee].
simpl in is_inverse. induction is_inverse as [l r].
split.
- apply morphism_extensionality. simpl. intro x.
change ((@compose precat_fincard _ _ _ ffun g) x = x). simpl. rewrite l. reflexivity.
- apply morphism_extensionality. intro x. simpl.
change (ffun (g x)) with (compose (C:=Δ_sdg) g ffun x).
simpl. rewrite r. unfold "id". reflexivity.
Lemma U_reflects_isos (n m : Δ) ( f : n --> m ) : (is_z_isomorphism ((# U) f)) -> (is_z_isomorphism f).
Show proof.
intro I.
use tpair. { exact (is_z_isomorphism_mor I,, mon_iso_mon_inv I). }
cbv beta.
exact (fincard_inv_is_inverse_in_precat n m f I).
use tpair. { exact (is_z_isomorphism_mor I,, mon_iso_mon_inv I). }
cbv beta.
exact (fincard_inv_is_inverse_in_precat n m f I).
Local Proposition U_reflects_id (a : Δ) (f : a --> a) :
(# U f) = id (U a) -> f = id a.
Show proof.
Local Definition ordinal_addition : (Δ ⊠ Δ) → Δ.
Show proof.
Arguments ordinal_addition /.
Local Definition pr_n_m_l { n m : nat} ( x : (⟦ n + m⟧)%stn ) (s : x < n) : (⟦ n ⟧)%stn.
Show proof.
Local Definition pr_n_m_r { n m : nat} ( x : (⟦ n + m⟧)%stn ) (s : x ≥ n) : (⟦ m ⟧)%stn.
Show proof.
Local Definition sumfn {n n' m m' : nat} (f : (⟦ n ⟧)%stn → (⟦ m ⟧)%stn) ( g : (⟦ n' ⟧)%stn → (⟦ m' ⟧)%stn) : (⟦ n + n' ⟧)%stn → (⟦ m + m'⟧)%stn.
Show proof.
intro x.
induction (natlthorgeh x n) as [less_n | geq_n].
- set (x' := pr_n_m_l x less_n).
refine (ordconstr (n:=m+m') (stntonat _ (f x')) _).
apply (natgehgthtrans _ m _).
+ exact (natlehnplusnm m m').
+ exact (stnlt (f x')).
- set (x' := pr_n_m_r x geq_n).
refine (ordconstr (stntonat _ (g x')+m) _).
rewrite natpluscomm. apply natlthandplusl. exact (stnlt (g x')).
induction (natlthorgeh x n) as [less_n | geq_n].
- set (x' := pr_n_m_l x less_n).
refine (ordconstr (n:=m+m') (stntonat _ (f x')) _).
apply (natgehgthtrans _ m _).
+ exact (natlehnplusnm m m').
+ exact (stnlt (f x')).
- set (x' := pr_n_m_r x geq_n).
refine (ordconstr (stntonat _ (g x')+m) _).
rewrite natpluscomm. apply natlthandplusl. exact (stnlt (g x')).
Local Proposition pr_n_m_l_compute { n m : nat}
( x : (⟦ n + m⟧)%stn ) (s : x < n) : stntonat _ (pr_n_m_l x s) = stntonat _ x.
Show proof.
reflexivity.
Local Proposition pr_n_m_r_compute { n m : nat}
( x : (⟦ n + m⟧)%stn ) (s : x ≥ n) : stntonat _ (pr_n_m_r x s) = (stntonat _ x) - n.
Show proof.
reflexivity.
Local Proposition proj_incl_l { n m : nat } ( x : (⟦ n + m⟧)%stn ) (s : x < n) :
(stn_left n m) (pr_n_m_l x s) = x.
Show proof.
Local Proposition proj_incl_r { n m : nat } ( x : (⟦ n + m⟧)%stn ) (s : x ≥ n) :
(stn_right n m) (pr_n_m_r x s) = x.
Show proof.
unfold stn_right. simpl.
apply subtypeInjectivity_prop.
simpl.
rewrite natpluscomm. exact (minusplusnmm x n s).
apply subtypeInjectivity_prop.
simpl.
rewrite natpluscomm. exact (minusplusnmm x n s).
Definition natlthorgeh_left_branch {n m : nat} (s : n < m) (j : (n < m) ⨿ (n ≥ m)) : j = inl s
:= (proofirrelevancecontr (iscontr_inequal m n) j (inl s)).
Definition natlthorgeh_right_branch {n m : nat} (s : n ≥ m) (j : (n < m) ⨿ (n ≥ m)) : j = inr s
:= (proofirrelevancecontr (iscontr_inequal m n) j (inr s)).
Local Proposition sumfn_l { n n' m m' : nat}
(f : (⟦ n ⟧)%stn -> (⟦ m ⟧)%stn) ( g : (⟦ n' ⟧)%stn -> (⟦ m' ⟧)%stn)
(x : (⟦ n + n' ⟧)%stn) ( s : x < n) : (sumfn f g) x < m.
Show proof.
Local Proposition sumfn_r { n n' m m' : nat }
(f : (⟦ n ⟧)%stn -> (⟦ m ⟧)%stn) (g : (⟦ n' ⟧)%stn -> (⟦ m' ⟧)%stn)
(x : (⟦ n + n' ⟧)%stn) ( s : x ≥ n) : (sumfn f g) x ≥ m.
Show proof.
unfold sumfn. rewrite (natlthorgeh_right_branch s _).
simpl. change (g (pr_n_m_r x s) + m ≥ m). exact (natlehmplusnm _ m).
simpl. change (g (pr_n_m_r x s) + m ≥ m). exact (natlehmplusnm _ m).
Local Proposition sumfn_l1 { n n' m m' : nat}
(f : (⟦ n ⟧)%stn -> (⟦ m ⟧)%stn) ( g : (⟦ n' ⟧)%stn -> (⟦ m' ⟧)%stn)
(x : (⟦ n + n' ⟧)%stn) ( s : x < n) :
f (pr_n_m_l x s) = pr_n_m_l ((sumfn f g) x) (sumfn_l f g x s).
Show proof.
apply subtypeInjectivity_prop.
simpl. unfold sumfn. rewrite (natlthorgeh_left_branch s _).
simpl. reflexivity.
simpl. unfold sumfn. rewrite (natlthorgeh_left_branch s _).
simpl. reflexivity.
Local Proposition sumfn_r1 { n n' m m' : nat}
(f : (⟦ n ⟧)%stn -> (⟦ m ⟧)%stn) (g : (⟦ n' ⟧)%stn -> (⟦ m' ⟧)%stn)
(x : (⟦ n + n' ⟧)%stn) ( s :x ≥ n) :
g (pr_n_m_r x s) = pr_n_m_r ((sumfn f g) x) (sumfn_r f g x s).
Show proof.
apply subtypeInjectivity_prop.
simpl. unfold sumfn. rewrite (natlthorgeh_right_branch s _).
simpl. rewrite ( plusminusnmm _ m). reflexivity.
simpl. unfold sumfn. rewrite (natlthorgeh_right_branch s _).
simpl. rewrite ( plusminusnmm _ m). reflexivity.
Local Proposition sumfn_l2 { n n' m m' : nat}
(f : (⟦ n ⟧)%stn -> (⟦ m ⟧)%stn) ( g : (⟦ n' ⟧)%stn -> (⟦ m' ⟧)%stn)
(x : (⟦ n + n' ⟧)%stn) ( s : x < n) :
(stn_left m m') (f (pr_n_m_l x s)) = (sumfn f g) x.
Show proof.
Local Proposition sumfn_r2 { n n' m m' : nat}
(f : (⟦ n ⟧)%stn -> (⟦ m ⟧)%stn) ( g : (⟦ n' ⟧)%stn -> (⟦ m' ⟧)%stn)
(x : (⟦ n + n' ⟧)%stn) ( s : x ≥ n) :
(stn_right m m') (g (pr_n_m_r x s)) = (sumfn f g) x.
Show proof.
Local Proposition stn_left_monotonic ( n m : nat ) :
∏ x y : (⟦ n ⟧)%stn, (x ≤ y) -> ( stn_left n m x ) ≤ ( stn_left n m y).
Show proof.
intros x y l.
exact l.
exact l.
Local Proposition stn_right_monotonic ( n m : nat ) :
∏ x y : (⟦ m ⟧)%stn, (x ≤ y) -> ( stn_right n m x ) ≤ ( stn_right n m y).
Show proof.
intros x y l. simpl.
change (n + x ≤ n + y).
rewrite natpluscomm. rewrite (natpluscomm n y). apply natlehandplusr.
exact l.
change (n + x ≤ n + y).
rewrite natpluscomm. rewrite (natpluscomm n y). apply natlehandplusr.
exact l.
Definition monfunmonprop { n m : nat } (f : monfunstn n m) := pr2 f.
Local Arguments precategory_binproduct_mor /.
Local Definition ordinal_hom :
∏ a b : ob (Δ ⊠ Δ), a --> b -> (ordinal_addition a) --> (ordinal_addition b).
Show proof.
simpl. intros nn' mm'. induction nn' as [n n'], mm' as [m m'].
intro fg. simpl in fg. induction fg as [f g].
unshelve refine (make_monfunstn _ _).
- exact (sumfn f g).
- intros x y.
induction f as [f_fun f_guarantee]. induction g as [g_fun g_guarantee].
intro l. simpl. change (sumfn f_fun g_fun x ≤ sumfn f_fun g_fun y).
unfold sumfn.
induction natlthorgeh as [xl | xgth], (natlthorgeh y n) as [yl | ygth].
+ simpl. exact (f_guarantee (pr_n_m_l x xl) (pr_n_m_l y yl) l).
+ simpl. apply natlthtoleh. apply (natgehgthtrans _ m _ ).
* exact (natlehmplusnm _ m).
* exact (stnlt (f_fun _)).
+ contradiction (natgthnegleh yl). exact (istransnatleh xgth l).
+ simpl. change (g_fun (pr_n_m_r x xgth) + m ≤ g_fun (pr_n_m_r y ygth) +m ).
apply natlehandplusr. apply g_guarantee. rewrite pr_n_m_r_compute.
rewrite pr_n_m_r_compute. exact (natgehandminusr _ _ n l).
intro fg. simpl in fg. induction fg as [f g].
unshelve refine (make_monfunstn _ _).
- exact (sumfn f g).
- intros x y.
induction f as [f_fun f_guarantee]. induction g as [g_fun g_guarantee].
intro l. simpl. change (sumfn f_fun g_fun x ≤ sumfn f_fun g_fun y).
unfold sumfn.
induction natlthorgeh as [xl | xgth], (natlthorgeh y n) as [yl | ygth].
+ simpl. exact (f_guarantee (pr_n_m_l x xl) (pr_n_m_l y yl) l).
+ simpl. apply natlthtoleh. apply (natgehgthtrans _ m _ ).
* exact (natlehmplusnm _ m).
* exact (stnlt (f_fun _)).
+ contradiction (natgthnegleh yl). exact (istransnatleh xgth l).
+ simpl. change (g_fun (pr_n_m_r x xgth) + m ≤ g_fun (pr_n_m_r y ygth) +m ).
apply natlehandplusr. apply g_guarantee. rewrite pr_n_m_r_compute.
rewrite pr_n_m_r_compute. exact (natgehandminusr _ _ n l).
Local Definition tensor_data_card : (functor_data (Δ_sdg ⊠ Δ_sdg) Δ_sdg).
Show proof.
use functor_data_constr.
+ exact ordinal_addition.
+ intros a b pr. induction pr as [f g]. exact (sumfn f g).
+ exact ordinal_addition.
+ intros a b pr. induction pr as [f g]. exact (sumfn f g).
Local Definition tensor_data_ord : (functor_data (Δ ⊠ Δ) Δ).
Show proof.
Local Proposition tensor_id_card : (functor_idax tensor_data_card).
Show proof.
intro a. induction a as [n m]. simpl. unfold sumfn. apply fincard_hom_extensionality.
intro x.
induction natlthorgeh.
- simpl. unfold "id". reflexivity.
- simpl. unfold "id". simpl. exact (minusplusnmm x n b).
intro x.
induction natlthorgeh.
- simpl. unfold "id". reflexivity.
- simpl. unfold "id". simpl. exact (minusplusnmm x n b).
Local Proposition tensor_id_ord : (functor_idax tensor_data_ord).
Show proof.
Local Proposition tensor_comp_card : (functor_compax tensor_data_card).
Show proof.
unfold functor_compax. unfold tensor_data_card. simpl.
intros a b c f g.
induction a as [a0 a1], b as [b0 b1], c as [c0 c1].
simpl in f, g. induction f as [f0 f1], g as [g0 g1].
apply fincard_hom_extensionality. simpl. intro x.
unfold "·". simpl. unfold sumfn.
induction natlthorgeh.
- rewrite (natlthorgeh_left_branch (stnlt (f0 (ordconstr x a) )) _). simpl in *.
apply maponpaths. apply maponpaths.
apply subtypeInjectivity_prop.
reflexivity.
- rewrite (natlthorgeh_right_branch (natgehplusnmm _ b0) _). simpl in *.
apply (maponpaths (λ k : nat, k+c0)). apply maponpaths. apply maponpaths.
apply subtypeInjectivity_prop.
simpl. exact (pathsinv0 (plusminusnmm _ b0)).
intros a b c f g.
induction a as [a0 a1], b as [b0 b1], c as [c0 c1].
simpl in f, g. induction f as [f0 f1], g as [g0 g1].
apply fincard_hom_extensionality. simpl. intro x.
unfold "·". simpl. unfold sumfn.
induction natlthorgeh.
- rewrite (natlthorgeh_left_branch (stnlt (f0 (ordconstr x a) )) _). simpl in *.
apply maponpaths. apply maponpaths.
apply subtypeInjectivity_prop.
reflexivity.
- rewrite (natlthorgeh_right_branch (natgehplusnmm _ b0) _). simpl in *.
apply (maponpaths (λ k : nat, k+c0)). apply maponpaths. apply maponpaths.
apply subtypeInjectivity_prop.
simpl. exact (pathsinv0 (plusminusnmm _ b0)).
Local Proposition tensor_comp_ord : (functor_compax tensor_data_ord).
Show proof.
unfold functor_compax, tensor_data_ord. intros a b c f g.
induction f as [f0 f1], g as [g0 g1].
set (Uf := make_dirprod (# U f0) (# U f1)).
set (Ug := make_dirprod (# U g0) (# U g1)).
apply U_faithful. exact (tensor_comp_card a b c Uf Ug).
induction f as [f0 f1], g as [g0 g1].
set (Uf := make_dirprod (# U f0) (# U f1)).
set (Ug := make_dirprod (# U g0) (# U g1)).
apply U_faithful. exact (tensor_comp_card a b c Uf Ug).
Local Proposition tensor_card_is_functor : is_functor tensor_data_card.
Show proof.
Local Proposition tensor_ord_is_functor : is_functor tensor_data_ord.
Show proof.
Local Definition tensor_functor_card : functor (Δ_sdg ⊠ Δ_sdg) Δ_sdg.
Show proof.
Local Definition tensor_functor_ord : functor (Δ ⊠ Δ) Δ.
Show proof.
Local Definition tensor_unit : Δ :=0.
Arguments tensor_unit /.
Local Definition tensor_left_unitor_card : left_unitor tensor_functor_card tensor_unit.
Show proof.
unfold left_unitor, I_pretensor, functor_fix_fst_arg,functor_identity,nat_z_iso.
use tpair.
- unfold "⟹". use tpair.
+ unfold nat_trans_data. intro x. exact (id x).
+ abstract (cbv beta;
unfold is_nat_trans; intros n m f;
apply fincard_hom_extensionality;
simpl; unfold functor_fix_fst_arg_ob, tensor_functor_card;
simpl; intro x;
simpl; rewrite natplusr0; apply maponpaths, maponpaths, subtypeInjectivity_prop; simpl;
exact (natminuseqn x)).
- cbv beta. unfold is_nat_z_iso, is_z_isomorphism, is_inverse_in_precat.
intro c. exists (id c).
abstract ( split; unfold tensor_functor_card, functor_fix_fst_arg_ob, tensor_data_card;
simpl; exact (id_left (id c)); exact (id_left (id c))).
use tpair.
- unfold "⟹". use tpair.
+ unfold nat_trans_data. intro x. exact (id x).
+ abstract (cbv beta;
unfold is_nat_trans; intros n m f;
apply fincard_hom_extensionality;
simpl; unfold functor_fix_fst_arg_ob, tensor_functor_card;
simpl; intro x;
simpl; rewrite natplusr0; apply maponpaths, maponpaths, subtypeInjectivity_prop; simpl;
exact (natminuseqn x)).
- cbv beta. unfold is_nat_z_iso, is_z_isomorphism, is_inverse_in_precat.
intro c. exists (id c).
abstract ( split; unfold tensor_functor_card, functor_fix_fst_arg_ob, tensor_data_card;
simpl; exact (id_left (id c)); exact (id_left (id c))).
Local Definition tensor_left_unitor_ord : left_unitor tensor_functor_ord tensor_unit.
Show proof.
unfold left_unitor, I_pretensor, functor_fix_fst_arg,functor_identity,nat_z_iso.
use tpair.
- unfold "⟹". use tpair.
+ unfold nat_trans_data. intro n. exact (id n).
+ abstract (cbv beta;
unfold is_nat_trans; intros n m f; apply morphism_extensionality;
unfold tensor_functor_ord; simpl;
unfold functor_fix_fst_arg_ob, sumfn; simpl;
intro x;
apply subtypeInjectivity_prop;
simpl; rewrite natplusr0;
apply maponpaths, maponpaths, subtypeInjectivity_prop; simpl; exact (natminuseqn x)).
- cbv beta;
unfold is_nat_z_iso; intro c; unfold is_z_isomorphism.
exists (id c). abstract (simpl; unfold is_inverse_in_precat;
split;
unfold tensor_functor_ord, functor_fix_fst_arg_ob, tensor_data_ord; simpl;
exact (id_left (id c))).
use tpair.
- unfold "⟹". use tpair.
+ unfold nat_trans_data. intro n. exact (id n).
+ abstract (cbv beta;
unfold is_nat_trans; intros n m f; apply morphism_extensionality;
unfold tensor_functor_ord; simpl;
unfold functor_fix_fst_arg_ob, sumfn; simpl;
intro x;
apply subtypeInjectivity_prop;
simpl; rewrite natplusr0;
apply maponpaths, maponpaths, subtypeInjectivity_prop; simpl; exact (natminuseqn x)).
- cbv beta;
unfold is_nat_z_iso; intro c; unfold is_z_isomorphism.
exists (id c). abstract (simpl; unfold is_inverse_in_precat;
split;
unfold tensor_functor_ord, functor_fix_fst_arg_ob, tensor_data_ord; simpl;
exact (id_left (id c))).
Local Definition tensor_right_unitor_card_nt_data : nat_trans_data (I_posttensor tensor_functor_card tensor_unit) (functor_identity Δ_sdg).
Show proof.
simpl. unfold "⟹". unfold nat_trans_data. simpl. intro x.
unfold functor_fix_snd_arg_ob, tensor_functor_card, tensor_unit. simpl.
rewrite natplusr0. exact (idfun _).
unfold functor_fix_snd_arg_ob, tensor_functor_card, tensor_unit. simpl.
rewrite natplusr0. exact (idfun _).
Local Definition tensor_right_unitor_card_is_nat_trans : is_nat_trans (I_posttensor tensor_functor_card tensor_unit) (functor_identity Δ_sdg) tensor_right_unitor_card_nt_data.
Show proof.
unfold is_nat_trans, tensor_right_unitor_card_nt_data. simpl.
intros n m f. unfold functor_fix_snd_arg_mor; simpl.
apply fincard_hom_extensionality; unfold functor_fix_snd_arg_ob; simpl.
intro x.
unfold "·"; simpl. unfold sumfn.
assert (x < n) as j. { simpl; induction (natplusr0 n); exact (stnlt x). }
rewrite (natlthorgeh_left_branch j _). simpl.
generalize (natgehgthtrans (m+0) m), (! natplusr0 m). intros h p.
intermediate_path (pr1 (f (ordconstr x j))).
- induction (natplusr0 m). reflexivity.
- apply maponpaths, maponpaths, subtypeInjectivity_prop;
simpl; induction (natplusr0 n); reflexivity.
intros n m f. unfold functor_fix_snd_arg_mor; simpl.
apply fincard_hom_extensionality; unfold functor_fix_snd_arg_ob; simpl.
intro x.
unfold "·"; simpl. unfold sumfn.
assert (x < n) as j. { simpl; induction (natplusr0 n); exact (stnlt x). }
rewrite (natlthorgeh_left_branch j _). simpl.
generalize (natgehgthtrans (m+0) m), (! natplusr0 m). intros h p.
intermediate_path (pr1 (f (ordconstr x j))).
- induction (natplusr0 m). reflexivity.
- apply maponpaths, maponpaths, subtypeInjectivity_prop;
simpl; induction (natplusr0 n); reflexivity.
Local Definition tensor_right_unitor_card : right_unitor tensor_functor_card tensor_unit.
Show proof.
use tpair. { exact (tensor_right_unitor_card_nt_data,,tensor_right_unitor_card_is_nat_trans). }
cbv beta.
unfold is_nat_z_iso, is_z_isomorphism. simpl. intro c.
use tpair.
+ simpl. unfold functor_fix_snd_arg_ob, tensor_functor_card. simpl.
rewrite natplusr0. exact (idfun _).
+ abstract(cbv beta;
unfold is_inverse_in_precat, tensor_right_unitor_card_nt_data;
split;
induction (natplusr0 c); unfold functor_fix_snd_arg_ob, tensor_functor_card;
simpl; exact (id_left (id Δ_sdg_ob_constr (c + 0)));
induction (natplusr0 c); simpl; exact (id_left (id Δ_sdg_ob_constr (c + 0)))).
cbv beta.
unfold is_nat_z_iso, is_z_isomorphism. simpl. intro c.
use tpair.
+ simpl. unfold functor_fix_snd_arg_ob, tensor_functor_card. simpl.
rewrite natplusr0. exact (idfun _).
+ abstract(cbv beta;
unfold is_inverse_in_precat, tensor_right_unitor_card_nt_data;
split;
induction (natplusr0 c); unfold functor_fix_snd_arg_ob, tensor_functor_card;
simpl; exact (id_left (id Δ_sdg_ob_constr (c + 0)));
induction (natplusr0 c); simpl; exact (id_left (id Δ_sdg_ob_constr (c + 0)))).
Local Definition tensor_right_unitor_ord_nt_data : nat_trans_data (I_posttensor tensor_functor_ord tensor_unit) (functor_identity Δ_sd).
Show proof.
unfold nat_trans_data. intro n. use make_monfunstn.
* simpl. unfold functor_fix_snd_arg_ob, tensor_functor_ord.
simpl. rewrite natplusr0. exact (idfun _).
* cbv beta. intros x y leq. induction (natplusr0 n). exact leq.
* simpl. unfold functor_fix_snd_arg_ob, tensor_functor_ord.
simpl. rewrite natplusr0. exact (idfun _).
* cbv beta. intros x y leq. induction (natplusr0 n). exact leq.
Arguments tensor_right_unitor_ord_nt_data /.
Local Definition tensor_right_unitor_ord_is_nat_trans : is_nat_trans (I_posttensor tensor_functor_ord tensor_unit) (functor_identity Δ_sd) tensor_right_unitor_ord_nt_data.
Show proof.
unfold is_nat_trans. intros n m f.
apply U_faithful. rewrite (functor_comp U). simpl.
unfold "·". simpl.
apply fincard_hom_extensionality.
unfold functor_fix_snd_arg_ob, tensor_functor_ord. simpl.
induction (natplusr0 m). simpl. intro x.
unfold sumfn.
assert (x < n) as xbd. { simpl in *. induction (pathsinv0 (natplusr0 n)). exact (stnlt x). }
rewrite (natlthorgeh_left_branch xbd _). simpl.
apply maponpaths. apply maponpaths. apply subtypeInjectivity_prop.
induction (natplusr0 n). simpl. reflexivity.
apply U_faithful. rewrite (functor_comp U). simpl.
unfold "·". simpl.
apply fincard_hom_extensionality.
unfold functor_fix_snd_arg_ob, tensor_functor_ord. simpl.
induction (natplusr0 m). simpl. intro x.
unfold sumfn.
assert (x < n) as xbd. { simpl in *. induction (pathsinv0 (natplusr0 n)). exact (stnlt x). }
rewrite (natlthorgeh_left_branch xbd _). simpl.
apply maponpaths. apply maponpaths. apply subtypeInjectivity_prop.
induction (natplusr0 n). simpl. reflexivity.
Local Proposition tensor_right_unitor_ord : right_unitor tensor_functor_ord tensor_unit.
Show proof.
unfold right_unitor.
use tpair. { exact (tensor_right_unitor_ord_nt_data,,tensor_right_unitor_ord_is_nat_trans). }
cbv beta. unfold is_nat_z_iso. simpl. intro c. unfold is_z_isomorphism.
use tpair. { simpl. unfold functor_fix_snd_arg_ob. simpl.
rewrite natplusr0. exact (monfunstnid c). }
{
abstract(cbv beta; unfold tensor_right_unitor_ord_nt_data;
split;
unfold functor_fix_snd_arg_ob; simpl;
induction (natplusr0 c); simpl; reflexivity;
induction (natplusr0 c); reflexivity).
}
use tpair. { exact (tensor_right_unitor_ord_nt_data,,tensor_right_unitor_ord_is_nat_trans). }
cbv beta. unfold is_nat_z_iso. simpl. intro c. unfold is_z_isomorphism.
use tpair. { simpl. unfold functor_fix_snd_arg_ob. simpl.
rewrite natplusr0. exact (monfunstnid c). }
{
abstract(cbv beta; unfold tensor_right_unitor_ord_nt_data;
split;
unfold functor_fix_snd_arg_ob; simpl;
induction (natplusr0 c); simpl; reflexivity;
induction (natplusr0 c); reflexivity).
}
Definition tensor_associator_card_nat_trans_data : nat_trans_data (assoc_left tensor_functor_card) (assoc_right tensor_functor_card).
Show proof.
unfold nat_trans_data. simpl. induction x as [nm k], nm as [n m].
simpl. rewrite natplusassoc. exact (idfun _).
simpl. rewrite natplusassoc. exact (idfun _).
Arguments tensor_associator_card_nat_trans_data /.
Definition tensor_associator_card_is_nat_trans : is_nat_trans _ _ tensor_associator_card_nat_trans_data.
Show proof.
unfold is_nat_trans. simpl.
induction x as [nm k], nm as [n m], x' as [n'm' k'], n'm' as [n' m'].
simpl. induction f as [fg h], fg as [f g].
unfold "·". simpl.
apply fincard_hom_extensionality. simpl.
induction x as [xval xbd].
simpl. induction (natplusassoc n' m' k'). simpl.
unfold sumfn. simpl.
set (QQ := internal_paths_rew_r nat (n + m + k ) (n + (m + k )) _ _ _).
assert (xval < n + (m + k)) as xbd'. { rewrite (pathsinv0 (natplusassoc n m k)). exact xbd. }
assert ((QQ (xval,, xbd)) = (xval,, xbd')) as j.
{ apply subtypeInjectivity_prop. induction (natplusassoc n m k). reflexivity. }
simpl in j. rewrite j.
induction (natlthorgeh _ _) as [INDXLN | INDXGTN].
+ simpl.
assert (xval < (n + m)) as leq by exact (natgehgthtrans _ n _ (natlehnplusnm n m) INDXLN).
rewrite (natlthorgeh_left_branch leq _). simpl.
reflexivity.
+ simpl. induction (natlthorgeh _ _) as [XNLM | XNGTM].
* simpl.
assert ((xval - n) < m) as SS by exact (nat_split XNLM INDXGTN).
rewrite (natlthorgeh_left_branch SS _). simpl.
apply (maponpaths (λ k, k + n')), maponpaths, maponpaths, subtypeInjectivity_prop.
reflexivity.
* simpl. assert (xval - n ≥ m) as SS.
{ rewrite (pathsinv0 (plusminusnmm m n)).
apply natgehandminusr. rewrite natpluscomm. exact XNGTM.
}
rewrite (natlthorgeh_right_branch SS _). simpl.
rewrite natplusassoc, (natpluscomm n' m').
apply (maponpaths (λ k, k + (m' + n'))), maponpaths, maponpaths, subtypeInjectivity_prop.
simpl. rewrite natminusminus. reflexivity.
induction x as [nm k], nm as [n m], x' as [n'm' k'], n'm' as [n' m'].
simpl. induction f as [fg h], fg as [f g].
unfold "·". simpl.
apply fincard_hom_extensionality. simpl.
induction x as [xval xbd].
simpl. induction (natplusassoc n' m' k'). simpl.
unfold sumfn. simpl.
set (QQ := internal_paths_rew_r nat (n + m + k ) (n + (m + k )) _ _ _).
assert (xval < n + (m + k)) as xbd'. { rewrite (pathsinv0 (natplusassoc n m k)). exact xbd. }
assert ((QQ (xval,, xbd)) = (xval,, xbd')) as j.
{ apply subtypeInjectivity_prop. induction (natplusassoc n m k). reflexivity. }
simpl in j. rewrite j.
induction (natlthorgeh _ _) as [INDXLN | INDXGTN].
+ simpl.
assert (xval < (n + m)) as leq by exact (natgehgthtrans _ n _ (natlehnplusnm n m) INDXLN).
rewrite (natlthorgeh_left_branch leq _). simpl.
reflexivity.
+ simpl. induction (natlthorgeh _ _) as [XNLM | XNGTM].
* simpl.
assert ((xval - n) < m) as SS by exact (nat_split XNLM INDXGTN).
rewrite (natlthorgeh_left_branch SS _). simpl.
apply (maponpaths (λ k, k + n')), maponpaths, maponpaths, subtypeInjectivity_prop.
reflexivity.
* simpl. assert (xval - n ≥ m) as SS.
{ rewrite (pathsinv0 (plusminusnmm m n)).
apply natgehandminusr. rewrite natpluscomm. exact XNGTM.
}
rewrite (natlthorgeh_right_branch SS _). simpl.
rewrite natplusassoc, (natpluscomm n' m').
apply (maponpaths (λ k, k + (m' + n'))), maponpaths, maponpaths, subtypeInjectivity_prop.
simpl. rewrite natminusminus. reflexivity.
Definition tensor_associator_card_nat_trans : nat_trans (assoc_left tensor_functor_card) (assoc_right tensor_functor_card)
:= (tensor_associator_card_nat_trans_data,,tensor_associator_card_is_nat_trans).
Definition tensor_associator_ord_nat_trans_data :
nat_trans_data (assoc_left tensor_functor_ord) (assoc_right tensor_functor_ord).
Show proof.
unfold nat_trans_data. intro x. induction x as [nm k], nm as [n m].
unfold tensor_functor_ord. simpl.
rewrite natplusassoc. exact (monfunstnid _).
unfold tensor_functor_ord. simpl.
rewrite natplusassoc. exact (monfunstnid _).
Arguments tensor_associator_ord_nat_trans_data /.
Definition tensor_associator_ord_is_nat_trans : is_nat_trans _ _ tensor_associator_ord_nat_trans_data.
Show proof.
cbv beta. unfold is_nat_trans, tensor_associator_ord_nat_trans_data. simpl.
intros nmk n'm'k' fgh. induction nmk as [nm k], nm as [n m].
induction n'm'k' as [n'm' k'], n'm' as [n' m'].
induction fgh as [fg h], fg as [f g].
simpl in *. apply U_faithful. unfold U. simpl.
apply fincard_hom_extensionality. intro x. simpl.
induction (natplusassoc n' m' k'). simpl.
unfold sumfn. simpl.
set (QQ := internal_paths_rew_r nat (n + m + k ) (n + (m + k )) _ _ _).
simpl in QQ.
assert (x < n + (m + k)) as xbd'.
{ rewrite (pathsinv0 (natplusassoc n m k)). exact (stnlt x). }
set (x' := ordconstr (stntonat _ x) xbd').
assert (QQ x =x') as RW.
{ apply subtypeInjectivity_prop. induction (natplusassoc n m k). reflexivity. }
rewrite RW. simpl.
induction (natlthorgeh x n).
+ simpl. assert (x < (n + m)) as l.
{ apply (natgehgthtrans _ n _ ).
* rewrite natpluscomm. exact (natlehmplusnm m n).
* exact a.
}
rewrite (natlthorgeh_left_branch l _). simpl.
apply maponpaths. apply maponpaths. apply subtypeInjectivity_prop. reflexivity.
+ simpl. induction x as [xval xbd]. simpl.
induction (natlthorgeh (xval - n) m).
* simpl. assert ( xval < n + m) as l. {
rewrite (pathsinv0 (minusplusnmm xval n b)). rewrite (natpluscomm n m).
exact (natlthandplusr _ _ n a).
} simpl.
rewrite (natlthorgeh_left_branch l _). simpl. apply (maponpaths (λ k, k + n')).
apply maponpaths. apply maponpaths. apply subtypeInjectivity_prop. reflexivity.
* simpl. assert (xval ≥ n + m) as geq. {
rewrite (pathsinv0 (minusplusnmm xval n b)). rewrite (natpluscomm n m).
exact (natlehandplusr _ _ _ b0).
}
rewrite (natlthorgeh_right_branch geq _). simpl. rewrite (natpluscomm n' m').
rewrite natplusassoc. apply (maponpaths (λ k, k + (m'+n'))).
apply maponpaths. apply maponpaths. apply subtypeInjectivity_prop. simpl.
exact (pathsinv0 (natminusminus _ _ _)).
intros nmk n'm'k' fgh. induction nmk as [nm k], nm as [n m].
induction n'm'k' as [n'm' k'], n'm' as [n' m'].
induction fgh as [fg h], fg as [f g].
simpl in *. apply U_faithful. unfold U. simpl.
apply fincard_hom_extensionality. intro x. simpl.
induction (natplusassoc n' m' k'). simpl.
unfold sumfn. simpl.
set (QQ := internal_paths_rew_r nat (n + m + k ) (n + (m + k )) _ _ _).
simpl in QQ.
assert (x < n + (m + k)) as xbd'.
{ rewrite (pathsinv0 (natplusassoc n m k)). exact (stnlt x). }
set (x' := ordconstr (stntonat _ x) xbd').
assert (QQ x =x') as RW.
{ apply subtypeInjectivity_prop. induction (natplusassoc n m k). reflexivity. }
rewrite RW. simpl.
induction (natlthorgeh x n).
+ simpl. assert (x < (n + m)) as l.
{ apply (natgehgthtrans _ n _ ).
* rewrite natpluscomm. exact (natlehmplusnm m n).
* exact a.
}
rewrite (natlthorgeh_left_branch l _). simpl.
apply maponpaths. apply maponpaths. apply subtypeInjectivity_prop. reflexivity.
+ simpl. induction x as [xval xbd]. simpl.
induction (natlthorgeh (xval - n) m).
* simpl. assert ( xval < n + m) as l. {
rewrite (pathsinv0 (minusplusnmm xval n b)). rewrite (natpluscomm n m).
exact (natlthandplusr _ _ n a).
} simpl.
rewrite (natlthorgeh_left_branch l _). simpl. apply (maponpaths (λ k, k + n')).
apply maponpaths. apply maponpaths. apply subtypeInjectivity_prop. reflexivity.
* simpl. assert (xval ≥ n + m) as geq. {
rewrite (pathsinv0 (minusplusnmm xval n b)). rewrite (natpluscomm n m).
exact (natlehandplusr _ _ _ b0).
}
rewrite (natlthorgeh_right_branch geq _). simpl. rewrite (natpluscomm n' m').
rewrite natplusassoc. apply (maponpaths (λ k, k + (m'+n'))).
apply maponpaths. apply maponpaths. apply subtypeInjectivity_prop. simpl.
exact (pathsinv0 (natminusminus _ _ _)).
Definition tensor_associator_ord_nat_trans :
nat_trans (assoc_left tensor_functor_ord) (assoc_right tensor_functor_ord):=
(tensor_associator_ord_nat_trans_data,, tensor_associator_ord_is_nat_trans).
Definition tensor_associator_card : associator tensor_functor_card.
Show proof.
unfold associator, nat_z_iso, is_nat_z_iso.
exists tensor_associator_card_nat_trans.
induction c as [nm k], nm as [n m].
unfold is_z_isomorphism.
use tpair.
- simpl.
rewrite natplusassoc. exact (monfunstnid _).
- abstract(cbv beta;
unfold is_inverse_in_precat;
split;
simpl; unfold tensor_associator_card_nat_trans_data; simpl;
induction (natplusassoc n m k); simpl;
apply fincard_hom_extensionality; reflexivity;
simpl; unfold tensor_associator_card_nat_trans_data;
induction (pathsinv0 (natplusassoc n m k));
simpl; induction (natplusassoc n m k); simpl; apply fincard_hom_extensionality;
reflexivity).
exists tensor_associator_card_nat_trans.
induction c as [nm k], nm as [n m].
unfold is_z_isomorphism.
use tpair.
- simpl.
rewrite natplusassoc. exact (monfunstnid _).
- abstract(cbv beta;
unfold is_inverse_in_precat;
split;
simpl; unfold tensor_associator_card_nat_trans_data; simpl;
induction (natplusassoc n m k); simpl;
apply fincard_hom_extensionality; reflexivity;
simpl; unfold tensor_associator_card_nat_trans_data;
induction (pathsinv0 (natplusassoc n m k));
simpl; induction (natplusassoc n m k); simpl; apply fincard_hom_extensionality;
reflexivity).
Definition tensor_associator_ord : associator tensor_functor_ord.
unfold associator, nat_z_iso.
exists tensor_associator_ord_nat_trans.
unfold is_nat_z_iso.
intro c. induction c as [nm k]. induction nm as [n m].
unfold is_z_isomorphism.
use tpair. {
simpl. rewrite natplusassoc. exact (monfunstnid _).
}
{ abstract(cbv beta;
unfold is_inverse_in_precat, tensor_associator_ord_nat_trans,
tensor_associator_ord_nat_trans_data;
split;
simpl; induction (natplusassoc n m k); simpl;
apply morphism_extensionality; reflexivity;
simpl; induction (pathsinv0 (natplusassoc n m k));
simpl; induction (natplusassoc n m k); simpl; apply morphism_extensionality;
reflexivity).
}
Defined.
Proposition triangle_eq_holds_card : triangle_eq tensor_functor_card tensor_unit tensor_left_unitor_card tensor_right_unitor_card tensor_associator_card.
Show proof.
unfold triangle_eq. simpl. intros a b. apply fincard_hom_extensionality.
unfold tensor_functor_card, functor_fix_snd_arg_ob,
tensor_right_unitor_card_nt_data, tensor_associator_card_nat_trans_data.
simpl.
intro x. induction x as [xval xbd].
unfold sumfn. simpl.
set (QJ := internal_paths_rew_r nat (a + 0 + b) _ _ _ _ ). simpl in QJ.
assert (xval < a + b) as XLAB'. { rewrite (pathsinv0 (natplusr0 a)). exact xbd. }
set (x' := ordconstr xval XLAB'). unfold "·". simpl.
assert ((QJ (xval,, xbd)) = x') as RW.
{ apply subtypeInjectivity_prop. simpl in *. unfold QJ. generalize (natplusassoc a 0 b).
simpl. generalize (a + b). induction p. reflexivity.
} simpl in *. rewrite RW.
induction (natlthorgeh xval _) as [XLA | XGA].
- simpl. assert (xval < a) as XLA'. { rewrite (natplusr0 a) in XLA. exact XLA. }
rewrite (natlthorgeh_left_branch XLA' _). simpl in *. induction (natplusr0 a). reflexivity.
- simpl. assert (xval ≥ a) as XGA'. { rewrite (natplusr0 a) in XGA. exact XGA. }
rewrite (natlthorgeh_right_branch XGA' _). simpl in *. rewrite (natplusr0 a). reflexivity.
unfold tensor_functor_card, functor_fix_snd_arg_ob,
tensor_right_unitor_card_nt_data, tensor_associator_card_nat_trans_data.
simpl.
intro x. induction x as [xval xbd].
unfold sumfn. simpl.
set (QJ := internal_paths_rew_r nat (a + 0 + b) _ _ _ _ ). simpl in QJ.
assert (xval < a + b) as XLAB'. { rewrite (pathsinv0 (natplusr0 a)). exact xbd. }
set (x' := ordconstr xval XLAB'). unfold "·". simpl.
assert ((QJ (xval,, xbd)) = x') as RW.
{ apply subtypeInjectivity_prop. simpl in *. unfold QJ. generalize (natplusassoc a 0 b).
simpl. generalize (a + b). induction p. reflexivity.
} simpl in *. rewrite RW.
induction (natlthorgeh xval _) as [XLA | XGA].
- simpl. assert (xval < a) as XLA'. { rewrite (natplusr0 a) in XLA. exact XLA. }
rewrite (natlthorgeh_left_branch XLA' _). simpl in *. induction (natplusr0 a). reflexivity.
- simpl. assert (xval ≥ a) as XGA'. { rewrite (natplusr0 a) in XGA. exact XGA. }
rewrite (natlthorgeh_right_branch XGA' _). simpl in *. rewrite (natplusr0 a). reflexivity.
Proposition triangle_eq_holds_ord : triangle_eq tensor_functor_ord tensor_unit tensor_left_unitor_ord tensor_right_unitor_ord tensor_associator_ord.
Show proof.
unfold triangle_eq. simpl. intros a b. apply morphism_extensionality.
unfold tensor_functor_ord, functor_fix_snd_arg_ob. simpl.
unfold tensor_associator_ord_nat_trans_data. simpl.
intro x. induction x as [xval xbd].
unfold sumfn. simpl.
set (QJ := internal_paths_rew_r nat (a + 0 + b) _ _ _ _ ). simpl in QJ.
assert (xval < a + b) as XLAB'. { rewrite (pathsinv0 (natplusr0 a)). exact xbd. }
set (x' := ordconstr xval XLAB'). unfold "·". simpl.
assert ((QJ (xval,, xbd)) = x') as RW.
{ apply subtypeInjectivity_prop. simpl in *. unfold QJ. generalize (natplusassoc a 0 b).
simpl. generalize (a + b). induction p. reflexivity.
} simpl in *. rewrite RW.
apply subtypeInjectivity_prop.
induction (natlthorgeh xval _) as [XLA | XGA].
- simpl. assert (xval < a) as XLA'. { rewrite (natplusr0 a) in XLA. exact XLA. }
rewrite (natlthorgeh_left_branch XLA' _). simpl in *.
induction (natplusr0 a). reflexivity.
- simpl. assert (xval ≥ a) as XGA'. { rewrite (natplusr0 a) in XGA. exact XGA. }
rewrite (natlthorgeh_right_branch XGA' _). simpl in *. rewrite (natplusr0 a). reflexivity.
unfold tensor_functor_ord, functor_fix_snd_arg_ob. simpl.
unfold tensor_associator_ord_nat_trans_data. simpl.
intro x. induction x as [xval xbd].
unfold sumfn. simpl.
set (QJ := internal_paths_rew_r nat (a + 0 + b) _ _ _ _ ). simpl in QJ.
assert (xval < a + b) as XLAB'. { rewrite (pathsinv0 (natplusr0 a)). exact xbd. }
set (x' := ordconstr xval XLAB'). unfold "·". simpl.
assert ((QJ (xval,, xbd)) = x') as RW.
{ apply subtypeInjectivity_prop. simpl in *. unfold QJ. generalize (natplusassoc a 0 b).
simpl. generalize (a + b). induction p. reflexivity.
} simpl in *. rewrite RW.
apply subtypeInjectivity_prop.
induction (natlthorgeh xval _) as [XLA | XGA].
- simpl. assert (xval < a) as XLA'. { rewrite (natplusr0 a) in XLA. exact XLA. }
rewrite (natlthorgeh_left_branch XLA' _). simpl in *.
induction (natplusr0 a). reflexivity.
- simpl. assert (xval ≥ a) as XGA'. { rewrite (natplusr0 a) in XGA. exact XGA. }
rewrite (natlthorgeh_right_branch XGA' _). simpl in *. rewrite (natplusr0 a). reflexivity.
Proposition pentagon_eq_holds_card : pentagon_eq tensor_functor_card tensor_associator_card.
Show proof.
unfold pentagon_eq. intros. apply fincard_hom_extensionality. simpl.
unfold tensor_associator_card_nat_trans_data. simpl.
intro x. induction (natplusassoc b c d). simpl.
induction (natplusassoc a b (c + d)). simpl.
unfold "·". simpl.
induction (natplusassoc (a + b) c d). simpl.
unfold "id". simpl. set (k:=(tensor_id_card (make_dirprod a (b + c + d)))).
unfold "id" in k. simpl in k. simpl.
unfold "id" in k. simpl in k. unfold Δ_sdg_ob_constr. rewrite k.
induction (natplusassoc a (b + c) d), (natplusassoc a b c). simpl.
set (k':=(tensor_id_card (make_dirprod (a + b + c) d))).
unfold "id" in k'. simpl in k'.
unfold "id" in k'. simpl in k'. rewrite k'. reflexivity.
unfold tensor_associator_card_nat_trans_data. simpl.
intro x. induction (natplusassoc b c d). simpl.
induction (natplusassoc a b (c + d)). simpl.
unfold "·". simpl.
induction (natplusassoc (a + b) c d). simpl.
unfold "id". simpl. set (k:=(tensor_id_card (make_dirprod a (b + c + d)))).
unfold "id" in k. simpl in k. simpl.
unfold "id" in k. simpl in k. unfold Δ_sdg_ob_constr. rewrite k.
induction (natplusassoc a (b + c) d), (natplusassoc a b c). simpl.
set (k':=(tensor_id_card (make_dirprod (a + b + c) d))).
unfold "id" in k'. simpl in k'.
unfold "id" in k'. simpl in k'. rewrite k'. reflexivity.
Proposition pentagon_eq_holds_ord : pentagon_eq tensor_functor_ord tensor_associator_ord.
Show proof.
unfold pentagon_eq.
intros. apply U_faithful. rewrite (functor_comp U), (functor_comp U), (functor_comp U).
apply fincard_hom_extensionality.
unfold tensor_associator_ord. simpl.
unfold tensor_associator_ord_nat_trans_data. simpl.
intro x. induction (natplusassoc b c d), (natplusassoc a b (c + d)).
unfold "·". simpl.
induction (natplusassoc (a + b) c d).
set (j:= (tensor_id_card (make_dirprod a (b + c + d)))).
unfold tensor_data_card in j. simpl in j. unfold "id" in j. simpl in j.
unfold idfun. simpl. unfold idfun in j. rewrite j. induction (natplusassoc a (b + c) d).
simpl.
induction (natplusassoc a b c). simpl.
set (j' := (tensor_id_card (make_dirprod (a + b + c) d))).
unfold tensor_data_card in j'. simpl in j'.
simpl in j'. unfold "id" in j'. simpl in j'. unfold idfun in *. rewrite j'.
reflexivity.
intros. apply U_faithful. rewrite (functor_comp U), (functor_comp U), (functor_comp U).
apply fincard_hom_extensionality.
unfold tensor_associator_ord. simpl.
unfold tensor_associator_ord_nat_trans_data. simpl.
intro x. induction (natplusassoc b c d), (natplusassoc a b (c + d)).
unfold "·". simpl.
induction (natplusassoc (a + b) c d).
set (j:= (tensor_id_card (make_dirprod a (b + c + d)))).
unfold tensor_data_card in j. simpl in j. unfold "id" in j. simpl in j.
unfold idfun. simpl. unfold idfun in j. rewrite j. induction (natplusassoc a (b + c) d).
simpl.
induction (natplusassoc a b c). simpl.
set (j' := (tensor_id_card (make_dirprod (a + b + c) d))).
unfold tensor_data_card in j'. simpl in j'.
simpl in j'. unfold "id" in j'. simpl in j'. unfold idfun in *. rewrite j'.
reflexivity.
Definition AugmentedSimplexCategory : monoidal_cat.
Show proof.
use make_monoidal_cat.
+ exact Δ.
+ exact tensor_functor_ord.
+ exact tensor_unit.
+ exact tensor_left_unitor_ord.
+ exact tensor_right_unitor_ord.
+ exact tensor_associator_ord.
+ exact triangle_eq_holds_ord.
+ exact pentagon_eq_holds_ord.
+ exact Δ.
+ exact tensor_functor_ord.
+ exact tensor_unit.
+ exact tensor_left_unitor_ord.
+ exact tensor_right_unitor_ord.
+ exact tensor_associator_ord.
+ exact triangle_eq_holds_ord.
+ exact pentagon_eq_holds_ord.
Definition FinCard : monoidal_cat.
Show proof.
use make_monoidal_cat.
+ exact Δ_sdg.
+ exact tensor_functor_card.
+ exact tensor_unit.
+ exact tensor_left_unitor_card.
+ exact tensor_right_unitor_card.
+ exact tensor_associator_card.
+ exact triangle_eq_holds_card.
+ exact pentagon_eq_holds_card.
+ exact Δ_sdg.
+ exact tensor_functor_card.
+ exact tensor_unit.
+ exact tensor_left_unitor_card.
+ exact tensor_right_unitor_card.
+ exact tensor_associator_card.
+ exact triangle_eq_holds_card.
+ exact pentagon_eq_holds_card.
Definition U_ε : (monoidal_cat_unit FinCard) --> U (monoidal_cat_unit AugmentedSimplexCategory).
Show proof.
Definition U_μ : monoidal_functor_map AugmentedSimplexCategory FinCard U.
Show proof.
unfold monoidal_functor_map. simpl.
unfold "⟹". use tpair.
- unfold nat_trans_data. unfold precategory_binproduct_data.
simpl. simpl. intro x. induction x as [n m].
simpl. exact (idfun (⟦ n + m ⟧)%stn).
- abstract(cbv beta;
unfold is_nat_trans; simpl; intros x x'; induction x as [n m], x' as [n' m'];
unfold precategory_binproduct_mor; intro fg; simpl in fg; induction fg as [f g];
simpl;
set (s:= id_left (Δ_sdg_mor_constr (AugmentedSimplexCategory.sumfn (pr1 f) (pr1 g))));
unfold "id" in s; simpl in s; unfold Δ_sdg_mor_constr in s;
unfold Δ_sdg_ob_constr in s; unfold idfun;
simpl in s; simpl; induction f as [ffun fguarantee], g as [gfun gguarantee];
simpl in s; simpl; unfold "·"; unfold "·" in s; simpl in s; simpl;
unfold idfun in s; rewrite s; reflexivity).
unfold "⟹". use tpair.
- unfold nat_trans_data. unfold precategory_binproduct_data.
simpl. simpl. intro x. induction x as [n m].
simpl. exact (idfun (⟦ n + m ⟧)%stn).
- abstract(cbv beta;
unfold is_nat_trans; simpl; intros x x'; induction x as [n m], x' as [n' m'];
unfold precategory_binproduct_mor; intro fg; simpl in fg; induction fg as [f g];
simpl;
set (s:= id_left (Δ_sdg_mor_constr (AugmentedSimplexCategory.sumfn (pr1 f) (pr1 g))));
unfold "id" in s; simpl in s; unfold Δ_sdg_mor_constr in s;
unfold Δ_sdg_ob_constr in s; unfold idfun;
simpl in s; simpl; induction f as [ffun fguarantee], g as [gfun gguarantee];
simpl in s; simpl; unfold "·"; unfold "·" in s; simpl in s; simpl;
unfold idfun in s; rewrite s; reflexivity).
Definition U_α : monoidal_functor_associativity AugmentedSimplexCategory FinCard U U_μ.
Show proof.
unfold monoidal_functor_associativity.
intros x y z. simpl.
unfold MonoidalFunctorsTensored.α_D, MonoidalFunctorsTensored.α_C. simpl.
unfold monoidal_cat_associator. simpl.
change (idfun (⟦ x + y + z⟧)%stn) with (identity (C:=Δ_sdg) (x + y + z)).
change (idfun (⟦ x + y ⟧)%stn) with (identity (C:=Δ_sdg) (x + y)).
change (idfun (⟦ x + (y + z) ⟧)%stn) with (identity (C:=Δ_sdg) (x + (y+z))).
change (idfun (⟦ y + z ⟧)%stn) with (identity (C:=Δ_sdg) (y+z)).
set (j':= (tensor_id_card (make_dirprod (x + y) z))). simpl in *. rewrite j'.
set (j:= (tensor_id_card (make_dirprod x (y + z)))). simpl in *. rewrite j.
simpl in *.
rewrite (id_right (C:=Δ_sdg)), (id_right (C:=Δ_sdg)),
(id_right (C:=Δ_sdg)), (id_left (C:=Δ_sdg)).
apply fincard_hom_extensionality. intro t. cbn. unfold tensor_associator_ord_nat_trans_data, tensor_associator_card_nat_trans_data.
cbn.
induction (nat_rect _ _). reflexivity.
intros x y z. simpl.
unfold MonoidalFunctorsTensored.α_D, MonoidalFunctorsTensored.α_C. simpl.
unfold monoidal_cat_associator. simpl.
change (idfun (⟦ x + y + z⟧)%stn) with (identity (C:=Δ_sdg) (x + y + z)).
change (idfun (⟦ x + y ⟧)%stn) with (identity (C:=Δ_sdg) (x + y)).
change (idfun (⟦ x + (y + z) ⟧)%stn) with (identity (C:=Δ_sdg) (x + (y+z))).
change (idfun (⟦ y + z ⟧)%stn) with (identity (C:=Δ_sdg) (y+z)).
set (j':= (tensor_id_card (make_dirprod (x + y) z))). simpl in *. rewrite j'.
set (j:= (tensor_id_card (make_dirprod x (y + z)))). simpl in *. rewrite j.
simpl in *.
rewrite (id_right (C:=Δ_sdg)), (id_right (C:=Δ_sdg)),
(id_right (C:=Δ_sdg)), (id_left (C:=Δ_sdg)).
apply fincard_hom_extensionality. intro t. cbn. unfold tensor_associator_ord_nat_trans_data, tensor_associator_card_nat_trans_data.
cbn.
induction (nat_rect _ _). reflexivity.
Local Proposition U_unitality : monoidal_functor_unitality AugmentedSimplexCategory FinCard U U_ε U_μ.
Show proof.
unfold monoidal_functor_unitality.
simpl. intro x. unfold MonoidalFunctorsTensored.λ_D, monoidal_cat_left_unitor. simpl.
split.
- change (idfun (⟦x⟧)%stn) with (identity (C:=Δ_sdg) x).
rewrite (id_right (C:=Δ_sdg)), (id_right (C:=Δ_sdg)).
cbn. unfold U_ε, sumfn. simpl. apply funextsec. intro A. simpl.
apply subtypeInjectivity_prop. simpl. rewrite natminuseqn. rewrite natplusr0. reflexivity.
- change (idfun (⟦x⟧)%stn) with (identity (C:=Δ_sdg) x).
unfold MonoidalFunctorsTensored.I_C, monoidal_cat_unit. simpl.
rewrite (id_right (C:=Δ_sdg)). cbn.
unfold tensor_right_unitor_card_nt_data.
induction (natplusr0 x). simpl.
apply funextsec. intro y. simpl. unfold sumfn.
induction y as [yval ybd]. simpl.
assert (yval < x) as j. { rewrite (natplusr0 x) in ybd. exact ybd. }
rewrite (natlthorgeh_left_branch j _). simpl.
induction (! natplusr0 x). simpl. apply subtypeInjectivity_prop. reflexivity.
simpl. intro x. unfold MonoidalFunctorsTensored.λ_D, monoidal_cat_left_unitor. simpl.
split.
- change (idfun (⟦x⟧)%stn) with (identity (C:=Δ_sdg) x).
rewrite (id_right (C:=Δ_sdg)), (id_right (C:=Δ_sdg)).
cbn. unfold U_ε, sumfn. simpl. apply funextsec. intro A. simpl.
apply subtypeInjectivity_prop. simpl. rewrite natminuseqn. rewrite natplusr0. reflexivity.
- change (idfun (⟦x⟧)%stn) with (identity (C:=Δ_sdg) x).
unfold MonoidalFunctorsTensored.I_C, monoidal_cat_unit. simpl.
rewrite (id_right (C:=Δ_sdg)). cbn.
unfold tensor_right_unitor_card_nt_data.
induction (natplusr0 x). simpl.
apply funextsec. intro y. simpl. unfold sumfn.
induction y as [yval ybd]. simpl.
assert (yval < x) as j. { rewrite (natplusr0 x) in ybd. exact ybd. }
rewrite (natlthorgeh_left_branch j _). simpl.
induction (! natplusr0 x). simpl. apply subtypeInjectivity_prop. reflexivity.
Definition U_Mon_Lax : lax_monoidal_functor AugmentedSimplexCategory FinCard.
Show proof.
use make_lax_monoidal_functor.
+ exact U.
+ exact U_ε.
+ exact U_μ.
+ exact U_α.
+ exact U_unitality.
+ exact U.
+ exact U_ε.
+ exact U_μ.
+ exact U_α.
+ exact U_unitality.
Definition U_Mon_Strong : strong_monoidal_functor AugmentedSimplexCategory FinCard.
Show proof.
exists U_Mon_Lax. split.
- cbn. unfold is_z_isomorphism. use tpair.
+ simpl. exact (idfun (⟦ tensor_unit ⟧)%stn).
+ abstract(simpl; unfold is_inverse_in_precat; split;
unfold U_ε; exact (id_right (C:=Δ_sdg) (idfun _));
unfold U_ε; exact (id_right (C:=Δ_sdg) (idfun _))).
- unfold is_nat_z_iso. simpl. intro c. induction c as [n m].
unfold is_z_isomorphism. simpl. exists (idfun (⟦ n + m⟧)%stn).
abstract(unfold is_inverse_in_precat; split;
exact (id_right (C:=Δ_sdg) (idfun _));
exact (id_right (C:=Δ_sdg) (idfun _))).
- cbn. unfold is_z_isomorphism. use tpair.
+ simpl. exact (idfun (⟦ tensor_unit ⟧)%stn).
+ abstract(simpl; unfold is_inverse_in_precat; split;
unfold U_ε; exact (id_right (C:=Δ_sdg) (idfun _));
unfold U_ε; exact (id_right (C:=Δ_sdg) (idfun _))).
- unfold is_nat_z_iso. simpl. intro c. induction c as [n m].
unfold is_z_isomorphism. simpl. exists (idfun (⟦ n + m⟧)%stn).
abstract(unfold is_inverse_in_precat; split;
exact (id_right (C:=Δ_sdg) (idfun _));
exact (id_right (C:=Δ_sdg) (idfun _))).
Local Lemma functor_eq_to_object_eq_on_homs
(C D : precategory) (F G : functor C D) ( p : F = G) (c : C) (d : D) ( f : d --> G c) :
internal_paths_rew_r (C ⟶ D) F G (λ H : C ⟶ D, D ⟦ d , H c⟧) f p =
internal_paths_rew_r D (F c) (G c) (λ d' : D, D ⟦ d , d' ⟧) f
(maponpaths (λ H : C ⟶ D, H c) p).
Show proof.
induction p. reflexivity.
Local Proposition tensor_card_is_strict_left_iso_id :
∏ eq_λ : I_pretensor (monoidal_cat_tensor FinCard)
(monoidal_cat_unit FinCard) = functor_identity (pr1 FinCard),
(is_nat_z_iso_id eq_λ (monoidal_cat_left_unitor FinCard)).
Show proof.
intro eq_λ.
unfold is_nat_z_iso_id. intro c. unfold nat_comp_to_endo.
rewrite functor_eq_to_object_eq_on_homs. set (j := maponpaths _ _). simpl in j. simpl in c.
assert (j = idpath c) as RW by apply (setproperty natset); rewrite RW.
reflexivity.
unfold is_nat_z_iso_id. intro c. unfold nat_comp_to_endo.
rewrite functor_eq_to_object_eq_on_homs. set (j := maponpaths _ _). simpl in j. simpl in c.
assert (j = idpath c) as RW by apply (setproperty natset); rewrite RW.
reflexivity.
Local Arguments monoidal_cat_tensor /.
Local Arguments monoidal_cat_unit /.
Local Arguments functor_fix_fst_arg /.
Local Arguments functor_fix_snd_arg /.
Local Arguments functor_fix_fst_arg_ob /.
Local Arguments functor_fix_snd_arg_ob /.
Local Definition right_unitor_id (c : Δ_sdg) :
I_posttensor (monoidal_cat_tensor FinCard)
(monoidal_cat_unit FinCard) c = functor_identity (pr1 FinCard) c.
Show proof.
Local Proposition tensor_card_is_strict_right_iso_id : ∏ eq_ρ : I_posttensor (monoidal_cat_tensor FinCard)
(monoidal_cat_unit FinCard) = functor_identity (pr1 FinCard),
is_nat_z_iso_id eq_ρ (monoidal_cat_right_unitor FinCard).
Show proof.
unfold is_nat_z_iso_id. intros eq_ρ c. unfold nat_comp_to_endo.
set (Δ_sdg := (pr1 FinCard)).
set (Rtensor0 := (I_posttensor _ _)).
set (idfunctor := (functor_identity _)).
rewrite functor_eq_to_object_eq_on_homs. set (j := maponpaths _ _).
cbv beta in j.
assert (j = right_unitor_id c) as RW by apply (setproperty natset); rewrite RW.
unfold right_unitor_id, transportb. apply fincard_hom_extensionality.
intro x. unfold Rtensor0 in x. simpl in x.
simpl. unfold tensor_right_unitor_card_nt_data. simpl.
induction (natplusr0 c). simpl. reflexivity.
set (Δ_sdg := (pr1 FinCard)).
set (Rtensor0 := (I_posttensor _ _)).
set (idfunctor := (functor_identity _)).
rewrite functor_eq_to_object_eq_on_homs. set (j := maponpaths _ _).
cbv beta in j.
assert (j = right_unitor_id c) as RW by apply (setproperty natset); rewrite RW.
unfold right_unitor_id, transportb. apply fincard_hom_extensionality.
intro x. unfold Rtensor0 in x. simpl in x.
simpl. unfold tensor_right_unitor_card_nt_data. simpl.
induction (natplusr0 c). simpl. reflexivity.
Local Proposition tensor_card_is_strict_associator_id :
∏ eq_α : assoc_left tensor_functor_card = assoc_right tensor_functor_card,
is_nat_z_iso_id eq_α (monoidal_cat_associator FinCard).
Show proof.
unfold is_nat_z_iso_id. intro eq_α.
intro c. simpl in c. induction c as [nm k]. induction nm as [n m].
unfold nat_comp_to_endo. rewrite functor_eq_to_object_eq_on_homs.
unfold assoc_left. simpl.
set (j:= maponpaths _ _).
assert (j = (natplusassoc n m k)) as RW by apply (pr2 natset). rewrite RW.
simpl. generalize (natplusassoc n m k). induction p. simpl. reflexivity.
intro c. simpl in c. induction c as [nm k]. induction nm as [n m].
unfold nat_comp_to_endo. rewrite functor_eq_to_object_eq_on_homs.
unfold assoc_left. simpl.
set (j:= maponpaths _ _).
assert (j = (natplusassoc n m k)) as RW by apply (pr2 natset). rewrite RW.
simpl. generalize (natplusassoc n m k). induction p. simpl. reflexivity.
Definition FinCardStrict : strict_monoidal_cat.
Show proof.
use tpair. { exact FinCard. }
cbv beta. intros eq_λ eq_ρ eq_α.
use tpair. { exact (tensor_card_is_strict_left_iso_id eq_λ). }
cbv beta. split. { exact (tensor_card_is_strict_right_iso_id eq_ρ). }
exact (tensor_card_is_strict_associator_id eq_α).
cbv beta. intros eq_λ eq_ρ eq_α.
use tpair. { exact (tensor_card_is_strict_left_iso_id eq_λ). }
cbv beta. split. { exact (tensor_card_is_strict_right_iso_id eq_ρ). }
exact (tensor_card_is_strict_associator_id eq_α).
Local Proposition tensor_Δ_left_unitor_is_id :
∏ eq_λ : I_pretensor (monoidal_cat_tensor AugmentedSimplexCategory)
(monoidal_cat_unit AugmentedSimplexCategory) = functor_identity (pr1 AugmentedSimplexCategory), (is_nat_z_iso_id eq_λ (monoidal_cat_left_unitor AugmentedSimplexCategory)).
Show proof.
unfold is_nat_z_iso_id. intros eq_λ c.
unfold nat_comp_to_endo. set (Δ_sd := (pr1 FinCard)).
set (Ltensor0 := (I_pretensor _ _)).
set (idfunctor := (functor_identity _)).
rewrite functor_eq_to_object_eq_on_homs. set (j := maponpaths _ _).
unfold monoidal_cat_left_unitor. simpl pr1.
unfold tensor_left_unitor_ord. simpl.
unfold Ltensor0, idfunctor in j. simpl in j.
assert (j = idpath c) as RW by apply (setproperty natset). rewrite RW.
reflexivity.
unfold nat_comp_to_endo. set (Δ_sd := (pr1 FinCard)).
set (Ltensor0 := (I_pretensor _ _)).
set (idfunctor := (functor_identity _)).
rewrite functor_eq_to_object_eq_on_homs. set (j := maponpaths _ _).
unfold monoidal_cat_left_unitor. simpl pr1.
unfold tensor_left_unitor_ord. simpl.
unfold Ltensor0, idfunctor in j. simpl in j.
assert (j = idpath c) as RW by apply (setproperty natset). rewrite RW.
reflexivity.
Local Proposition tensor_Δ_right_unitor_is_id :
∏ eq_ρ : I_posttensor (monoidal_cat_tensor AugmentedSimplexCategory)
(monoidal_cat_unit AugmentedSimplexCategory) =
functor_identity (pr1 AugmentedSimplexCategory),
is_nat_z_iso_id eq_ρ (monoidal_cat_right_unitor AugmentedSimplexCategory).
Show proof.
unfold is_nat_z_iso_id. intro eq_ρ. intro c.
unfold nat_comp_to_endo.
set (Rtensor0 := (I_posttensor _ _)).
set (idfunctor := (functor_identity _)).
rewrite functor_eq_to_object_eq_on_homs. set (j := maponpaths _ _).
cbv beta in j.
assert (j = right_unitor_id c) as RW. { apply (setproperty natset). } rewrite RW.
simpl. unfold right_unitor_id. induction (natplusr0 c). simpl. reflexivity.
unfold nat_comp_to_endo.
set (Rtensor0 := (I_posttensor _ _)).
set (idfunctor := (functor_identity _)).
rewrite functor_eq_to_object_eq_on_homs. set (j := maponpaths _ _).
cbv beta in j.
assert (j = right_unitor_id c) as RW. { apply (setproperty natset). } rewrite RW.
simpl. unfold right_unitor_id. induction (natplusr0 c). simpl. reflexivity.
Local Proposition tensor_ord_is_strict_associator_id :
∏ eq_α : assoc_left tensor_functor_ord = assoc_right tensor_functor_ord,
is_nat_z_iso_id eq_α (monoidal_cat_associator AugmentedSimplexCategory).
Show proof.
unfold is_nat_z_iso_id. intro eq_α.
intro c. simpl in c. induction c as [nm k], nm as [n m].
unfold nat_comp_to_endo. rewrite functor_eq_to_object_eq_on_homs.
unfold assoc_left. simpl.
set (j:= maponpaths _ _).
assert (j = (natplusassoc n m k)) as RW by apply (setproperty natset); rewrite RW.
simpl. generalize (natplusassoc n m k). induction p. reflexivity.
intro c. simpl in c. induction c as [nm k], nm as [n m].
unfold nat_comp_to_endo. rewrite functor_eq_to_object_eq_on_homs.
unfold assoc_left. simpl.
set (j:= maponpaths _ _).
assert (j = (natplusassoc n m k)) as RW by apply (setproperty natset); rewrite RW.
simpl. generalize (natplusassoc n m k). induction p. reflexivity.
Definition FinOrdStrict : strict_monoidal_cat.
Show proof.
use tpair. { exact AugmentedSimplexCategory. }
cbv beta. intros eq_λ eq_ρ eq_α.
use tpair. { exact (tensor_Δ_left_unitor_is_id eq_λ). }
split. { exact (tensor_Δ_right_unitor_is_id eq_ρ). }
exact (tensor_ord_is_strict_associator_id eq_α).
cbv beta. intros eq_λ eq_ρ eq_α.
use tpair. { exact (tensor_Δ_left_unitor_is_id eq_λ). }
split. { exact (tensor_Δ_right_unitor_is_id eq_ρ). }
exact (tensor_ord_is_strict_associator_id eq_α).