Library UniMath.CategoryTheory.exponentials

**********************************************************

Anders Mörtberg, 2016

**********************************************************

Contents:

Definition of the functors given by binary product with a fixed object
Definition of exponentials

Section ExponentialsCarriedThroughAdjointEquivalence added by Ralph Matthes in 2023

use tpair.
- intro x; simpl; unfold BinProduct_of_functors_ob; simpl.
  apply BinProductArrow; [ apply BinProductPr2 | apply BinProductPr1 ].
- abstract (intros x y f; simpl; unfold BinProduct_of_functors_mor; simpl;
  eapply pathscomp0; [apply precompWithBinProductArrow|];
  apply pathsinv0; eapply pathscomp0; [apply postcompWithBinProductArrow|];
  now rewrite (BinProductOfArrowsPr2 C _ (PC a x)), (BinProductOfArrowsPr1 C _ (PC a x))).

Definition nat_trans_constprod_functor2 (a : C) :
nat_trans (constprod_functor2 a) (constprod_functor1 a).
Show proof.

Lemma is_z_iso_constprod_functor1 a :
@is_z_isomorphism [C ,C ] _ _ (nat_trans_constprod_functor1 a).
Show proof.

  exists (nat_trans_constprod_functor2 a).
  split.
  + abstract (
    apply (nat_trans_eq C); intro x; simpl; unfold BinProduct_of_functors_ob; simpl;
    eapply pathscomp0; [apply precompWithBinProductArrow|];
    now rewrite BinProductPr1Commutes, BinProductPr2Commutes, BinProductArrowEta, !id_left).
  + abstract (
    apply (nat_trans_eq C); intro x; simpl; unfold BinProduct_of_functors_ob; simpl;
    eapply pathscomp0; [apply precompWithBinProductArrow|];
    now rewrite BinProductPr1Commutes, BinProductPr2Commutes, BinProductArrowEta, !id_left).

Lemma is_z_iso_constprod_functor2 a :
@is_z_isomorphism [C ,C ] _ _ (nat_trans_constprod_functor2 a).
Show proof.

  exists (nat_trans_constprod_functor1 a).
  split.
  + abstract (
        apply (nat_trans_eq C); intro x; simpl; unfold BinProduct_of_functors_ob; simpl;
        eapply pathscomp0; [apply precompWithBinProductArrow|];
        now rewrite BinProductPr1Commutes, BinProductPr2Commutes, BinProductArrowEta, !id_left).
  + abstract (
        apply (nat_trans_eq C); intro x; simpl; unfold BinProduct_of_functors_ob; simpl;
        eapply pathscomp0; [apply precompWithBinProductArrow|];
        now rewrite BinProductPr1Commutes, BinProductPr2Commutes, BinProductArrowEta, !id_left).

Definition flip_z_iso a : @z_iso [C ,C ] (constprod_functor1 a) (constprod_functor2 a) :=
  tpair _ _ (is_z_iso_constprod_functor1 a).

Variable (a : C).
Variable (HF : is_left_adjoint (constprod_functor1 a)).

Local Notation F := (constprod_functor1 a).
Local Notation F' := (constprod_functor2 a).
Let G := right_adjoint HF.
Let H := pr2 HF : are_adjoints F G.
Let eta : [C ,C ]⟦functor_identity C ,functor_composite F G ⟧ := unit_from_left_adjoint H.
Let eps : [C ,C ]⟦functor_composite G F ,functor_identity C ⟧ := counit_from_left_adjoint H.
Let H1 := triangle_id_left_ad H.
Let H2 := triangle_id_right_ad H.

Arguments constprod_functor1 : simpl never.
Arguments constprod_functor2 : simpl never.
Arguments flip_z_iso : simpl never.

