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

open import category-theory.discrete-categories
open import category-theory.equivalences-of-precategories
open import category-theory.functors-precategories
open import category-theory.natural-isomorphisms-functors-precategories
open import category-theory.natural-transformations-functors-precategories
open import category-theory.precategories
open import category-theory.precategory-of-functors
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-extensionality
open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.propositions
open import foundation.sets
open import foundation.subtypes
open import foundation.universe-levels

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

module iterative.set.category.slices.functor where

module _ (i : Level) (X : V⁰ i) where
  V⁰/X : Precategory (lsuc i) i
  V⁰/X = V⁰/ X

  X-Precategory : Precategory i i
  X-Precategory = discrete-precategory-Set (El⁰-Set i X)

  X→V⁰ : Precategory (lsuc i) i
  X→V⁰ = functor-precategory-Precategory X-Precategory (V⁰-Precategory i)

  V⁰/X-to-X→V⁰ : functor-Precategory V⁰/X X→V⁰
  V⁰/X-to-X→V⁰ = obj , (λ {x} {y} → hom x y) , comp-assoc , comp-id
    where
      obj : obj-Precategory V⁰/X → obj-Precategory X→V⁰
      pr1 (obj (Y , p)) = fiber'⁰ Y X p
      pr1 (pr2 (obj (Y , p))) refl y = y
      pr1 (pr2 (pr2 (obj (Y , p)))) refl refl = refl
      pr2 (pr2 (pr2 (obj (Y , p)))) x = refl

      hom :
        (a b : obj-Precategory V⁰/X) →
        hom-Precategory V⁰/X a b →
        hom-Precategory X→V⁰ (obj a) (obj b)
      pr1 (hom a b (f , eq₁)) x (y , eq₂) = f y , (eq₂ ∙ htpy-eq eq₁ y)
      pr2 (hom a b (f , eq₁)) refl = refl

      comp-id : (x : obj-Precategory V⁰/X) → hom x x (id-hom-Precategory V⁰/X {x}) ＝ id-hom-Precategory X→V⁰ {obj x}
      comp-id x =
        eq-htpy-hom-family-natural-transformation-Precategory 
          X-Precategory
          (V⁰-Precategory i)
          (obj x)
          (obj x)
          (hom x x (id-hom-Precategory V⁰/X {x}))
          (id-hom-Precategory X→V⁰ {obj x})
          (λ d → eq-htpy (λ v → ap (λ x → pr1 v , x) right-unit))

      comp-assoc :
        {x y z : obj-Precategory V⁰/X}(g : hom-Precategory V⁰/X y z)(f : hom-Precategory V⁰/X x y) →
        hom x z (comp-hom-Precategory V⁰/X {x} {y} {z} g f) ＝
        comp-hom-Precategory X→V⁰ {obj x} {obj y} {obj z} (hom y z g) (hom x y f)
      comp-assoc {x} {y} {z} g f =
        eq-htpy-hom-family-natural-transformation-Precategory 
          X-Precategory
          (V⁰-Precategory i)
          (obj x)
          (obj z)
          (hom x z (comp-hom-Precategory V⁰/X {x} {y} {z} g f))
          (comp-hom-Precategory X→V⁰ {obj x} {obj y} {obj z} (hom y z g) (hom x y f))
          (λ d → eq-htpy λ v →
            eq-pair-Σ refl (eq-is-prop (is-set-El⁰ X d _)))

  X→V⁰-to-V⁰/X : functor-Precategory X→V⁰ V⁰/X
  X→V⁰-to-V⁰/X = obj , (λ {x} {y} → hom x y) , (λ {x}{y}{z} → comp-assoc x y z) , comp-id
    where
      obj : obj-Precategory X→V⁰ → obj-Precategory V⁰/X
      obj F = Σ⁰ X (pr1 F) , pr1

      hom :
        (F G : obj-Precategory X→V⁰) →
        hom-Precategory X→V⁰ F G →
        hom-Precategory V⁰/X (obj F) (obj G)
      pr1 (hom F G α) (x , b) = x , pr1 α x b
      pr2 (hom F G α) = refl

      comp-id : (x : obj-Precategory X→V⁰) → hom x x (id-hom-Precategory X→V⁰ {x}) ＝ id-hom-Precategory V⁰/X {obj x}
      comp-id x = refl

      comp-assoc :
        (x y z : obj-Precategory X→V⁰) (g : hom-Precategory X→V⁰ y z)
        (f : hom-Precategory X→V⁰ x y) →
        hom x z (comp-hom-Precategory X→V⁰ {x} {y} {z} g f) ＝
        comp-hom-Precategory V⁰/X {obj x} {obj y} {obj z} (hom y z g) (hom x y f)
      comp-assoc x y z g f = refl

  loop1 : functor-Precategory V⁰/X V⁰/X
  loop1 = comp-functor-Precategory V⁰/X X→V⁰ V⁰/X X→V⁰-to-V⁰/X V⁰/X-to-X→V⁰

  α : natural-isomorphism-Precategory V⁰/X V⁰/X loop1 (id-functor-Precategory V⁰/X)
  α = (f , λ {A} {B} → f-nat {A} {B}) , f-iso
    where
      f : (Y : obj-Precategory V⁰/X) → hom-Precategory V⁰/X (obj-functor-Precategory V⁰/X V⁰/X loop1 Y) Y
      f Y = (λ x → pr1 (pr2 x)) , eq-htpy (λ x → pr2 (pr2 x))

      f-nat : is-natural-transformation-Precategory V⁰/X V⁰/X loop1 (id-functor-Precategory V⁰/X) f
      f-nat {A} {B} g =
        eq-hom-Slice-Precategory (V⁰-Precategory i) X
          {obj-functor-Precategory V⁰/X V⁰/X loop1 A} {B}
          (comp-hom-Precategory V⁰/X {obj-functor-Precategory V⁰/X V⁰/X loop1 A} {A} {B} g (f A))
          (comp-hom-Precategory V⁰/X
            {obj-functor-Precategory V⁰/X V⁰/X loop1 A} {obj-functor-Precategory V⁰/X V⁰/X loop1 B} {B}
            (f B)
            (hom-functor-Precategory V⁰/X V⁰/X loop1 {A} {B} g))
          refl

      f-inv : (Y : obj-Precategory V⁰/X) → hom-Precategory V⁰/X Y (obj-functor-Precategory V⁰/X V⁰/X loop1 Y)
      f-inv (Y , π) = (λ y → π y , y , refl) , refl

      f-inv-f : (Y : obj-Precategory V⁰/X) (y : El⁰ (pr1 (obj-functor-Precategory V⁰/X V⁰/X loop1 Y)))
        → (pr1 (f-inv Y) ∘ pr1 (f Y)) y ＝ y
      f-inv-f Y (x , y , refl) = refl

      f-iso : is-natural-isomorphism-Precategory V⁰/X V⁰/X loop1 (id-functor-Precategory V⁰/X) (f , λ {A} {B} → f-nat {A} {B})
      f-iso Y =
        f-inv Y ,
        eq-hom-Slice-Precategory (V⁰-Precategory i) X
          {Y} {Y}
          (comp-hom-Precategory V⁰/X {Y} {obj-functor-Precategory V⁰/X V⁰/X loop1 Y} {Y} (f Y) (f-inv Y))
          (id-hom-Precategory V⁰/X {Y})
          refl ,
        eq-hom-Slice-Precategory (V⁰-Precategory i) X
          {obj-functor-Precategory V⁰/X V⁰/X loop1 Y} {obj-functor-Precategory V⁰/X V⁰/X loop1 Y}
          (comp-hom-Precategory V⁰/X {obj-functor-Precategory V⁰/X V⁰/X loop1 Y} {Y} {obj-functor-Precategory V⁰/X V⁰/X loop1 Y}
            (f-inv Y) (f Y))
          (id-hom-Precategory V⁰/X {obj-functor-Precategory V⁰/X V⁰/X loop1 Y})
          (eq-htpy (f-inv-f Y))

  loop2 : functor-Precategory X→V⁰ X→V⁰
  loop2 = comp-functor-Precategory X→V⁰ V⁰/X X→V⁰ V⁰/X-to-X→V⁰ X→V⁰-to-V⁰/X

  β : natural-isomorphism-Precategory X→V⁰ X→V⁰ loop2 (id-functor-Precategory X→V⁰)
  β = ((f , λ {F} {G} → f-nat {F} {G}) , f-iso)
    where
      f : (F : obj-Precategory X→V⁰) → hom-Precategory X→V⁰ (obj-functor-Precategory X→V⁰ X→V⁰ loop2 F) F
      pr1 (f F) x ((a , b) , refl) = b
      pr2 (f F) refl = eq-htpy λ { ((a , b) , refl) →
        htpy-eq (preserves-id-functor-Precategory X-Precategory (V⁰-Precategory i) F a) b}

      f-nat : is-natural-transformation-Precategory X→V⁰ X→V⁰ loop2 (id-functor-Precategory X→V⁰) f
      f-nat {F} {G} g =
        eq-htpy-hom-family-natural-transformation-Precategory X-Precategory
          (V⁰-Precategory i) (obj-functor-Precategory X→V⁰ X→V⁰ loop2 F) G
          (comp-hom-Precategory X→V⁰ {obj-functor-Precategory X→V⁰ X→V⁰ loop2 F} {F} {G} g (f F))
          (comp-hom-Precategory X→V⁰ {obj-functor-Precategory X→V⁰ X→V⁰ loop2 F} {obj-functor-Precategory X→V⁰ X→V⁰ loop2 G} {G}
            (f G) (hom-functor-Precategory X→V⁰ X→V⁰ loop2 {F} {G} g))
          (λ x → eq-htpy (λ { ((a , b) , refl) → refl}))

      f-inv : (F : obj-Precategory X→V⁰) → hom-Precategory X→V⁰ F (obj-functor-Precategory X→V⁰ X→V⁰ loop2 F)
      pr1 (f-inv F) x a = (x , a) , refl
      pr2 (f-inv F) {x} refl =
        eq-htpy λ a →
          eq-pair-Σ
            (eq-pair-Σ refl (inv (htpy-eq (preserves-id-functor-Precategory X-Precategory (V⁰-Precategory i) F x) a)))
            (eq-is-prop (is-set-El⁰ X x _))

      f-iso : is-natural-isomorphism-Precategory X→V⁰ X→V⁰ loop2 (id-functor-Precategory X→V⁰) (f , (λ {F} {G} → f-nat {F} {G}))
      f-iso F =
        f-inv F ,
        eq-htpy-hom-family-natural-transformation-Precategory X-Precategory (V⁰-Precategory i) F F
          (comp-hom-Precategory X→V⁰ {F} {obj-functor-Precategory X→V⁰ X→V⁰ loop2 F} {F} (f F) (f-inv F))
          (id-hom-Precategory X→V⁰ {F})
          refl-htpy ,
        eq-htpy-hom-family-natural-transformation-Precategory X-Precategory (V⁰-Precategory i)
          (obj-functor-Precategory X→V⁰ X→V⁰ loop2 F) (obj-functor-Precategory X→V⁰ X→V⁰ loop2 F)
          (comp-hom-Precategory X→V⁰
            {obj-functor-Precategory X→V⁰ X→V⁰ loop2 F} {F} {obj-functor-Precategory X→V⁰ X→V⁰ loop2 F}
            (f-inv F) (f F))
          (id-hom-Precategory X→V⁰ {obj-functor-Precategory X→V⁰ X→V⁰ loop2 F})
          (λ x → eq-htpy (λ {((a , b) , refl) → refl}))

  X→V⁰≃V⁰/X : equiv-Precategory X→V⁰ V⁰/X
  X→V⁰≃V⁰/X = X→V⁰-to-V⁰/X , (V⁰/X-to-X→V⁰ , β) , (V⁰/X-to-X→V⁰ , α)