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

open import category-theory.coproducts-in-precategories
open import category-theory.initial-objects-precategories
open import category-theory.natural-numbers-object-precategories
open import category-theory.precategories
open import category-theory.products-in-precategories
open import category-theory.pullbacks-in-precategories
open import category-theory.pushouts-in-precategories
open import category-theory.terminal-objects-precategories

open import elementary-number-theory.natural-numbers
open import elementary-number-theory.universal-property-natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.booleans
open import foundation.cartesian-product-types
open import foundation.contractible-types
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.equality-cartesian-product-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.functoriality-cartesian-product-types
open import foundation.functoriality-dependent-pair-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.propositions
open import foundation.raising-universe-levels
open import foundation.sets
open import foundation.subtypes
open import foundation.universal-property-equivalences
open import foundation.universal-property-unit-type
open import foundation.universe-levels
open import foundation.unit-type

open import set-quotient
open import iterative.set
open import iterative.set.category
open import notation

module iterative.set.category.properties where


-- V⁰-Precategory has initial and terminal objects
-- and a natural numbers object
module _ (i : Level) where

  initial-obj-Precategory-V⁰ : initial-obj-Precategory (V⁰-Precategory i)
  pr1 initial-obj-Precategory-V⁰ = empty⁰
  pr1 (pr2 initial-obj-Precategory-V⁰ x) = raise-ex-falso i
  pr2 (pr2 initial-obj-Precategory-V⁰ x) _ = eq-htpy (λ z → raise-ex-falso i z)

  terminal-obj-Precategory-V⁰ : terminal-obj-Precategory (V⁰-Precategory i)
  pr1 terminal-obj-Precategory-V⁰ = unit⁰
  pr1 (pr2 terminal-obj-Precategory-V⁰ x) _ = raise-star
  pr2 (pr2 terminal-obj-Precategory-V⁰ x) _ = eq-htpy (λ _ → eq-is-prop is-prop-raise-unit)

  NNO-V⁰ : natural-numbers-object-Precategory (V⁰-Precategory i) terminal-obj-Precategory-V⁰
  pr1 NNO-V⁰ = ℕ⁰
  pr1 (pr2 NNO-V⁰) _ = map-raise zero-ℕ
  pr1 (pr2 (pr2 NNO-V⁰)) = map-raise ∘ (succ-ℕ ∘ map-inv-raise)
  pr2 (pr2 (pr2 NNO-V⁰)) x q f =
    is-contr-equiv
     (Σ (ℕ → El⁰ x) (λ α → α zero-ℕ == q (map-raise star) × (α ∘ succ-ℕ ~ f ∘ α)))
     (equiv-Σ _
       (equiv-precomp (compute-raise i ℕ) (El⁰ x))
       (λ α → equiv-prod
         (equiv-ap (equiv-universal-property-unit (El⁰ x) ∘e equiv-precomp (compute-raise-unit i) (El⁰ x)) _ _)
         (equiv-funext
         ∘e equiv-ap (equiv-precomp (compute-raise i ℕ) (El⁰ x)) _ _)))
     (is-contr-structure-preserving-map-ℕ (q (map-raise star)) f)

-- V⁰-Precategory has all binary products
module _ (i : Level) where

  module _ (x y : V⁰ i) where

    proj₁-product⁰ : El⁰ (x ×⁰ y) → El⁰ x
    proj₁-product⁰ (x , _) = x

    proj₂-product⁰ : El⁰ (x ×⁰ y) → El⁰ y
    proj₂-product⁰ (_ , y) = y

    is-product-Precategory-V⁰ : is-product-Precategory (V⁰-Precategory i) x y (x ×⁰ y) proj₁-product⁰ proj₂-product⁰
    is-product-Precategory-V⁰ z f g =
      is-contr-Σ-is-prop
        (λ w → f w , g w )
        (refl , refl)
        (λ _ → is-prop-prod (is-set-hom-Precategory (V⁰-Precategory i) z x _ _)
                            (is-set-hom-Precategory (V⁰-Precategory i) z y _ _))
        (λ h p → eq-htpy (λ x → map-inv-equiv (equiv-pair-eq (f x , g x) (h x))
                                              ((inv (htpy-eq (pr1 p) x))
                                              , inv (htpy-eq (pr2 p) x))))

  has-all-binary-products-V⁰ : has-all-binary-products-Precategory (V⁰-Precategory i)
  pr1 (has-all-binary-products-V⁰ x y) = x ×⁰ y
  pr1 (pr2 (has-all-binary-products-V⁰ x y)) = proj₁-product⁰ x y
  pr1 (pr2 (pr2 (has-all-binary-products-V⁰ x y))) = proj₂-product⁰ x y
  pr2 (pr2 (pr2 (has-all-binary-products-V⁰ x y))) = is-product-Precategory-V⁰ x y