Local Definition eta' : [C ,C ]⟦functor_identity C ,functor_composite F' G ⟧ :=
  let G' := (post_composition_functor C C C G)
  in eta · (# G' (flip_z_iso a )).

Local Definition eps' : [C ,C ]⟦functor_composite G F',functor_identity C ⟧ :=
  let G' := (pre_composition_functor C C C G)
  in # G' (inv_from_z_iso (flip_z_iso a )) · eps.

Local Lemma form_adjunction_eta'_eps' : form_adjunction F' G eta' eps'.
Show proof.

fold eta in H1; fold eps in H1; fold eta in H2; fold eps in H2; fold G in H2.
use tpair.
+ intro x; unfold eta', eps'; cbn.
  rewrite assoc.
  eapply pathscomp0.
  - eapply cancel_postcomposition.
    exact (nat_trans_ax (inv_from_z_iso (flip_z_iso _)) _ _ _).
  - rewrite functor_comp, assoc.
    eapply pathscomp0; [rewrite <- assoc; apply maponpaths, (nat_trans_ax eps)|].
    rewrite <- assoc.
    eapply pathscomp0; [apply maponpaths; rewrite assoc; apply cancel_postcomposition, H1|].
    rewrite id_left.
    apply (nat_trans_eq_pointwise (z_iso_after_z_iso_inv (flip_z_iso a)) x).
+ intro x; cbn.
  rewrite <- (H2 x), <- assoc, <- (functor_comp G).
  apply maponpaths, maponpaths.
  rewrite assoc.
  apply remove_id_left; try apply idpath.
  apply (nat_trans_eq_pointwise (z_iso_inv_after_z_iso (flip_z_iso a))).

Lemma is_left_adjoint_constprod_functor2 : is_left_adjoint F'.
Show proof.

apply (tpair _ G).
apply (tpair _ (make_dirprod eta' eps')).
apply form_adjunction_eta'_eps'.

End exponentials.

Section ExponentialsCarriedThroughAdjointEquivalence.

  Context {C : category} (PC : BinProducts C) {D : category} (PD : BinProducts D)
    (ExpC : Exponentials PC) (adjeq : adj_equiv C D).

  Let F : functor C D := adjeq.
  Let G : functor D C := adj_equivalence_inv adjeq.
  Let η_z_iso : ∏ (c : C ), z_iso c (G (F c)) := unit_pointwise_z_iso_from_adj_equivalence adjeq.
  Let ε_z_iso : ∏ (d : D ), z_iso (F (G d)) d := counit_pointwise_z_iso_from_adj_equivalence adjeq.
  Let η_nat_z_iso : nat_z_iso (functor_identity C) (functor_composite F G) :=
        unit_nat_z_iso_from_adj_equivalence_of_cats adjeq.
  Let ε_nat_z_iso : nat_z_iso (functor_composite G F) (functor_identity D) :=
        counit_nat_z_iso_from_adj_equivalence_of_cats adjeq.

  Let FC (c : C) : functor C C := constprod_functor1 PC c.
  Let GC (c : C) : functor C C := right_adjoint (ExpC c).
  Let ηC (c : C) : functor_identity C ⟹ (FC c ) ∙ (GC c ) := unit_from_left_adjoint (ExpC c).
  Let εC (c : C) : functor_composite (GC c) (FC c) ⟹ functor_identity C := counit_from_left_adjoint (ExpC c).

Section FixAnObject.

  Context (d0 : D).

  Let Fd0 : functor D D := constprod_functor1 PD d0.
  Let Gd0 : functor D D := functor_composite (functor_composite G (GC (G d0))) F.

Local Definition inherited_BP_on_C (d : D) : BinProduct C (G d0) (G d).
Show proof.

  use tpair.
  - exists (G (pr1 (pr1 (PD d0 d)))).
    exact (# G (pr1 (pr2 (pr1 (PD d0 d )))),,# G (pr2 (pr2 (pr1 (PD d0 d ))))).
  - set (Hpres := right_adjoint_preserves_binproduct adjeq adjeq : preserves_binproduct G).
    exact (Hpres _ _ _ _ _ (pr2 (PD d0 d))).

Local Definition μ_nat_trans_data : nat_trans_data (G ∙ FC (G d0)) (Fd0 ∙ G).
Show proof.

intro d.
exact (BinProductOfArrows _ (inherited_BP_on_C d) (PC (G d0) (G d)) (identity _) (identity _)).

Local Lemma μ_nat_trans_law : is_nat_trans _ _ μ_nat_trans_data.
Show proof.

  intros d' d f.
  apply (BinProductArrowsEq _ _ _ (inherited_BP_on_C d)).
  - etrans.
    { rewrite assoc'.
      apply maponpaths.
      apply (BinProductOfArrowsPr1 _ (inherited_BP_on_C d) (PC (G d0) (G d))). }
    rewrite id_right.
    etrans.
    2: { cbn.
         rewrite assoc'.
         etrans.
         2: { apply maponpaths.
              apply functor_comp. }
         unfold BinProduct_of_functors_mor.
         cbn.
         etrans.
         2: { do 2 apply maponpaths.
              apply pathsinv0, BinProductOfArrowsPr1. }
         rewrite id_right.
         unfold BinProductPr1.
         apply pathsinv0, (BinProductOfArrowsPr1 _ (inherited_BP_on_C d') (PC (G d0) (G d'))).
    }
    rewrite id_right.
    cbn.
    unfold BinProduct_of_functors_mor, constant_functor, functor_identity.
    cbn.
    etrans.
    { apply (BinProductOfArrowsPr1 _ (PC (G d0) (G d)) (PC (G d0) (G d'))). }
    apply id_right.
  - etrans.
    { rewrite assoc'.
      apply maponpaths.
      apply (BinProductOfArrowsPr2 _ (inherited_BP_on_C d) (PC (G d0) (G d))). }
    rewrite id_right.
    etrans.
    2: { cbn.
         rewrite assoc'.
         etrans.
         2: { apply maponpaths.
              apply functor_comp. }
         unfold BinProduct_of_functors_mor.
         cbn.
         etrans.
         2: { do 2 apply maponpaths.
              apply pathsinv0, BinProductOfArrowsPr2. }
         rewrite functor_comp.
         rewrite assoc.
         apply cancel_postcomposition.
         unfold BinProductPr2.
         apply pathsinv0, (BinProductOfArrowsPr2 _ (inherited_BP_on_C d') (PC (G d0) (G d'))).
    }
    rewrite id_right.
    cbn.
    unfold BinProduct_of_functors_mor, constant_functor, functor_identity.
    cbn.
    etrans.
    { apply (BinProductOfArrowsPr2 _ (PC (G d0) (G d)) (PC (G d0) (G d'))). }
    apply idpath.

Local Definition μ_nat_trans : nat_trans (G ∙ FC (G d0)) (Fd0 ∙ G) := _,,μ_nat_trans_law.

Local Definition μ_nat_trans_inv_pointwise (d : D) : C ⟦ (Fd0 ∙ G ) d , (G ∙ FC (G d0)) d ⟧.
Show proof.

exact (BinProductOfArrows _ (PC (G d0) (G d)) (inherited_BP_on_C d) (identity _) (identity _)).

Local Lemma μ_nat_trans_is_inverse (d : D): is_inverse_in_precat (μ_nat_trans d) (μ_nat_trans_inv_pointwise d).
Show proof.

  split; cbn.
  - apply pathsinv0, BinProduct_endo_is_identity.
    + rewrite assoc'.
      etrans.
      { apply maponpaths.
        cbn.
        apply (BinProductOfArrowsPr1 _ (PC (G d0) (G d)) (inherited_BP_on_C d)). }
      rewrite id_right.
      etrans.
      { cbn.
        apply (BinProductOfArrowsPr1 _ (inherited_BP_on_C d) (PC (G d0) (G d))). }
      apply id_right.
    + rewrite assoc'.
      etrans.
      { apply maponpaths.
        cbn.
        apply (BinProductOfArrowsPr2 _ (PC (G d0) (G d)) (inherited_BP_on_C d)). }
      rewrite id_right.
      etrans.
      { cbn.
        apply (BinProductOfArrowsPr2 _ (inherited_BP_on_C d) (PC (G d0) (G d))). }
      apply id_right.
  - unfold BinProduct_of_functors_ob, constant_functor, functor_identity.
    cbn.
    apply pathsinv0. apply (BinProduct_endo_is_identity _ _ _ (inherited_BP_on_C d)).
    + rewrite assoc'.
      etrans.
      { apply maponpaths.
        apply (BinProductOfArrowsPr1 _ (inherited_BP_on_C d) (PC (G d0) (G d))). }
      rewrite id_right.
      etrans.
      { apply (BinProductOfArrowsPr1 _ (PC (G d0) (G d)) (inherited_BP_on_C d)). }
      apply id_right.
    + rewrite assoc'.
      etrans.
      { apply maponpaths.
        apply (BinProductOfArrowsPr2 _ (inherited_BP_on_C d) (PC (G d0) (G d))). }
      rewrite id_right.
      etrans.
      { apply (BinProductOfArrowsPr2 _ (PC (G d0) (G d)) (inherited_BP_on_C d)). }
      apply id_right.

Local Definition μ : nat_z_iso (functor_composite G (FC (G d0))) (functor_composite Fd0 G).
Show proof.

  use make_nat_z_iso.
  - exact μ_nat_trans.
  - intro d.
    use tpair.
    + exact (μ_nat_trans_inv_pointwise d).
    + exact (μ_nat_trans_is_inverse d).

Local Definition ηDd0 : functor_identity D ⟹ Fd0 ∙ Gd0.
Show proof.

  simple refine (nat_trans_comp _ _ _ (nat_z_iso_to_trans_inv ε_nat_z_iso) _).
  unfold Gd0.
  change ((functor_composite G (functor_identity C)) ∙ F ⟹ (Fd0 ∙ (G ∙ GC (G d0))) ∙ F).
  apply post_whisker.
  refine (nat_trans_comp _ _ _ _ _).
  - apply (pre_whisker G (ηC (G d0))).
  - change (functor_composite (functor_composite G (FC (G d0))) (GC (G d0)) ⟹
              functor_composite (Fd0 ∙ G) (GC (G d0))).
    apply post_whisker.
    apply μ.

Local Definition εDd0 : Gd0 ∙ Fd0 ⟹ functor_identity D.
Show proof.

  simple refine (nat_trans_comp _ _ _ _ ε_nat_z_iso).
  change (functor_composite (functor_composite Gd0 Fd0) (functor_identity D) ⟹ G ∙ F).
  refine (nat_trans_comp _ _ _ _ _).
  - apply (pre_whisker _ (nat_z_iso_to_trans_inv ε_nat_z_iso)).
  - change ((functor_composite (Gd0 ∙ Fd0) G ) ∙ F ⟹ G ∙ F).
    apply post_whisker.
    unfold Gd0.
    change (((G ∙ GC (G d0)) ∙ F ) ∙ (Fd0 ∙ G ) ⟹ G).
    refine (nat_trans_comp _ _ _ _ _).
    + apply (pre_whisker _ (nat_z_iso_to_trans_inv μ)).
    + change ((((G ∙ GC (G d0)) ∙ F ) ∙ G ) ∙ FC (G d0) ⟹ G).
      refine (nat_trans_comp _ _ _ _ _).
      * use (post_whisker _ (FC (G d0))).
        -- exact (G ∙ GC (G d0)).
        -- change (functor_composite (G ∙ GC (G d0)) (functor_composite F G) ⟹
                     functor_composite (G ∙ GC (G d0)) (functor_identity C)).
           apply (pre_whisker _ (nat_z_iso_to_trans_inv η_nat_z_iso)).
      * change (functor_composite G (functor_composite (GC (G d0)) (FC (G d0))) ⟹ G).
        apply (pre_whisker _ (εC (G d0))).

Definition is_expDd0_adjunction_data : adjunction_data D D.
Show proof.

  use make_adjunction_data.
  - exact Fd0.
  - exact Gd0.
  - exact ηDd0.
  - exact εDd0.

Lemma is_expDd0_adjunction_laws : form_adjunction' is_expDd0_adjunction_data.
Show proof.

  split.
  - intro d.
    change (# Fd0 (ηDd0 d ) · εDd0 (Fd0 d) = identity (Fd0 d)).
    unfold ηDd0.
    etrans.
    { apply cancel_postcomposition.
      etrans.
      { apply functor_comp. }
      do 2 apply maponpaths.
      assert (Hpost := post_whisker_composition _ _ _ F _ _ _ (pre_whisker G (ηC (G d0))) (post_whisker (pr1 μ) (GC (G d0)))).
      refine (toforallpaths _ _ _ (maponpaths pr1 Hpost) d).
    }
    etrans.
    { apply cancel_postcomposition.
      apply maponpaths.
      apply functor_comp. }
    unfold εDd0.
Abort.

End FixAnObject.

End ExponentialsCarriedThroughAdjointEquivalence.

Section AlternativeWithUnivalence.

  Context {C : category} (PC : BinProducts C) {D : category} (PD : BinProducts D)
    (ExpC : Exponentials PC) (adjeq : adj_equiv C D) (Cuniv : is_univalent C) (Duniv : is_univalent D).

  Local Lemma CDeq : C = D.
  Proof.
    assert (aux : category_to_precategory C = category_to_precategory D).
    { apply (invmap (catiso_is_path_precat C D D)).
      apply (adj_equivalence_of_cats_to_cat_iso adjeq); assumption. }
    apply subtypePath. intro. apply isaprop_has_homsets.
    exact aux.

Definition exponentials_through_adj_equivalence_univalent_cats : Exponentials PD.
Show proof.

    induction CDeq.
    clear adjeq.
    assert (aux : PC = PD).
    2: { rewrite <- aux. exact ExpC. }
    apply funextsec.
    intro c1.
    apply funextsec.
    intro c2.
    apply isaprop_BinProduct; exact Cuniv.

End AlternativeWithUnivalence.

Accessors for exponentials

Section AccessorsExponentials.
  Context {C : category}
          {prodC : BinProducts C}
          (expC : Exponentials prodC).

  Definition exp
             (x y : C)
    : C
    := pr1 (expC x) y.

  Definition exp_eval
             (x y : C)
    : prodC x (exp x y) --> y
    := counit_from_are_adjoints (pr2 (expC x)) y.

  Definition exp_eval_alt
             (x y : C)
    : prodC (exp x y) x --> y
    := prod_swap prodC _ _ · exp_eval x y.

  Definition exp_lam
             {x y z : C}
             (f : prodC y x --> z)
    : x --> exp y z
    := unit_from_are_adjoints (pr2 (expC y)) x · # (pr1 (expC y)) f.

  Definition exp_lam_alt
             {x y z : C}
             (f : prodC z x --> y)
    : z --> exp x y
    := exp_lam (prod_swap prodC _ _ · f).

  Proposition exp_beta
              {x y z : C}
              (f : prodC y x --> z)
    : BinProductOfArrows _ _ _ (identity _) (exp_lam f)
      · exp_eval _ _
      =
      f.
  Show proof.

    unfold exp_lam.
    rewrite <- BinProductOfArrows_idxcomp.
    rewrite !assoc'.
    etrans.
    {
      apply maponpaths.
      exact (nat_trans_ax
              (counit_from_are_adjoints (pr2 (expC y)))
              _
              _
              f).
    }
    cbn.
    rewrite !assoc.
    refine (_ @ id_left _).
    apply maponpaths_2.
    apply (triangle_id_left_ad (pr2 (expC y))).

  Proposition exp_beta_alt
              {x y z : C}
              (f : prodC z x --> y)
    : BinProductOfArrows _ _ _ (exp_lam_alt f) (identity x)
      · exp_eval_alt x y
      =
      f.
  Show proof.

    unfold exp_eval_alt.
    rewrite !assoc.
    rewrite BinProductOfArrows_swap.
    unfold exp_lam_alt.
    rewrite !assoc'.
    rewrite exp_beta.
    rewrite !assoc.
    rewrite prod_swap_swap.
    apply id_left.

  Proposition exp_eta
              {x y z : C}
              (f : z --> exp x y)
    : f
      =
      exp_lam (BinProductOfArrows C _ _ (identity x) f · exp_eval x y).
  Show proof.

    unfold exp_lam.
    rewrite functor_comp.
    rewrite !assoc.
    refine (!_).
    etrans.
    {
      apply maponpaths_2.
      exact (!(nat_trans_ax
                 (unit_from_are_adjoints (pr2 (expC x)))
                 _
                 _
                 f)).
    }
    refine (_ @ id_right _).
    rewrite !assoc'.
    apply maponpaths.
    exact (triangle_id_right_ad (pr2 (expC x)) _).

  Proposition exp_eta_alt
              {x y z : C}
              (f : z --> exp x y)
    : f
      =
      exp_lam_alt (BinProductOfArrows C _ _ f (identity x) · exp_eval_alt x y).
  Show proof.

    refine (exp_eta _ @ _).
    unfold exp_lam_alt.
    apply maponpaths.
    unfold exp_eval_alt.
    rewrite !assoc.
    apply maponpaths_2.
    rewrite !assoc'.
    rewrite BinProductOfArrows_swap.
    rewrite !assoc.
    rewrite prod_swap_swap.
    rewrite id_left.
    apply idpath.

  Proposition exp_funext
              {x y z : C}
              {f g : z --> exp x y}
              (p : ∏ (a : C)
                     (h : a --> x ),
                   BinProductOfArrows C _ (prodC a z) h f · exp_eval x y
                   =
                   BinProductOfArrows C _ (prodC a z) h g · exp_eval x y)
    : f = g.
  Show proof.

    refine (exp_eta f @ _ @ !(exp_eta g)).
    apply maponpaths.
    apply p.

  Proposition exp_lam_natural
              {w x y z : C}
              (f : prodC y x --> z)
              (s : w --> x)
    : s · exp_lam f
      =
      exp_lam (BinProductOfArrows _ _ _ (identity _ ) s · f).
  Show proof.

    use exp_funext.
    intros a h.
    etrans.
    {
      do 2 apply maponpaths_2.
      exact (!(id_right _)).
    }
    rewrite <- BinProductOfArrows_comp.
    rewrite !assoc'.
    rewrite exp_beta.
    refine (!_).
    etrans.
    {
      do 2 apply maponpaths_2.
      exact (!(id_right _)).
    }
    etrans.
    {
      apply maponpaths_2.
      apply maponpaths.
      exact (!(id_left _)).
    }
    rewrite <- BinProductOfArrows_comp.
    rewrite !assoc'.
    rewrite exp_beta.
    rewrite !assoc.
    apply maponpaths_2.
    rewrite BinProductOfArrows_comp.
    rewrite id_left, id_right.
    apply idpath.

End AccessorsExponentials.