Library UniMath.CategoryTheory.FunctorAlgebras
****************************************************************
Benedikt Ahrens
started March 2015
Extended by: Anders Mörtberg. October 2015
***************************************************************
Contents :
- Category of algebras of an endofunctor
- This category is saturated if base precategory is
- Lambek's lemma: if (A,a) is an inital F-algebra then a is an iso
- The natural numbers are initial for X ↦ 1 + X
Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.limits.initial.
Require Import UniMath.CategoryTheory.limits.terminal.
Require Import UniMath.CategoryTheory.limits.bincoproducts.
Require Import UniMath.CategoryTheory.NNO.
Local Open Scope cat.
Section Algebra_Definition.
Context {C : precategory} (F : functor C C).
Definition algebra_ob : UU := ∑ X : C, F X --> X.
Definition alg_carrier (X : algebra_ob) : C := pr1 X.
Local Coercion alg_carrier : algebra_ob >-> ob.
Definition alg_map (X : algebra_ob) : F X --> X := pr2 X.
A morphism of an F-algebras (F X, g : F X --> X) and (F Y, h : F Y --> Y)
is a morphism f : X --> Y such that the following diagram commutes:
F f
F x ----> F y
| |
| g | h
V V
x ------> y
f
Definition is_algebra_mor (X Y : algebra_ob) (f : alg_carrier X --> alg_carrier Y) : UU
:= alg_map X · f = #F f · alg_map Y.
Definition algebra_mor (X Y : algebra_ob) : UU :=
∑ f : X --> Y, is_algebra_mor X Y f.
Coercion mor_from_algebra_mor (X Y : algebra_ob) (f : algebra_mor X Y) : X --> Y := pr1 f.
Definition isaset_algebra_mor (hs : has_homsets C) (X Y : algebra_ob) : isaset (algebra_mor X Y).
Show proof.
Definition algebra_mor_eq (hs : has_homsets C) {X Y : algebra_ob} {f g : algebra_mor X Y}
: (f : X --> Y) = g ≃ f = g.
Show proof.
Lemma algebra_mor_commutes (X Y : algebra_ob) (f : algebra_mor X Y)
: alg_map X · f = #F f · alg_map Y.
Show proof.
Definition algebra_mor_id (X : algebra_ob) : algebra_mor X X.
Show proof.
Definition algebra_mor_comp (X Y Z : algebra_ob) (f : algebra_mor X Y) (g : algebra_mor Y Z)
: algebra_mor X Z.
Show proof.
Definition precategory_alg_ob_mor : precategory_ob_mor.
Show proof.
Definition precategory_alg_data : precategory_data.
Show proof.
Lemma is_precategory_precategory_alg_data (hs : has_homsets C)
: is_precategory precategory_alg_data.
Show proof.
Definition precategory_FunctorAlg (hs : has_homsets C)
: precategory := tpair _ _ (is_precategory_precategory_alg_data hs).
Local Notation FunctorAlg := precategory_FunctorAlg.
Lemma has_homsets_FunctorAlg (hs : has_homsets C)
: has_homsets (FunctorAlg hs).
Show proof.
:= alg_map X · f = #F f · alg_map Y.
Definition algebra_mor (X Y : algebra_ob) : UU :=
∑ f : X --> Y, is_algebra_mor X Y f.
Coercion mor_from_algebra_mor (X Y : algebra_ob) (f : algebra_mor X Y) : X --> Y := pr1 f.
Definition isaset_algebra_mor (hs : has_homsets C) (X Y : algebra_ob) : isaset (algebra_mor X Y).
Show proof.
apply (isofhleveltotal2 2).
- apply hs.
- intro f.
apply isasetaprop.
apply hs.
- apply hs.
- intro f.
apply isasetaprop.
apply hs.
Definition algebra_mor_eq (hs : has_homsets C) {X Y : algebra_ob} {f g : algebra_mor X Y}
: (f : X --> Y) = g ≃ f = g.
Show proof.
apply invweq.
apply subtypeInjectivity.
intro a. apply hs.
apply subtypeInjectivity.
intro a. apply hs.
Lemma algebra_mor_commutes (X Y : algebra_ob) (f : algebra_mor X Y)
: alg_map X · f = #F f · alg_map Y.
Show proof.
exact (pr2 f).
Definition algebra_mor_id (X : algebra_ob) : algebra_mor X X.
Show proof.
exists (identity _ ).
abstract (unfold is_algebra_mor;
rewrite id_right ;
rewrite functor_id;
rewrite id_left;
apply idpath).
abstract (unfold is_algebra_mor;
rewrite id_right ;
rewrite functor_id;
rewrite id_left;
apply idpath).
Definition algebra_mor_comp (X Y Z : algebra_ob) (f : algebra_mor X Y) (g : algebra_mor Y Z)
: algebra_mor X Z.
Show proof.
exists (f · g).
abstract (unfold is_algebra_mor;
rewrite assoc;
rewrite algebra_mor_commutes;
rewrite <- assoc;
rewrite algebra_mor_commutes;
rewrite functor_comp, assoc;
apply idpath).
abstract (unfold is_algebra_mor;
rewrite assoc;
rewrite algebra_mor_commutes;
rewrite <- assoc;
rewrite algebra_mor_commutes;
rewrite functor_comp, assoc;
apply idpath).
Definition precategory_alg_ob_mor : precategory_ob_mor.
Show proof.
exists algebra_ob.
exact algebra_mor.
exact algebra_mor.
Definition precategory_alg_data : precategory_data.
Show proof.
exists precategory_alg_ob_mor.
exists algebra_mor_id.
exact algebra_mor_comp.
exists algebra_mor_id.
exact algebra_mor_comp.
Lemma is_precategory_precategory_alg_data (hs : has_homsets C)
: is_precategory precategory_alg_data.
Show proof.
repeat split; intros; simpl.
- apply algebra_mor_eq.
+ apply hs.
+ apply id_left.
- apply algebra_mor_eq.
+ apply hs.
+ apply id_right.
- apply algebra_mor_eq.
+ apply hs.
+ apply assoc.
- apply algebra_mor_eq.
+ apply hs.
+ apply assoc'.
- apply algebra_mor_eq.
+ apply hs.
+ apply id_left.
- apply algebra_mor_eq.
+ apply hs.
+ apply id_right.
- apply algebra_mor_eq.
+ apply hs.
+ apply assoc.
- apply algebra_mor_eq.
+ apply hs.
+ apply assoc'.
Definition precategory_FunctorAlg (hs : has_homsets C)
: precategory := tpair _ _ (is_precategory_precategory_alg_data hs).
Local Notation FunctorAlg := precategory_FunctorAlg.
Lemma has_homsets_FunctorAlg (hs : has_homsets C)
: has_homsets (FunctorAlg hs).
Show proof.
intros f g.
apply isaset_algebra_mor.
assumption.
apply isaset_algebra_mor.
assumption.
forgetful functor from FunctorAlg to its underlying category
Definition forget_algebras_data (hsC: has_homsets C): functor_data (FunctorAlg hsC) C.
Show proof.
set (onobs := fun alg : FunctorAlg hsC => alg_carrier alg).
apply (mk_functor_data onobs).
intros alg1 alg2 m.
simpl in m.
exact (mor_from_algebra_mor _ _ m).
apply (mk_functor_data onobs).
intros alg1 alg2 m.
simpl in m.
exact (mor_from_algebra_mor _ _ m).
Definition forget_algebras (hsC: has_homsets C): functor (FunctorAlg hsC) C.
Show proof.
apply (mk_functor (forget_algebras_data hsC)).
red.
split; red.
- intro alg. apply idpath.
- intros alg1 alg2 alg3 m n. apply idpath.
red.
split; red.
- intro alg. apply idpath.
- intros alg1 alg2 alg3 m n. apply idpath.
Section FunctorAlg_saturated.
Hypothesis H : is_univalent C.
Definition algebra_eq_type (X Y : FunctorAlg (pr2 H)) : UU
:= ∑ p : iso (pr1 X) (pr1 Y), is_algebra_mor X Y p.
Definition algebra_ob_eq (X Y : FunctorAlg (pr2 H)) :
(X = Y) ≃ algebra_eq_type X Y.
Show proof.
eapply weqcomp.
- apply total2_paths_equiv.
- set (H1 := weqpair _ (pr1 H (pr1 X) (pr1 Y))).
apply (weqbandf H1).
simpl.
intro p.
destruct X as [X α].
destruct Y as [Y β]; simpl in *.
destruct p.
rewrite idpath_transportf.
unfold is_algebra_mor; simpl.
rewrite functor_id.
rewrite id_left, id_right.
apply idweq.
- apply total2_paths_equiv.
- set (H1 := weqpair _ (pr1 H (pr1 X) (pr1 Y))).
apply (weqbandf H1).
simpl.
intro p.
destruct X as [X α].
destruct Y as [Y β]; simpl in *.
destruct p.
rewrite idpath_transportf.
unfold is_algebra_mor; simpl.
rewrite functor_id.
rewrite id_left, id_right.
apply idweq.
Definition is_iso_from_is_algebra_iso (X Y : FunctorAlg (pr2 H)) (f : X --> Y)
: is_iso f → is_iso (pr1 f).
Show proof.
intro p.
apply is_iso_from_is_z_iso.
set (H' := iso_inv_after_iso (isopair f p)).
set (H'':= iso_after_iso_inv (isopair f p)).
exists (pr1 (inv_from_iso (isopair f p))).
split; simpl.
- apply (maponpaths pr1 H').
- apply (maponpaths pr1 H'').
apply is_iso_from_is_z_iso.
set (H' := iso_inv_after_iso (isopair f p)).
set (H'':= iso_after_iso_inv (isopair f p)).
exists (pr1 (inv_from_iso (isopair f p))).
split; simpl.
- apply (maponpaths pr1 H').
- apply (maponpaths pr1 H'').
Definition inv_algebra_mor_from_is_iso {X Y : FunctorAlg (pr2 H)} (f : X --> Y)
: is_iso (pr1 f) → (Y --> X).
Show proof.
intro T.
set (fiso:=isopair (pr1 f) T).
set (finv:=inv_from_iso fiso).
exists finv.
unfold finv.
apply pathsinv0.
apply iso_inv_on_left.
simpl.
rewrite functor_on_inv_from_iso.
rewrite <- assoc.
apply pathsinv0.
apply iso_inv_on_right.
simpl.
apply (pr2 f).
set (fiso:=isopair (pr1 f) T).
set (finv:=inv_from_iso fiso).
exists finv.
unfold finv.
apply pathsinv0.
apply iso_inv_on_left.
simpl.
rewrite functor_on_inv_from_iso.
rewrite <- assoc.
apply pathsinv0.
apply iso_inv_on_right.
simpl.
apply (pr2 f).
Definition is_algebra_iso_from_is_iso {X Y : FunctorAlg (pr2 H)} (f : X --> Y)
: is_iso (pr1 f) → is_iso f.
Show proof.
intro T.
apply is_iso_from_is_z_iso.
exists (inv_algebra_mor_from_is_iso f T).
split; simpl.
- apply algebra_mor_eq.
+ apply (pr2 H).
+ simpl.
apply (iso_inv_after_iso (isopair (pr1 f) T)).
- apply algebra_mor_eq.
+ apply (pr2 H).
+ apply (iso_after_iso_inv (isopair (pr1 f) T)).
apply is_iso_from_is_z_iso.
exists (inv_algebra_mor_from_is_iso f T).
split; simpl.
- apply algebra_mor_eq.
+ apply (pr2 H).
+ simpl.
apply (iso_inv_after_iso (isopair (pr1 f) T)).
- apply algebra_mor_eq.
+ apply (pr2 H).
+ apply (iso_after_iso_inv (isopair (pr1 f) T)).
Definition algebra_iso_first_iso {X Y : FunctorAlg (pr2 H)}
: iso X Y ≃ ∑ f : X --> Y, is_iso (pr1 f).
Show proof.
apply (weqbandf (idweq _ )).
unfold idweq. simpl.
intro f.
apply weqimplimpl.
- apply is_iso_from_is_algebra_iso.
- apply is_algebra_iso_from_is_iso.
- apply isaprop_is_iso.
- apply isaprop_is_iso.
unfold idweq. simpl.
intro f.
apply weqimplimpl.
- apply is_iso_from_is_algebra_iso.
- apply is_algebra_iso_from_is_iso.
- apply isaprop_is_iso.
- apply isaprop_is_iso.
Definition swap (A B : UU) : A × B → B × A.
Show proof.
intro ab.
exists (pr2 ab).
exact (pr1 ab).
exists (pr2 ab).
exact (pr1 ab).
Definition swapweq (A B : UU) : (A × B) ≃ (B × A).
Show proof.
exists (swap A B).
apply (isweq_iso _ (swap B A)).
- intro ab. destruct ab. apply idpath.
- intro ba. destruct ba. apply idpath.
apply (isweq_iso _ (swap B A)).
- intro ab. destruct ab. apply idpath.
- intro ba. destruct ba. apply idpath.
Definition algebra_iso_rearrange {X Y : FunctorAlg (pr2 H)}
: (∑ f : X --> Y, is_iso (pr1 f)) ≃ algebra_eq_type X Y.
Show proof.
eapply weqcomp.
- apply weqtotal2asstor.
- simpl. unfold algebra_eq_type.
apply invweq.
eapply weqcomp.
+ apply weqtotal2asstor.
+ simpl. apply (weqbandf (idweq _ )).
unfold idweq. simpl.
intro f; apply swapweq.
- apply weqtotal2asstor.
- simpl. unfold algebra_eq_type.
apply invweq.
eapply weqcomp.
+ apply weqtotal2asstor.
+ simpl. apply (weqbandf (idweq _ )).
unfold idweq. simpl.
intro f; apply swapweq.
Definition algebra_idtoiso (X Y : FunctorAlg (pr2 H)) :
(X = Y) ≃ iso X Y.
Show proof.
eapply weqcomp.
- apply algebra_ob_eq.
- eapply weqcomp.
+ apply (invweq (algebra_iso_rearrange)).
+ apply (invweq algebra_iso_first_iso).
- apply algebra_ob_eq.
- eapply weqcomp.
+ apply (invweq (algebra_iso_rearrange)).
+ apply (invweq algebra_iso_first_iso).
Lemma isweq_idtoiso_FunctorAlg (X Y : FunctorAlg (pr2 H))
: isweq (@idtoiso _ X Y).
Show proof.
apply (isweqhomot (algebra_idtoiso X Y)).
- intro p. induction p.
simpl. apply eq_iso. apply algebra_mor_eq.
+ apply (pr2 H).
+ apply idpath.
- apply (pr2 _ ).
- intro p. induction p.
simpl. apply eq_iso. apply algebra_mor_eq.
+ apply (pr2 H).
+ apply idpath.
- apply (pr2 _ ).
Lemma is_univalent_FunctorAlg : is_univalent (FunctorAlg (pr2 H)).
Show proof.
split.
- apply isweq_idtoiso_FunctorAlg.
- intros a b.
apply isaset_algebra_mor.
apply (pr2 H).
- apply isweq_idtoiso_FunctorAlg.
- intros a b.
apply isaset_algebra_mor.
apply (pr2 H).
End FunctorAlg_saturated.
Lemma idtomor_FunctorAlg_commutes (hsC: has_homsets C)(X Y: FunctorAlg hsC)(e: X = Y): mor_from_algebra_mor _ _ (idtomor _ _ e) = idtomor _ _ (maponpaths alg_carrier e).
Show proof.
induction e.
apply idpath.
apply idpath.
Corollary idtoiso_FunctorAlg_commutes (hsC: has_homsets C)(X Y: FunctorAlg hsC)(e: X = Y): mor_from_algebra_mor _ _ (morphism_from_iso _ _ _ (idtoiso e)) = idtoiso (maponpaths alg_carrier e).
Show proof.
unfold morphism_from_iso.
do 2 rewrite eq_idtoiso_idtomor.
apply idtomor_FunctorAlg_commutes.
do 2 rewrite eq_idtoiso_idtomor.
apply idtomor_FunctorAlg_commutes.
End Algebra_Definition.
Notation FunctorAlg := precategory_FunctorAlg.
Section Lambeks_lemma.
Variables (C : precategory) (hsC : has_homsets C) (F : functor C C).
Variables (Aa : algebra_ob F) (AaIsInitial : isInitial (FunctorAlg F hsC) Aa).
Local Definition AaInitial : Initial (FunctorAlg F hsC) :=
mk_Initial _ AaIsInitial.
Local Notation A := (alg_carrier _ Aa).
Local Notation a := (alg_map _ Aa).
Local Definition FAa : algebra_ob F := tpair (λ X, C ⟦F X,X⟧) (F A) (# F a).
Local Definition Fa' := InitialArrow AaInitial FAa.
Local Definition a' : C⟦A,F A⟧ := mor_from_algebra_mor _ _ _ Fa'.
Local Definition Ha' := algebra_mor_commutes _ _ _ Fa'.
Lemma initialAlg_is_iso_subproof : is_inverse_in_precat a a'.
Show proof.
assert (Ha'a : a' · a = identity A).
assert (algMor_a'a : is_algebra_mor _ _ _ (a' · a)).
unfold is_algebra_mor, a'; rewrite functor_comp.
eapply pathscomp0; [|eapply cancel_postcomposition; apply Ha'].
now apply assoc.
apply pathsinv0; set (X := tpair _ _ algMor_a'a).
now apply (maponpaths pr1 (!@InitialEndo_is_identity _ AaInitial X)).
split; simpl; trivial.
eapply pathscomp0; [apply Ha'|]; simpl.
rewrite <- functor_comp.
eapply pathscomp0; [eapply maponpaths; apply Ha'a|].
now apply functor_id.
assert (algMor_a'a : is_algebra_mor _ _ _ (a' · a)).
unfold is_algebra_mor, a'; rewrite functor_comp.
eapply pathscomp0; [|eapply cancel_postcomposition; apply Ha'].
now apply assoc.
apply pathsinv0; set (X := tpair _ _ algMor_a'a).
now apply (maponpaths pr1 (!@InitialEndo_is_identity _ AaInitial X)).
split; simpl; trivial.
eapply pathscomp0; [apply Ha'|]; simpl.
rewrite <- functor_comp.
eapply pathscomp0; [eapply maponpaths; apply Ha'a|].
now apply functor_id.
Lemma initialAlg_is_iso : is_iso a.
Show proof.
exact (is_iso_qinv _ a' initialAlg_is_iso_subproof).
End Lambeks_lemma.
The natural numbers are intial for X ↦ 1 + X
Section Nats.
Context (C : precategory).
Context (bc : BinCoproducts C).
Context (hsC : has_homsets C).
Context (T : Terminal C).
Local Notation "1" := T.
Local Notation "f + g" := (BinCoproductOfArrows _ _ _ f g).
Local Notation "[ f , g ]" := (BinCoproductArrow _ _ f g).
Let F : functor C C := BinCoproduct_of_functors _ _ bc
(constant_functor _ _ 1)
(functor_identity _).
F on objects: X ↦ 1 + X
Definition F_compute1 : ∏ c : C, F c = BinCoproductObject _ (bc 1 c) :=
fun c => (idpath _).
fun c => (idpath _).
Definition F_compute2 {x y : C} : ∏ f : x --> y, # F f = (identity 1) + f :=
fun c => (idpath _).
Definition nat_ob : UU := Initial (FunctorAlg F hsC).
Definition nat_ob_carrier (N : nat_ob) : ob C :=
alg_carrier _ (InitialObject N).
Local Coercion nat_ob_carrier : nat_ob >-> ob.
fun c => (idpath _).
Definition nat_ob : UU := Initial (FunctorAlg F hsC).
Definition nat_ob_carrier (N : nat_ob) : ob C :=
alg_carrier _ (InitialObject N).
Local Coercion nat_ob_carrier : nat_ob >-> ob.
We have an arrow alg_map : (F N = 1 + N) --> N,
so by the η-rule (UMP) for the coproduct, we can assume that it
arises from a pair of maps nat_ob_z,nat_ob_s by composing with
coproduct injections.
in1 in2
1 ----> 1 + N <---- N
| | |
nat_ob_z | | alg_map | nat_ob_s
| V |
+-------> N <-------+
Definition nat_ob_z (N : nat_ob) : (1 --> N) :=
BinCoproductIn1 C (bc 1 (alg_carrier F (pr1 N))) · (alg_map _ (pr1 N)).
Definition nat_ob_s (N : nat_ob) : (N --> N) :=
BinCoproductIn2 C (bc 1 (alg_carrier F (pr1 N))) · (alg_map _ (pr1 N)).
Local Notation "0" := (nat_ob_z _).
BinCoproductIn1 C (bc 1 (alg_carrier F (pr1 N))) · (alg_map _ (pr1 N)).
Definition nat_ob_s (N : nat_ob) : (N --> N) :=
BinCoproductIn2 C (bc 1 (alg_carrier F (pr1 N))) · (alg_map _ (pr1 N)).
Local Notation "0" := (nat_ob_z _).
Use the universal property of the coproduct to make any object with a
point and an endomorphism into an F-algebra
Definition mk_F_alg {X : ob C} (f : 1 --> X) (g : X --> X) : ob (FunctorAlg F hsC).
Show proof.
Show proof.
refine (X,, _).
exact (BinCoproductArrow _ _ f g).
exact (BinCoproductArrow _ _ f g).
Using mk_F_alg, X will be an F-algebra, and by initiality of N, there will
be a unique morphism of F-algebras N --> X, which can be projected to a
morphism in C.
Definition nat_ob_rec (N : nat_ob) {X : ob C} :
∏ (f : 1 --> X) (g : X --> X), (N --> X) :=
fun f g => mor_from_algebra_mor _ _ _ (InitialArrow N (mk_F_alg f g)).
∏ (f : 1 --> X) (g : X --> X), (N --> X) :=
fun f g => mor_from_algebra_mor _ _ _ (InitialArrow N (mk_F_alg f g)).
When calling the recursor on 0, you get the base case.
Specifically,
nat_ob_z · nat_ob_rec = f
Lemma nat_ob_rec_z (N : nat_ob) {X : ob C} :
∏ (f : 1 --> X) (g : X --> X), nat_ob_z N · nat_ob_rec N f g = f.
Show proof.
Opaque nat_ob_rec_z.
∏ (f : 1 --> X) (g : X --> X), nat_ob_z N · nat_ob_rec N f g = f.
Show proof.
intros f g.
pose (inlN := BinCoproductIn1 _ (bc 1 N)).
pose (succ := nat_ob_s N).
pose (inlN := BinCoproductIn1 _ (bc 1 N)).
pose (succ := nat_ob_s N).
By initiality of N, there is a unique morphism making the following
diagram commute:
inlN identity 1 + nat_ob_rec
1 -----> 1 + N -------------------------> 1 + X
| |
alg_map N | | alg_map X
V V
N --------------------------> X
nat_ob_rec
This proof uses somewhat idiosyncratic "forward reasoning", transforming
the term "diagram" rather than the goal.
pose
(diagram :=
maponpaths
(fun x => inlN · x)
(algebra_mor_commutes F (pr1 N) _ (InitialArrow N (mk_F_alg f g)))).
rewrite (F_compute2 _) in diagram.
(diagram :=
maponpaths
(fun x => inlN · x)
(algebra_mor_commutes F (pr1 N) _ (InitialArrow N (mk_F_alg f g)))).
rewrite (F_compute2 _) in diagram.
rewrite (BinCoproductArrowEta C 1 X (bc _ _) _ _) in diagram.
Using the β-rules for coproducts, we can simplify some of the terms (identity 1 + _) · f, g --β--> identity 1 · f, _ · g
rewrite (precompWithBinCoproductArrow C (bc 1 N) (bc 1 X)
(identity 1) _ _ _) in diagram.
(identity 1) _ _ _) in diagram.
rewrite (BinCoproductIn1Commutes C 1 N (bc 1 _) _ _ _) in diagram.
We can dispense with the identity
rewrite (id_left _) in diagram.
rewrite assoc in diagram.
rewrite (BinCoproductArrowEta C 1 N (bc _ _) _ _) in diagram.
refine (_ @ (BinCoproductIn1Commutes C _ _ (bc 1 _) _ f g)).
rewrite (!BinCoproductIn1Commutes C _ _ (bc 1 _) _ 0 succ).
unfold nat_ob_rec in *.
exact diagram.
rewrite assoc in diagram.
rewrite (BinCoproductArrowEta C 1 N (bc _ _) _ _) in diagram.
refine (_ @ (BinCoproductIn1Commutes C _ _ (bc 1 _) _ f g)).
rewrite (!BinCoproductIn1Commutes C _ _ (bc 1 _) _ 0 succ).
unfold nat_ob_rec in *.
exact diagram.
Opaque nat_ob_rec_z.
The succesor case:
nat_ob_s · nat_ob_rec = nat_ob_rec · g
The proof is very similar.
Lemma nat_ob_rec_s (N : nat_ob) {X : ob C} :
∏ (f : 1 --> X) (g : X --> X),
nat_ob_s N · nat_ob_rec N f g = nat_ob_rec N f g · g.
Show proof.
Opaque nat_ob_rec_s.
End Nats.
∏ (f : 1 --> X) (g : X --> X),
nat_ob_s N · nat_ob_rec N f g = nat_ob_rec N f g · g.
Show proof.
intros f g.
pose (inrN := BinCoproductIn2 _ (bc 1 N)).
pose (succ := nat_ob_s N).
pose (inrN := BinCoproductIn2 _ (bc 1 N)).
pose (succ := nat_ob_s N).
By initiality of N, there is a unique morphism making the same diagram
commute as above, but with "inrN" in place of "inlN".
pose
(diagram :=
maponpaths
(fun x => inrN · x)
(algebra_mor_commutes F (pr1 N) _ (InitialArrow N (mk_F_alg f g)))).
rewrite (F_compute2 _) in diagram.
rewrite (BinCoproductArrowEta C 1 X (bc _ _) _ _) in diagram.
(diagram :=
maponpaths
(fun x => inrN · x)
(algebra_mor_commutes F (pr1 N) _ (InitialArrow N (mk_F_alg f g)))).
rewrite (F_compute2 _) in diagram.
rewrite (BinCoproductArrowEta C 1 X (bc _ _) _ _) in diagram.
Using the β-rules for coproducts, we can simplify some of the terms (identity 1 + _) · f, g --β--> identity 1 · f, _ · g
rewrite (precompWithBinCoproductArrow C (bc 1 N) (bc 1 X)
(identity 1) _ _ _) in diagram.
(identity 1) _ _ _) in diagram.
rewrite (BinCoproductIn2Commutes C 1 N (bc 1 _) _ _ _) in diagram.
rewrite assoc in diagram.
rewrite (BinCoproductArrowEta C 1 N (bc _ _) _ _) in diagram.
refine
(_ @ maponpaths (fun x => nat_ob_rec N f g · x)
(BinCoproductIn2Commutes C _ _ (bc 1 _) _ f g)).
rewrite (!BinCoproductIn2Commutes C _ _ (bc 1 _) _ 0 (nat_ob_s N)).
unfold nat_ob_rec in *.
exact diagram.
rewrite assoc in diagram.
rewrite (BinCoproductArrowEta C 1 N (bc _ _) _ _) in diagram.
refine
(_ @ maponpaths (fun x => nat_ob_rec N f g · x)
(BinCoproductIn2Commutes C _ _ (bc 1 _) _ f g)).
rewrite (!BinCoproductIn2Commutes C _ _ (bc 1 _) _ 0 (nat_ob_s N)).
unfold nat_ob_rec in *.
exact diagram.
Opaque nat_ob_rec_s.
End Nats.
nat_ob implies NNO
Lemma nat_ob_NNO {C : precategory} (BC : BinCoproducts C) (hsC : has_homsets C) (TC : Terminal C) :
nat_ob C BC hsC TC → NNO TC.
Show proof.
nat_ob C BC hsC TC → NNO TC.
Show proof.
intros N.
use mk_NNO.
- exact (nat_ob_carrier _ _ _ _ N).
- apply nat_ob_z.
- apply nat_ob_s.
- intros n z s.
use unique_exists.
+ apply (nat_ob_rec _ _ _ _ _ z s).
+ split; [ apply nat_ob_rec_z | apply nat_ob_rec_s ].
+ intros x; apply isapropdirprod; apply hsC.
+ intros x [H1 H2].
transparent assert (xalg : (FunctorAlg (BinCoproduct_of_functors C C BC
(constant_functor C C TC)
(functor_identity C)) hsC
⟦ InitialObject N, mk_F_alg C BC hsC TC z s ⟧)).
{ refine (x,,_).
abstract (apply pathsinv0; etrans; [apply precompWithBinCoproductArrow |];
rewrite id_left, <- H1;
etrans; [eapply maponpaths, pathsinv0, H2|];
now apply pathsinv0, BinCoproductArrowUnique; rewrite assoc;
apply maponpaths).
}
exact (maponpaths pr1 (InitialArrowUnique N (mk_F_alg C BC hsC TC z s) xalg)).
use mk_NNO.
- exact (nat_ob_carrier _ _ _ _ N).
- apply nat_ob_z.
- apply nat_ob_s.
- intros n z s.
use unique_exists.
+ apply (nat_ob_rec _ _ _ _ _ z s).
+ split; [ apply nat_ob_rec_z | apply nat_ob_rec_s ].
+ intros x; apply isapropdirprod; apply hsC.
+ intros x [H1 H2].
transparent assert (xalg : (FunctorAlg (BinCoproduct_of_functors C C BC
(constant_functor C C TC)
(functor_identity C)) hsC
⟦ InitialObject N, mk_F_alg C BC hsC TC z s ⟧)).
{ refine (x,,_).
abstract (apply pathsinv0; etrans; [apply precompWithBinCoproductArrow |];
rewrite id_left, <- H1;
etrans; [eapply maponpaths, pathsinv0, H2|];
now apply pathsinv0, BinCoproductArrowUnique; rewrite assoc;
apply maponpaths).
}
exact (maponpaths pr1 (InitialArrowUnique N (mk_F_alg C BC hsC TC z s) xalg)).