-- V⁰-Precategory has all binary coproducts
module _ (i : Level) where

  module _ (x y : V⁰ i) where

    inj₁-coproduct⁰ : El⁰ x → El⁰ (x +⁰ y)
    inj₁-coproduct⁰ = inl

    inj₂-coproduct⁰ : El⁰ y → El⁰ (x +⁰ y)
    inj₂-coproduct⁰ = inr

    split : (z : V⁰ i) → (El⁰ x → El⁰ z) → (El⁰ y → El⁰ z) → (El⁰ (x +⁰ y) → El⁰ z)
    split z left right (inl a) = left a
    split z left right (inr b) = right b

    is-coproduct-Precategory-V⁰ : is-coproduct-Precategory (V⁰-Precategory i) x y (x +⁰ y) inj₁-coproduct⁰ inj₂-coproduct⁰
    is-coproduct-Precategory-V⁰ z f g =
      (split z f g , refl , refl) , λ cospan →
        eq-pair-Σ
          (eq-htpy (unique-map cospan))
          (eq-pair
            (eq-is-prop (is-set-hom-Precategory (V⁰-Precategory i) x z _ _))
            (eq-is-prop (is-set-hom-Precategory (V⁰-Precategory i) y z _ _)))
      where
        unique-map :
          (cospan :
            Σ (hom-Precategory (V⁰-Precategory i) (x +⁰ y) z)
              (λ h →
                (comp-hom-Precategory (V⁰-Precategory i) {x = x} {y = x +⁰ y} {z = z} h inj₁-coproduct⁰ ＝ f)
                × (comp-hom-Precategory (V⁰-Precategory i) {x = y} {y = x +⁰ y} {z = z} h inj₂-coproduct⁰ ＝ g)))
            → (a : El⁰ (x +⁰ y)) → split z f g a ＝ pr1 cospan a
        unique-map (cogap , comm-l , comm-r) (inl c) = inv (htpy-eq comm-l c)
        unique-map (cogap , comm-l , comm-r) (inr d) = inv (htpy-eq comm-r d)

  has-all-binary-coproducts-V⁰ : has-all-binary-coproducts (V⁰-Precategory i)
  pr1 (has-all-binary-coproducts-V⁰ x y) = x +⁰ y
  pr1 (pr2 (has-all-binary-coproducts-V⁰ x y)) = inj₁-coproduct⁰ x y
  pr1 (pr2 (pr2 (has-all-binary-coproducts-V⁰ x y))) = inj₂-coproduct⁰ x y
  pr2 (pr2 (pr2 (has-all-binary-coproducts-V⁰ x y))) = is-coproduct-Precategory-V⁰ x y

-- V⁰-Precategory has all pullbacks
module _ (i : Level) where

  pullback⁰ : (A X Y : V⁰ i)
            → (El⁰ X → El⁰ A)
            → (El⁰ Y → El⁰ A)
            → V⁰ i
  pullback⁰ A X Y f g = Σ⁰ A (λ a → fiber'⁰ X A f a ×⁰ fiber'⁰ Y A g a)

  -- We characterise the identity type of pullback⁰
  module _ (A X Y : V⁰ i) (f : El⁰ X → El⁰ A) (g : El⁰ Y → El⁰ A) where

    Eq-pullback⁰ : El⁰ (pullback⁰ A X Y f g) → El⁰ (pullback⁰ A X Y f g) → UU i
    Eq-pullback⁰ (a₀ , ((x₀ , _), (y₀ , _))) (a₁ , ((x₁ , _), (y₁ , _))) =
      (x₀ == x₁) × (y₀ == y₁)

    extensionality-pullback⁰ : ∀ s t → (s == t) ≃ Eq-pullback⁰ s t
    extensionality-pullback⁰ s t
           = equiv-pair-eq _ _
           ∘e extensionality-type-subtype'
                  (λ (b , c) → Id-Prop (El⁰-Set i A) (f b) (g c))
                  _
                  _
           ∘e equiv-ap α s t
      where
        α : El⁰ (pullback⁰ A X Y f g) ≃ Σ (El⁰ X × El⁰ Y) (λ (x , y) → f x == g y)
        pr1 α (a , (x , p) , (y , q)) = (x , y) , (inv p ∙ q)
        pr2 α =
          is-equiv-is-invertible
            (λ ((x , y) , p) → (f x) , ((x , refl) , (y , p)))
            (λ ((x , y) , p) → refl)
            (λ { (.(f x) , (x , refl) , (y , q)) → refl })

  module _ (a x y : V⁰ i) (f : El⁰ x → El⁰ a) (g : El⁰ y → El⁰ a) where

    proj₁-pullback⁰ : El⁰ (pullback⁰ a x y f g) → El⁰ x
    proj₁-pullback⁰ = pr1 ∘ (pr1 ∘ pr2)

    proj₂-pullback⁰ : El⁰ (pullback⁰ a x y f g) → El⁰ y
    proj₂-pullback⁰ = pr1 ∘ (pr2 ∘ pr2)

    comm-square-pullback⁰ : (f ∘ proj₁-pullback⁰) == (g ∘ proj₂-pullback⁰)
    comm-square-pullback⁰ = eq-htpy (λ s → inv (pr2 (pr1 (pr2 s))) ∙ pr2 (pr2 (pr2 s)))

    is-pullback-Precategory-V⁰ :
      is-pullback-Precategory (V⁰-Precategory i) a x y f g
        (pullback⁰ a x y f g)
        proj₁-pullback⁰
        proj₂-pullback⁰
        comm-square-pullback⁰
    is-pullback-Precategory-V⁰ w p₁ p₂ α = is-contr-Σ-is-prop k d σ ϕ
      where
        k : hom-Precategory (V⁰-Precategory i) w (pullback⁰ a x y f g)
        k s = (f (p₁ s)) , ((p₁ s , refl) , (p₂ s , htpy-eq α s))

        d : (comp-hom-Precategory (V⁰-Precategory i) {w} {pullback⁰ a x y f g} {x} proj₁-pullback⁰ k ＝ p₁) ×
            (comp-hom-Precategory (V⁰-Precategory i) {w} {pullback⁰ a x y f g} {y} proj₂-pullback⁰ k ＝ p₂)
        pr1 d = refl
        pr2 d = refl

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

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

  has-all-pullback-Precategory-V⁰ : has-all-pullback-Precategory (V⁰-Precategory i)
  pr1 (has-all-pullback-Precategory-V⁰ a x y f g) = pullback⁰ a x y f g
  pr1 (pr2 (has-all-pullback-Precategory-V⁰ a x y f g)) = proj₁-pullback⁰ a x y f g
  pr1 (pr2 (pr2 (has-all-pullback-Precategory-V⁰ a x y f g))) = proj₂-pullback⁰ a x y f g
  pr1 (pr2 (pr2 (pr2 (has-all-pullback-Precategory-V⁰ a x y f g)))) = comm-square-pullback⁰ a x y f g
  pr2 (pr2 (pr2 (pr2 (has-all-pullback-Precategory-V⁰ a x y f g)))) = is-pullback-Precategory-V⁰ a x y f g


