Library UniMath.CategoryTheory.categories.HSET.Structures

Other structures in HSET

Contents

Written by: Benedikt Ahrens, Anders Mörtberg
October 2015 - January 2016

Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.

Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.MoreFoundations.AxiomOfChoice.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Adjunctions.Core.
Require Import UniMath.CategoryTheory.exponentials.
Require Import UniMath.CategoryTheory.slicecat.
Require Import UniMath.CategoryTheory.NNO.
Require Import UniMath.CategoryTheory.SubobjectClassifier.
Require Import UniMath.CategoryTheory.categories.Type.Core.
Require Import UniMath.CategoryTheory.categories.Type.MonoEpiIso.
Require Import UniMath.CategoryTheory.limits.binproducts.
Require Import UniMath.CategoryTheory.limits.coequalizers.
Require Import UniMath.CategoryTheory.limits.pullbacks.
Require Import UniMath.CategoryTheory.limits.terminal.
Require Import UniMath.CategoryTheory.covyoneda.
Require Import UniMath.CategoryTheory.EpiFacts.
Require Import UniMath.CategoryTheory.Monics.
Require Import UniMath.CategoryTheory.SplitMonicsAndEpis.
Require Import UniMath.CategoryTheory.ElementaryTopos.
Require Import UniMath.CategoryTheory.PowerObject.

Require Import UniMath.CategoryTheory.categories.HSET.Core.
Require Import UniMath.CategoryTheory.categories.HSET.Limits.
Require Import UniMath.CategoryTheory.categories.HSET.MonoEpiIso.
Require Import UniMath.CategoryTheory.categories.HSET.Univalence.

Local Open Scope cat.

Natural numbers object (NNO_HSET)


Lemma isNNO_nat : isNNO TerminalHSET natHSET (λ _, 0) S.
Show proof.
  intros X z s.
  use unique_exists.
  + intros n.
    induction n as [|_ n].
    * exact (z tt).
    * exact (s n).
  + now split; apply funextfun; intros [].
  + now intros; apply isapropdirprod; apply homset_property.
  + intros q [hq1 hq2].
    apply funextfun; intros n.
    induction n as [|n IH].
    * now rewrite <- hq1.
    * cbn in *; now rewrite (toforallpaths _ _ _ hq2 n), IH.

Definition NNO_HSET : NNO TerminalHSET.
Show proof.
  use make_NNO.
  - exact natHSET.
  - exact (λ _, 0).
  - exact S.
  - exact isNNO_nat.

Exponentials (Exponentials_HSET)


Section exponentials.

Define the functor: A -> _^A
Definition exponential_functor (A : HSET) : functor HSET HSET.
Show proof.
use make_functor.
+ exists (funset (A : hSet)); simpl.
  intros b c f g; apply (λ x, f (g x)).
+ abstract (use tpair;
  [ intro x; now (repeat apply funextfun; intro)
  | intros x y z f g; now (repeat apply funextfun; intro)]).

This checks that if we use constprod_functor2 the flip is not necessary
Lemma are_adjoints_constprod_functor2 A :
  are_adjoints (constprod_functor2 BinProductsHSET A) (exponential_functor A).
Show proof.
use tpair.
- use tpair.
  + use tpair.
    * intro x; simpl; apply make_dirprod.
    * abstract (intros x y f; apply idpath).
  + use tpair.
    * intros X fx; apply (pr1 fx (pr2 fx)).
    * abstract (intros x y f; apply idpath).
- abstract (use tpair;
  [ intro x; simpl; apply funextfun; intro ax; apply idpath
  | intro b; apply funextfun; intro f; apply idpath]).

Lemma Exponentials_HSET : Exponentials BinProductsHSET.
Show proof.
intro a.
exists (exponential_functor a).
use tpair.
- use tpair.
  + use tpair.
    * intro x; simpl; apply flip, make_dirprod.
    * abstract (intros x y f; apply idpath).
  + use tpair.
    * intros x xf; simpl in *; apply (pr2 xf (pr1 xf)).
    * abstract (intros x y f; apply idpath).
- abstract (use tpair;
  [ now intro x; simpl; apply funextfun; intro ax; apply idpath
  | now intro b; apply funextfun; intro f]).

End exponentials.

Construction of exponentials for functors into HSET

