{-# OPTIONS --without-K --rewriting #-}

open import category-theory.exponential-objects-precategories
open import category-theory.precategories
open import category-theory.products-in-precategories
open import category-theory.slice-precategories

open import foundation.action-on-identifications-functions
open import foundation.cartesian-product-types
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equality-dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.function-extensionality
open import foundation.homotopies
open import foundation.identity-types
open import foundation.propositions
open import foundation.sets
open import foundation.subtypes
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import iterative.set
open import iterative.set.category
open import iterative.set.category.properties
open import iterative.set.category.slices
open import notation

module iterative.set.category.slices.properties where

-- All slice categories of V⁰ have binary products since V⁰ has pullbacks
module _ {i : Level} (a : V⁰ i) where

  module _ ((x , f) (y , g) : obj-Precategory (V⁰/ a)) where

    product-V⁰/ : obj-Precategory (V⁰/ a)
    pr1 product-V⁰/ = pullback⁰ i a x y f g
    pr2 product-V⁰/ = pr1

    proj₁-V⁰/ : hom-Precategory (V⁰/ a) product-V⁰/ (x , f)
    pr1 proj₁-V⁰/ = pr1 ∘ (pr1 ∘ pr2)
    pr2 proj₁-V⁰/ = eq-htpy (pr2 ∘ (pr1 ∘ pr2))

    proj₂-V⁰/ : hom-Precategory (V⁰/ a) product-V⁰/ (y , g)
    pr1 proj₂-V⁰/ = pr1 ∘ (pr2 ∘ pr2)
    pr2 proj₂-V⁰/ = eq-htpy (pr2 ∘ (pr2 ∘ pr2))

    is-product-Precategory-V⁰/ : is-product-Precategory (V⁰/ a) (x , f) (y , g) product-V⁰/ proj₁-V⁰/ proj₂-V⁰/
    is-product-Precategory-V⁰/ (w , h) (h₁ , p₁) (h₂ , p₂) = is-contr-Σ-is-prop k d σ ϕ
      where
        k : hom-Precategory (V⁰/ a) (w , h) product-V⁰/
        pr1 k c = (h c , (h₁ c , htpy-eq p₁ c) , (h₂ c , htpy-eq p₂ c))
        pr2 k = refl

        d : (comp-hom-Precategory (V⁰/ a) {(w , h)} {product-V⁰/} {(x , f)} proj₁-V⁰/ k ＝ (h₁ , p₁)) ×
            (comp-hom-Precategory (V⁰/ a) {(w , h)} {product-V⁰/} {(y , g)} proj₂-V⁰/ k ＝ (h₂ , p₂))
        pr1 d = eq-hom-Slice-Precategory (V⁰-Precategory i) a {(w , h)} {(x , f)} _ _ refl
        pr2 d = eq-hom-Slice-Precategory (V⁰-Precategory i) a {(w , h)} {(y , g)} _ _ refl

        σ : (k' : hom-Precategory (V⁰/ a) (w , h) product-V⁰/)
          → is-prop
              ((comp-hom-Precategory (V⁰/ a) {(w , h)} {product-V⁰/} {(x , f)} proj₁-V⁰/ k' ＝ (h₁ , p₁)) ×
              (comp-hom-Precategory (V⁰/ a) {(w , h)} {product-V⁰/} {(y , g)} proj₂-V⁰/ k' ＝ (h₂ , p₂)))
        σ k' =
          is-prop-prod
            (is-set-type-Set (hom-set-Slice-Precategory (V⁰-Precategory i) a (w , h) (x , f)) _ _)
            (is-set-type-Set (hom-set-Slice-Precategory (V⁰-Precategory i) a (w , h) (y , g)) _ _)

        ϕ : (k' : hom-Precategory (V⁰/ a) (w , h) product-V⁰/)
          → ((comp-hom-Precategory (V⁰/ a) {(w , h)} {product-V⁰/} {(x , f)} proj₁-V⁰/ k' ＝ (h₁ , p₁)) ×
            (comp-hom-Precategory (V⁰/ a) {(w , h)} {product-V⁰/} {(y , g)} proj₂-V⁰/ k' ＝ (h₂ , p₂)))
          → k == k'
        ϕ (k' , α) (β₁ , β₂) =
          eq-hom-Slice-Precategory (V⁰-Precategory i) a {(w , h)} {product-V⁰/} k (k' , α)
            (eq-htpy (λ c →
              map-inv-equiv (extensionality-pullback⁰ i a x y f g _ (k' c))
                (inv (htpy-eq (ap pr1 β₁) c) , inv (htpy-eq (ap pr1 β₂) c))))

  has-all-binary-products-Precategory-V⁰/ : has-all-binary-products-Precategory (V⁰/ a)
  pr1 (has-all-binary-products-Precategory-V⁰/ s t) = product-V⁰/ s t
  pr1 (pr2 (has-all-binary-products-Precategory-V⁰/ s t)) = proj₁-V⁰/ s t
  pr1 (pr2 (pr2 (has-all-binary-products-Precategory-V⁰/ s t))) = proj₂-V⁰/ s t
  pr2 (pr2 (pr2 (has-all-binary-products-Precategory-V⁰/ s t))) = is-product-Precategory-V⁰/ s t


-- All slice categories of V⁰ have exponentials
module _ {i : Level} (a : V⁰ i) where

  module _ ((x , f) (y , g) : obj-Precategory (V⁰/ a)) where

    exp-V⁰/ : obj-Precategory (V⁰/ a)
    pr1 exp-V⁰/ = Σ⁰ a (λ j → fiber'⁰ x a f j →⁰ fiber'⁰ y a g j)
    pr2 exp-V⁰/ = pr1

    eq-exp-V⁰/ : {h k : El⁰ (Σ⁰ a (λ j → fiber'⁰ x a f j →⁰ fiber'⁰ y a g j))}
               → (p : pr1 k == pr1 h)
               → (∀ s → pr1 (pr2 h s) == pr1 (pr2 k (pr1 s , (p ∙ pr2 s))))
               → h == k
    eq-exp-V⁰/ refl q = eq-pair-Σ refl (eq-htpy (λ s → eq-type-subtype (λ _ → _ , is-set-El⁰ a _ _) (q s)))

    ev-V⁰/ : hom-Precategory (V⁰/ a) (product-V⁰/ a exp-V⁰/ (x , f)) (y , g)
    pr1 ev-V⁰/ (j , ((j' , h) , j=j') , (l , j=fl)) = pr1 (h (l , (inv j=j' ∙ j=fl)))
    pr2 ev-V⁰/ = eq-htpy (λ (j , ((j' , h) , j=j') , (l , j=fl)) → j=j' ∙ pr2 (h (l , (inv j=j' ∙ j=fl))))

    is-exponential-Precategory-V⁰/ :
      is-exponential-Precategory (V⁰/ a) (has-all-binary-products-Precategory-V⁰/ a)
        (x , f)
        (y , g)
        exp-V⁰/
        ev-V⁰/
    is-exponential-Precategory-V⁰/ (z , h) (k , α) = is-contr-Σ-is-prop h' d σ ϕ
      where
        h' : hom-Precategory (V⁰/ a) (z , h) exp-V⁰/
        pr1 h' s = (h s , λ (l , hs=fl) → (k (h s , (s , refl) , (l , hs=fl))) ,
                                          htpy-eq α (h s , (s , refl) , (l , hs=fl)))
        pr2 h' = refl

        d : comp-hom-Precategory (V⁰/ a)
              {product-V⁰/ a (z , h) (x , f)} {product-V⁰/ a exp-V⁰/ (x , f)} {(y , g)}
              (ev-V⁰/)
              (map-product-Precategory (V⁰/ a) (has-all-binary-products-Precategory-V⁰/ a)
                {(z , h)} {(x , f)} {exp-V⁰/} {(x , f)}
                (h')
                (id-hom-Precategory (V⁰/ a) {(x , f)}))
          == (k , α)
        d = eq-hom-Slice-Precategory (V⁰-Precategory i) a {product-V⁰/ a (z , h) (x , f)} {y , g} _ _
              (eq-htpy (λ { (.(h s) , (s , refl) , (l , hs=fl)) →
                            tr (λ p → k (h s , (s , refl) , l , p) == k (h s , (s , refl) , l , hs=fl))
                               (eq-is-prop (is-set-El⁰ a (h s) (f l)))
                               refl }))

        σ : (h'' : hom-Precategory (V⁰/ a) (z , h) exp-V⁰/)
          → is-prop
              (comp-hom-Precategory (V⁰/ a)
                {product-V⁰/ a (z , h) (x , f)} {product-V⁰/ a exp-V⁰/ (x , f)} {(y , g)}
                (ev-V⁰/)
                (map-product-Precategory (V⁰/ a) (has-all-binary-products-Precategory-V⁰/ a)
                  {(z , h)} {(x , f)} {exp-V⁰/} {(x , f)}
                  (h'')
                  (id-hom-Precategory (V⁰/ a) {(x , f)}))
              == (k , α))
        σ h'' = is-set-type-Set (hom-set-Slice-Precategory (V⁰-Precategory i) a (product-V⁰/ a (z , h) (x , f)) (y , g)) _ _

        ϕ : (h'' : hom-Precategory (V⁰/ a) (z , h) exp-V⁰/)
          → comp-hom-Precategory (V⁰/ a)
              {product-V⁰/ a (z , h) (x , f)} {product-V⁰/ a exp-V⁰/ (x , f)} {(y , g)}
              (ev-V⁰/)
              (map-product-Precategory (V⁰/ a) (has-all-binary-products-Precategory-V⁰/ a)
                {(z , h)} {(x , f)} {exp-V⁰/} {(x , f)}
                (h'')
                (id-hom-Precategory (V⁰/ a) {(x , f)}))
            == (k , α)
          → h' == h''
        ϕ (h'' , β) p =
          eq-hom-Slice-Precategory (V⁰-Precategory i) a {z , h} {exp-V⁰/} _ _
            (eq-htpy (λ s →
              eq-exp-V⁰/
                (inv (htpy-eq β s))
                (λ s' → inv (tr (λ q → pr1 (pr2 (h'' s) (pr1 s' , q)) == k (h s , (s , refl) , s'))
                                (eq-is-prop (is-set-El⁰ a _ _))
                                (htpy-eq (ap pr1 p) (h s , (s , refl) , s'))))))

  has-all-exponentials-Precategory-V⁰/ : has-all-exponentials-Precategory (V⁰/ a) (has-all-binary-products-Precategory-V⁰/ a)
  pr1 (has-all-exponentials-Precategory-V⁰/ s t) = exp-V⁰/ s t
  pr1 (pr2 (has-all-exponentials-Precategory-V⁰/ s t)) = ev-V⁰/ s t
  pr2 (pr2 (has-all-exponentials-Precategory-V⁰/ s t)) = is-exponential-Precategory-V⁰/ s t