-- V⁰-Precategory has all pushouts
module _ (i : Level) where

  module _ (A X Y : V⁰ i) (f : El⁰ A → El⁰ X) (g : El⁰ A → El⁰ Y) where
    ¦pushout¦ = (X +⁰ Y) /⁰ R where
             R : El⁰ (X +⁰ Y) → El⁰ (X +⁰ Y) → UU i
             R x y = Σ (El⁰ A) (λ a → inj₁-coproduct⁰ _ X Y (f a) == x × inj₂-coproduct⁰ _ X Y (g a) == y)
    p₁-pushout : El⁰ X → El⁰ ¦pushout¦
    p₁-pushout x = q[ (inj₁-coproduct⁰ _ X Y x) ]
    p₂-pushout : El⁰ Y → El⁰ ¦pushout¦
    p₂-pushout y = q[ (inj₂-coproduct⁰ _ X Y y) ]

    commutes-pushout : (p₁-pushout ∘ f) == (p₂-pushout ∘ g)
    commutes-pushout = eq-htpy (λ a → quot-rel (a , (refl , refl)))

    module _ (P : V⁰ i) (p₁ : El⁰ X → El⁰ P) (p₂ : El⁰ Y → El⁰ P) (c : (p₁ ∘ f) == (p₂ ∘ g) )where
      rec-pushout : El⁰ ¦pushout¦ → El⁰ P
      rec-pushout = set-quotient-rec (_)
                                     (is-set-El⁰ P)
                                     (split _ X Y P p₁ p₂)
                                     (λ { (a , (refl , refl) ) → htpy-eq c a})
      unique-rec-pushout : (w : El⁰ ¦pushout¦ → El⁰ P)
                         → ((w ∘ p₁-pushout) == p₁)
                         → ((w ∘ p₂-pushout) == p₂)
                         → w == rec-pushout
      unique-rec-pushout w p q = eq-htpy (set-quotient-prop-elim (_)
                                                                 (λ _ → is-set-El⁰ P _ _)
                                                                 (λ { (inl x) → htpy-eq p x ;
                                                                      (inr y) → htpy-eq q y}))

    pushouts-V⁰ : pushout-Precategory (V⁰-Precategory i) A X Y f g
    pushouts-V⁰ = ¦pushout¦
                , p₁-pushout
                , p₂-pushout
                , commutes-pushout
                , λ P p₁ p₂ c → ((rec-pushout P p₁ p₂ c , eq-htpy (λ _ → refl)
                                                        , eq-htpy (λ _ → refl))
                              , λ{(w , p , q) → eq-pair-Σ (inv (unique-rec-pushout P p₁ p₂ c w p q))
                                                          (eq-pair-Σ (eq-is-prop (is-set-function-type (is-set-El⁰ P) _ _))
                                                          (eq-is-prop (is-set-function-type (is-set-El⁰ P) _ _)))})

  has-all-pushout-V⁰ : has-all-pushout-Precategory (V⁰-Precategory i)
  has-all-pushout-V⁰ = pushouts-V⁰