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

open import foundation.action-on-identifications-functions
open import foundation.category-of-sets
open import foundation.contractible-maps
open import foundation.contractible-types
open import foundation.dependent-pair-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-dependent-pair-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.propositions
open import foundation.pullbacks
open import foundation.raising-universe-levels
open import foundation.sections
open import foundation.sets
open import foundation.subtypes
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.type-theoretic-principle-of-choice
open import foundation.universal-property-dependent-pair-types
open import foundation.universe-levels

open import category-theory.functors-precategories
open import category-theory.natural-transformations-functors-precategories
open import category-theory.opposite-precategories
open import category-theory.precategories
open import category-theory.precategory-of-elements-of-a-presheaf
open import category-theory.pullbacks-in-precategories

open import type-theories.pi-types-precategories-with-families
open import type-theories.precategories-with-families

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

module iterative.set.cwf-structure where

module _ (i : Level) where

  Ty-V⁰ : functor-Precategory (opposite-Precategory (V⁰-Precategory i)) (Set-Precategory (lsuc i))
  pr1 Ty-V⁰ Γ = hom-set-Set (El⁰-Set i Γ) (V⁰-Set i)
  pr1 (pr2 Ty-V⁰) σ = _∘ σ
  pr1 (pr2 (pr2 Ty-V⁰)) γ σ = refl
  pr2 (pr2 (pr2 Ty-V⁰)) Γ = refl

  Tm-V⁰ : functor-Precategory (opposite-Precategory (precategory-of-elements-presheaf-Precategory (V⁰-Precategory i) Ty-V⁰)) (Set-Precategory (lsuc i))
  pr1 Tm-V⁰ (Γ , A) = raise-Set (lsuc i) (Π-Set' (El⁰ Γ) λ x → El⁰-Set i (A x))
  pr1 (pr2 Tm-V⁰) (σ , refl) (map-raise a) = map-raise (a ∘ σ)
  pr1 (pr2 (pr2 Tm-V⁰)) (γ , refl) (σ , refl) = eq-htpy λ { (map-raise a) → refl }
  pr2 (pr2 (pr2 Tm-V⁰)) (Γ , A) = eq-htpy (λ { (map-raise a) → refl })

  ext-V⁰ : functor-Precategory (precategory-of-elements-presheaf-Precategory (V⁰-Precategory i) Ty-V⁰) (V⁰-Precategory i)
  pr1 ext-V⁰ (Γ , A) = Σ⁰ Γ A
  pr1 (pr2 ext-V⁰) (σ , refl) (x , a) = (σ x , a)
  pr1 (pr2 (pr2 ext-V⁰)) (γ , refl) (σ , refl) = refl
  pr2 (pr2 (pr2 ext-V⁰)) (Γ , A) = refl

  ext-iso-V⁰ : (Δ Γ : obj-Precategory (V⁰-Precategory i))
             → (A : El⁰ Γ → V⁰ i)
             → (El⁰ Δ → Σ (El⁰ Γ) (El⁰ ∘ A))
             ≃ Σ (El⁰ Δ → El⁰ Γ) λ σ → raise (lsuc i) ((x : El⁰ Δ) → El⁰ (A (σ x)))
  pr1 (ext-iso-V⁰ Δ Γ A) σ = (pr1 ∘ σ , map-raise (λ x → pr2 (σ x)))
  pr2 (ext-iso-V⁰ Δ Γ A) =
    is-equiv-is-invertible
      (λ (σ , map-raise-a) x → (σ x , map-inv-raise map-raise-a x))
      (λ { (σ , map-raise a) → refl })
      (λ σ → refl)

  Precategory-With-Families-V⁰ : Precategory-With-Families (lsuc i) i (lsuc i) (lsuc i)
  Precategory-With-Families.ctx-category Precategory-With-Families-V⁰ = V⁰-Precategory i
  Precategory-With-Families.empty-ctx Precategory-With-Families-V⁰ = terminal-obj-Precategory-V⁰ i
  Precategory-With-Families.ty-presheaf Precategory-With-Families-V⁰ = Ty-V⁰
  Precategory-With-Families.tm-presheaf Precategory-With-Families-V⁰ = Tm-V⁰
  Precategory-With-Families.ext-functor Precategory-With-Families-V⁰ = ext-V⁰
  Precategory-With-Families.ext-iso Precategory-With-Families-V⁰ = ext-iso-V⁰
  Precategory-With-Families.ext-iso-nat Precategory-With-Families-V⁰ _ _ _ _ _ _ = refl

  open Precategory-With-Families Precategory-With-Families-V⁰

  Π-structure-V⁰ : Π-structure-Precategory-With-Families (lsuc i) i (lsuc i) (lsuc i) Precategory-With-Families-V⁰
  Π-structure-Precategory-With-Families.Π Π-structure-V⁰ A B x = Π⁰ (A x) (λ a → B (x , a))
  Π-structure-Precategory-With-Families.iso-Π Π-structure-V⁰ A B = equiv-raise (lsuc i) (lsuc i) (inv-equiv equiv-ev-pair)
  Π-structure-Precategory-With-Families.substitution-law-Π Π-structure-V⁰ A B σ = refl
  Π-structure-Precategory-With-Families.substitution-law-iso-Π Π-structure-V⁰ A B σ t =
    ap (λ t' → map-equiv-raise (lsuc i) (lsuc i) (inv-equiv equiv-ev-pair) (t' [ σ ]))
       (inv (is-section-map-inv-raise t)) ∙
    ap (λ t' → map-equiv-raise (lsuc i) (lsuc i) (inv-equiv equiv-ev-pair) t' [ ⟨ σ , A ⟩ ])
       (is-section-map-inv-raise t)