This section defines exponential in C,HSET following a slight variation of Moerdijk-MacLane (p. 46, Prop. 1).
The formula for C,Set is G^F(f)=Hom(Hom(f,−)×id(F),G) taken from:
http://mathoverflow.net/questions/104152/exponentials-in-functor-categories
Section exponentials_functor_cat.

Context (C : category).

Let CP := BinProducts_functor_precat C _ BinProductsHSET.
Let cy := covyoneda C.

Local Definition exponential_functor_cat (P Q : functor C HSET) : functor C HSET.
Show proof.
use tpair.
- use tpair.
  + intro c.
    use make_hSet.
    * apply (nat_trans (BinProduct_of_functors C _ BinProductsHSET (cy c) P) Q).
    * abstract (apply (isaset_nat_trans has_homsets_HSET)).
  + simpl; intros a b f alpha.
    apply (BinProductOfArrows _ (CP (cy a) P) (CP (cy b) P)
                           (# cy f) (identity _) · alpha).
- abstract (
    split;
      [ intros c; simpl; apply funextsec; intro a;
        apply (nat_trans_eq has_homsets_HSET); cbn; unfold prodtofuntoprod; intro x;
        apply funextsec; intro f;
        destruct f as [cx Px]; simpl; unfold covyoneda_morphisms_data;
        now rewrite id_left
      | intros a b c f g; simpl; apply funextsec; intro alpha;
        apply (nat_trans_eq has_homsets_HSET); cbn; unfold prodtofuntoprod; intro x;
        apply funextsec; intro h;
        destruct h as [cx pcx]; simpl; unfold covyoneda_morphisms_data;
        now rewrite assoc ]).

Local Definition eval (P Q : functor C HSET) :
  nat_trans (BinProductObject _ (CP P (exponential_functor_cat P Q)) : functor _ _) Q.
Show proof.
use tpair.
- intros c ytheta; set (y := pr1 ytheta); set (theta := pr2 ytheta);
  simpl in *.
  use (theta c).
  exact (identity c,,y).
- abstract (
    intros c c' f; simpl;
    apply funextfun; intros ytheta; destruct ytheta as [y theta];
    cbn; unfold prodtofuntoprod;
    unfold covyoneda_morphisms_data;
    assert (X := nat_trans_ax theta);
    assert (Y := toforallpaths _ _ _ (X c c' f) (identity c,, y));
    eapply pathscomp0; [|apply Y]; cbn; unfold prodtofuntoprod; cbn;
    now rewrite id_right, id_left).

Lemma Exponentials_functor_HSET : Exponentials CP.
Show proof.
intro P.
use left_adjoint_from_partial.
- apply (exponential_functor_cat P).
- intro Q; simpl; apply eval.
- intros Q R φ; simpl in *.
  use tpair.
  + use tpair.
    * { use make_nat_trans.
        - intros c u; simpl.
          use make_nat_trans.
          + simpl; intros d fx.
            apply (φ d (make_dirprod (pr2 fx) (# R (pr1 fx) u))).
          + intros a b f; simpl; cbn; unfold prodtofuntoprod.
            apply funextsec; intro x.
            etrans;
              [|apply (toforallpaths _ _ _ (nat_trans_ax φ _ _ f)
                                     (make_dirprod (pr2 x) (# R (pr1 x) u)))]; cbn.
              repeat (apply maponpaths).
              assert (H : # R (pr1 x · f) = # R (pr1 x) · #R f).
              { apply functor_comp. }
              unfold prodtofuntoprod.
              simpl (pr1 _); simpl (pr2 _).
              apply maponpaths.
              apply (eqtohomot H u).
        - intros a b f; cbn.
          apply funextsec; intros x; cbn.
          apply subtypePath;
            [intros xx; apply (isaprop_is_nat_trans _ _ has_homsets_HSET)|].
          apply funextsec; intro y; apply funextsec; intro z; cbn.
          repeat apply maponpaths; unfold covyoneda_morphisms_data.
          assert (H : # R (f · pr1 z) = # R f · # R (pr1 z)).
          { apply functor_comp. }
          apply pathsinv0.
          now etrans; [apply (toforallpaths _ _ _ H x)|].
      }
    * abstract (
        apply (nat_trans_eq has_homsets_HSET); cbn; intro x;
        apply funextsec; intro p;
        apply maponpaths;
        assert (H : # R (identity x) = identity (R x));
          [apply functor_id|];
        induction p as [t p]; apply maponpaths; simpl;
        now apply pathsinv0; eapply pathscomp0; [apply (toforallpaths _ _ _ H p)|]).
  + abstract (
    intros [t p]; apply subtypePath; simpl;
    [intros x; apply (isaset_nat_trans has_homsets_HSET)|];
    apply (nat_trans_eq has_homsets_HSET); intros c;
    apply funextsec; intro rc;
    apply subtypePath;
    [intro x; apply (isaprop_is_nat_trans _ _ has_homsets_HSET)|]; simpl;
    rewrite p; cbn; clear p; apply funextsec; intro d; cbn;
    apply funextsec; intros [t0 pd]; simpl;
    assert (HH := toforallpaths _ _ _ (nat_trans_ax t c d t0) rc);
    cbn in HH; rewrite HH; cbn; unfold covyoneda_morphisms_data;
    unfold prodtofuntoprod; cbn;
    now rewrite id_right).

End exponentials_functor_cat.

Kernel pairs (kernel_pair_HSET)


Lemma pullback_HSET_univprop_elements {P A B C : HSET}
    {p1 : HSET ⟦ P, A ⟧} {p2 : HSET ⟦ P, B ⟧}
    {f : HSET ⟦ A, C ⟧} {g : HSET ⟦ B, C ⟧}
    (ep : p1 · f = p2 · g)
    (pb : isPullback ep)
  : (∏ a b (e : f a = g b), ∃! ab, p1 ab = a × p2 ab = b).
Show proof.
  intros a b e.
  set (Pb := (make_Pullback _ pb)).
  apply iscontraprop1.
  - apply invproofirrelevance; intros [ab [ea eb]] [ab' [ea' eb']].
    apply subtypePath; simpl.
      intros x; apply isapropdirprod; apply setproperty.
    use (@toforallpaths unitset _ (λ _, ab) (λ _, ab') _ tt).
    use (MorphismsIntoPullbackEqual pb);
    apply funextsec; intros []; cbn;
    (eapply @pathscomp0; [ eassumption | apply pathsinv0; eassumption]).
  - use (_,,_).
    use (_ tt).
    use (PullbackArrow Pb (unitset : HSET)
      (λ _, a) (λ _, b)).
    apply funextsec; intro; exact e.
    simpl; split.
    + generalize tt; apply toforallpaths.
      apply (PullbackArrow_PullbackPr1 Pb unitset).
    + generalize tt; apply toforallpaths.
      apply (PullbackArrow_PullbackPr2 Pb unitset).

Section kernel_pair_Set.

  Context {A B: HSET}.
  Variable (f: HSET ⟦A,B⟧).

  Definition kernel_pair_HSET : kernel_pair f.
    red.
    apply PullbacksHSET.
  Defined.

  Local Notation g := kernel_pair_HSET.

Formulation in the categorical language of the universal property enjoyed by surjections (univ_surj)
  Lemma isCoeqKernelPairSet (hf: issurjective f) :
    isCoequalizer _ _ _ (PullbackSqrCommutes g).
  Show proof.
    intros.
    red.
    intros C u equ.
    assert (hcompat : ∏ x y : pr1 A, f x = f y → u x = u y).
    {
      intros x y eqfxy.
      assert (hpb:=pullback_HSET_univprop_elements
                     (PullbackSqrCommutes g) (isPullback_Pullback g) x y eqfxy).
      assert( hpb' := pr2 (pr1 hpb)); simpl in hpb'.
      etrans.
      eapply pathsinv0.
      apply maponpaths.
      exact (pr1 hpb').
      eapply pathscomp0.
      apply toforallpaths in equ.
      apply equ.
      cbn.
      apply maponpaths.
      exact (pr2 hpb').
    }
    use (unique_exists (univ_surj (setproperty C) _ _ _ hf)).
    - exact u.
    - exact hcompat.
    - simpl.
      apply funextfun.
      intro.
      apply univ_surj_ax.
    - intro. apply has_homsets_HSET.
    - intros ??; simpl.
      apply funextfun.
      use univ_surj_unique.
      simpl in X.
      apply toforallpaths in X.
      exact X.

End kernel_pair_Set.

Effective epis (EffectiveEpis_HSET)


Lemma EffectiveEpis_HSET : EpisAreEffective HSET.
Show proof.
  red.
  clear.
  intros A B f epif.
  exists (kernel_pair_HSET f).
  apply isCoeqKernelPairSet.
  now apply EpisAreSurjective_HSET.

Split epis with axiom of choice (SplitEpis_HSET)


Lemma SplitEpis_HSET : AxiomOfChoice_surj -> epis_are_split HSET.
Show proof.
  intros axC A B f epif.
  apply EpisAreSurjective_HSET,axC in epif.
  unshelve eapply (hinhfun _ epif).
  intro h.
  exists (pr1 h).
  apply funextfun.
  exact (pr2 h).

Forgetful functor to type_precat


Definition forgetful_HSET : functor HSET type_precat.
Show proof.
  use make_functor.
  - use make_functor_data.
    + exact pr1.
    + exact (λ _ _, idfun _).
  - split.
    + intro; apply idpath.
    + intros ? ? ? ? ?; apply idpath.

This functor is conservative; it reflects isomorphisms.
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! This statement seems problematic. This conservativity statement is for precategories, but now it is only for categories in the library !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
Lemma conservative_forgetful_HSET : conservative forgetful_HSET. Proof. unfold conservative. intros a b f is_iso_forget_f. refine (hset_equiv_is_iso a b (make_weq f _)). apply (type_iso_is_equiv _ (make_iso _ is_iso_forget_f)). Defined.

Subobject classifier


Lemma isaprop_hfiber_monic {A B : hSet} (f : HSET⟦A, B⟧) (isM : isMonic f) :
  isPredicate (hfiber f).
Show proof.
  intro; apply incl_injectivity, MonosAreInjective_HSET; assumption.

Local Definition const_htrue {X : hSet} : HSET⟦X, hProp_set⟧ :=
  (fun _ => htrue : hProp_set).

Local Lemma hProp_eq_unit (p : hProp) : p -> p = htrue.
Show proof.
  intro pp.
  apply weqtopathshProp, weqimplimpl.
  - intro; exact tt.
  - intro; assumption.
  - apply propproperty.
  - apply propproperty.

Existence of the pullback square 
      X -------> TerminalHSET
      V              V
    m |              | true
      V     ∃!       V
      Y - - - - -> hProp
Uniqueness proven below.
Definition subobject_classifier_HSET_pullback {X Y : HSET}
  (m : Monic HSET X Y) :
    ∑ (chi : HSET ⟦ Y, hProp_set ⟧)
    (H : m · chi = TerminalArrow TerminalHSET X · const_htrue),
      isPullback H.
Show proof.
  exists (fun z => (hfiber (pr1 m) z,, isaprop_hfiber_monic (pr1 m) (pr2 m) z)).
  use tpair.
  + apply funextfun; intro.
    apply hProp_eq_unit; cbn.
    use make_hfiber.
    * assumption.
    * apply idpath.
  +
The aforementioned square is a pullback
    cbn beta.
    unfold isPullback; cbn.
    intros Z f g H.
    use make_iscontr.
    * use tpair.
      --
The hypothesis H states that that each f x is in the image of m, and since m is monic (injective), this assignment extends to a map Z -> X defined by z ↦ m^-1 (f z).
          intro z.
          eapply hfiberpr1.
          eapply eqweqmap.
          ++ apply pathsinv0.
            apply (maponpaths pr1 (toforallpaths _ _ _ H z)).
          ++ exact tt.
      -- split.
          ++
The first triangle commutes by definition of the above map: m sends the preimage m^-1 (f z) to f z.
            apply funextfun; intro z; cbn.
            apply hfiberpr2.
          ++
All maps to the terminal object are equal
            apply proofirrelevance, impred.
            intro; apply isapropunit.
    * intro t.
      apply subtypePath.
      -- intro.
          apply isapropdirprod.
         ++ apply funspace_isaset, setproperty.
         ++ apply funspace_isaset, isasetunit.
      -- cbn.
          apply funextsec; intro; cbn.
Precompose with m and use the commutative square
          apply (invweq (make_weq _ (MonosAreInjective_HSET m (MonicisMonic _ m) _ _))).
          eapply pathscomp0.
          ++ apply (toforallpaths _ _ _ (pr1 (pr2 t))).
          ++ apply pathsinv0.
             apply hfiberpr2.

For any subset s : Y -> hProp, the carrier ∑ y : Y, s y is a pullback of s with the constantly-true arrow.
Lemma carrier_Pullback {Y : HSET} (chi : HSET ⟦ Y, hProp_set ⟧) :
  Pullback chi (@const_htrue unitHSET).
Show proof.
  use make_Pullback.
  - exact (carrier_subset chi).
  - exact (pr1carrier _).
  - exact (TerminalArrow TerminalHSET _).
  - apply funextfun; intro yy.
    apply hProp_eq_unit; cbn.
    apply (pr2 yy).
  - cbn.
    intros pb' h k H.
    use make_iscontr.
    + use tpair.
      * intro p.
        use tpair.
        -- exact (h p).
        -- apply toforallpaths in H; cbn.
           specialize (H p); cbn in H.
           abstract (rewrite H; exact tt).
      * split; [apply idpath|].
        apply proofirrelevance, hlevelntosn, iscontrfuntounit.
    + intro t.
      apply subtypePath; [intro; apply isapropdirprod; apply isaset_set_fun_space|].
      apply funextfun; intro.
      apply subtypePath; [intro; apply propproperty|].
      refine (_ @ toforallpaths _ _ _ (pr1 (pr2 t)) x).
      apply idpath.

Lemma hfiber_in_hfiber :
  ∏ Z W (g : Z -> W) (w : W) (z : hfiber g w), hfiber g (g (hfiberpr1 _ _ z)).
Show proof.
  intros.
  use make_hfiber.
  - exact (hfiberpr1 _ _ z).
  - apply idpath.

Definition subobject_classifier_HSET : subobject_classifier TerminalHSET.
Show proof.
  exists hProp_set.
  exists const_htrue.
  intros ? ? m.

  use make_iscontr.

  -
The image of m
    apply subobject_classifier_HSET_pullback.
  - intro O'.
    apply subtypePath.
    + intro.
      apply Propositions.isaproptotal2.
      * intro; apply isaprop_isPullback.
      * intros; apply proofirrelevance, homset_property.
    +
If the following is a pullback square, 
            X ------- ! ---> unit
            |                 |
            |                 |
            V                 V
            Y -- pr1 O' --> hProp
then pr1 O' = hfiber m.

      assert (eq : m · pr1 O' ~
                     m · (fun z => (hfiber (pr1 m) z,, isaprop_hfiber_monic (pr1 m) (pr2 m) z :
                                   pr1hSet hProp_set))).
      {
        apply toforallpaths.
        refine (pr1 (pr2 O') @ _).
        apply (!pr1 (pr2 (subobject_classifier_HSET_pullback m))).
      }

      apply funextfun; intro y.
      apply weqtopathshProp, weqimplimpl.
      * intro isO.

We know that carrier (pr1 O') is a pullback of pr1 O' and const_htrue. By hypothesis, X is as well. Thus, we have a canonical isomorphism carrier (pr1 O') -> X, which commutes with the pullback projections. In particular, the following triangle commutes (where m is, by hypothesis, the first pullback projection of X): 
                                ∃!
              carrier (pr1 O') ---> X
                            \       |
                   pr1carrier \     | m
                                \   V
                                    Y

        pose (PBO' := make_Pullback (pr1 (pr2 O')) (pr2 (pr2 O'))).
        pose (PBC := carrier_Pullback (pr1 O')).
        pose (pbiso := pullbackiso _ PBC PBO').

        use make_hfiber.
        -- exact (morphism_from_z_iso _ _ (pr1 pbiso) (y,, isO)).
        -- change (pr1 m (morphism_from_z_iso _ _ (pr1 pbiso) (y,, isO))) with
                  (((pr1 pbiso) · pr1 m) (y,, isO)).
           change (pr1 m) with (PullbackPr1 PBO').
           pose (pr1 (pr2 pbiso)) as p.
           exact (maponpaths (λ z, z _) p).
      * intros fib.
        apply (eqweqmap (maponpaths pr1 (maponpaths (pr1 O') (pr2 fib)))).
        apply (eqweqmap (maponpaths pr1 (eq (hfiberpr1 _ _ fib)))).
        apply hfiber_in_hfiber.
      * apply propproperty.
      * apply propproperty.

Definition Topos_Structure_HSET : Topos_Structure HSET.
  Show proof.
    use make_Topos_Structure.
    + exact PullbacksHSET.
    + exact TerminalHSET.
    + exact subobject_classifier_HSET.
    + use PowerObject_from_exponentials.
      assert (p : (BinProductsFromPullbacks PullbacksHSET TerminalHSET) = BinProductsHSET).
      { use proofirrelevance.
        use impredtwice.
        repeat intro.
        use isaprop_BinProduct.
        use is_univalent_HSET. }
      rewrite p.
      use Exponentials_HSET.