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

open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.fibers-of-maps
open import foundation.function-types
open import foundation.functoriality-dependent-function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.slice
open import foundation.truncated-maps
open import foundation.truncation-levels
  renaming (truncation-level-minus-one-ℕ to minus-one)
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.univalence
open import foundation.universe-levels

open import e-structure.core
open import functor.n-slice
open import functor.slice
open import notation

module fixed-point.internalisations {i j} (n : ℕ)
  (V : UU j) (fixed-point-V : V ≃ T-[ n ] i V) where

-- Construction of ∈-structure on V
open import fixed-point.core n V fixed-point-V

-- Internalisations and representations
open import e-structure.internalisations ∈-structure-V

{- Having an internalisation of a type A in Vⁿ
is equivalent to having an (n-1)-truncated map from A into Vⁿ -}

equiv-internalisation-trunc-map : (A : UU i)
                                → trunc-map (minus-one n) A V
                                ≃ InternalisationOfType A
equiv-internalisation-trunc-map A =
  equivalence-reasoning
    trunc-map (minus-one n) A V
    ≃ Σ (Representation A) InternalisationOfRepr by equiv-tot (λ f →
      equivalence-reasoning
        is-trunc-map (minus-one n) f
        ≃ Σ (Σ (T∞ i V) (_== (A , f))) (λ ((B , g) , _) →
            is-trunc-map (minus-one n) g)         by inv-left-unit-law-Σ-is-contr
                                                       (is-torsorial-path' (A , f))
                                                       ((A , f) , refl)
        ≃ Σ (T-[ n ] i V) (λ (B , g) →
            (B , map-trunc-map g) == (A , f))     by equiv-Σ-equiv-base _ (associative-Σ _ _ _)
                                                     ∘e equiv-right-swap-Σ
        ≃ Σ (T-[ n ] i V) (λ (B , g) →
            Σ (B ≃ A) (λ e →
              map-trunc-map g ~ f ∘ map-equiv e)) by equiv-tot (λ (B , g) →
                                                       equiv-eq-T∞ (B , map-trunc-map g) (A , f))
        ≃ Σ V (λ a →
            Σ (¦ desup a ¦ ≃ A) (λ e →
              map-trunc-map (pr2 (desup a))
              ~ f ∘ map-equiv e))                 by equiv-Σ _
                                                       (inv-equiv fixed-point-V)
                                                       (λ (B , g) → equiv-eq
                                                         (ap (λ ((B' , g'))
                                                           → Σ (B' ≃ A) (λ e → map-trunc-map g' ~ f ∘ map-equiv e))
                                                             (inv (is-section-map-section-map-equiv fixed-point-V (B , g)))))
        ≃ InternalisationOfRepr f                 by equiv-tot (λ a →
                                                       equiv-fam-equiv-equiv-slice
                                                         (map-trunc-map (pr2 (desup a)))
                                                         f))
    ≃ InternalisationOfType A                     by equiv-IntOfRepr-IntOfType A