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

open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.natural-numbers

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.embeddings
open import foundation.equality-dependent-pair-types
open import foundation.equivalences
open import foundation.equivalence-extensionality
open import foundation.fibers-of-maps
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.functoriality-dependent-function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.functoriality-function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.locally-small-types
open import foundation.postcomposition-functions
open import foundation.propositional-maps
open import foundation.propositions
open import foundation.sets
open import foundation.transport-along-identifications
open import foundation.truncated-maps
open import foundation.truncated-types
open import foundation.truncation-levels
  renaming (truncation-level-minus-one-β„• to minus-one;
    truncation-level-β„• to to-𝕋)
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.type-theoretic-principle-of-choice
open import foundation.univalence
open import foundation.universal-property-equivalences
open import foundation.universe-levels

open import functor.n-slice
open import image-factorisation
open import notation hiding (sup)

module fixed-point.exponentiation {i j} (n : β„•)
  (V : UU j) (fixed-point-V : V ≃ T-[ n ] i V)
  (ordered-pairs : (V Γ— V) β†ͺ V) where

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

-- Property of having exponentiation
open import e-structure.property.exponentiation ∈-structure-V ordered-pairs

-- Notation for ordered pairs
import e-structure.core
open e-structure.core.ordered-pairing-structure.notation V ordered-pairs

module _ {A : UU i} {B : A β†’ UU i}
  (f : trunc-map (minus-one n) A V)
  (g : βˆ€ a β†’ trunc-map (minus-one n) (B a) V)
  where

  trunc-map-graph : (βˆ€ a β†’ B a)
                  β†’ trunc-map (minus-one n) A V
  trunc-map-graph Ο• =
    comp-trunc-map _
      ((Ξ» (x , y) β†’ ⟨ x , y ⟩) , is-trunc-map-is-prop-map _ (is-prop-map-is-emb (pr2 ordered-pairs)))
      (comp-trunc-map _
        (map-Ξ£ _ (pr1 f) (Ξ» a β†’ pr1 (g a)) , is-trunc-map-map-Ξ£ _ _ (pr2 f) (Ξ» a β†’ pr2 (g a)))
        graph-on-types)
    where
      equiv-fiber-graph-on-types : ((a , b) : Ξ£ A B)
                               β†’ Ξ£ A (Ξ» a' β†’ (a' , Ο• a') == (a , b))
                               ≃ (Ο• a == b)
      equiv-fiber-graph-on-types (a , b) =
        equivalence-reasoning
          Ξ£ A (Ξ» a' β†’ (a' , Ο• a') == (a , b))
            ≃ Ξ£ A (Ξ» a' β†’ Ξ£ (a' == a) (Ξ» Ξ± β†’ tr B Ξ± (Ο• a') == b))        by equiv-tot (Ξ» a' β†’ inv-equiv (equiv-eq-pair-Ξ£ _ _))
            ≃ Ξ£ (Ξ£ A (Ξ» a' β†’ a' == a)) (Ξ» (a' , Ξ±) β†’ tr B Ξ± (Ο• a') == b) by inv-associative-Ξ£ _ _ _
            ≃ (Ο• a == b)                                                 by left-unit-law-Ξ£-is-contr
                                                                              (is-torsorial-path' a) (a , refl)

      graph-on-types : trunc-map (minus-one n) A (Ξ£ A B)
      pr1 graph-on-types a = (a , Ο• a)
      pr2 graph-on-types (a , b) =
        is-trunc-equiv _ _
          (equiv-fiber-graph-on-types (a , b))
          (is-trunc-is-trunc-map-into-is-trunc
            (minus-one n)
            (pr1 (g a))
            is-trunc-V
            (pr2 (g a))
            (Ο• a)
            b)

  graph : (βˆ€ a β†’ B a) β†’ V
  graph Ο• = sup (A , trunc-map-graph Ο•)

  is-trunc-map-graph : is-trunc-map (minus-one n) graph
  is-trunc-map-graph =
    is-trunc-map-is-trunc-map-ap _ graph (Ξ» Ο• ψ β†’
      is-trunc-map-htpy _
        {g = ap sup ∘
             (map-inv-equiv (equiv-eq-T-[ n ] _ _) ∘
             (tot (Ξ» e β†’ ap (pr1 ordered-pairs ∘ map-Ξ£ _ (pr1 f) (pr1 ∘ g)) ∘_) ∘
             map-equiv (e Ο• ψ)))}
        (Ξ» {refl β†’ ap (ap sup) (inv (is-retraction-map-inv-equiv (equiv-eq-T-[ n ] _ _) refl))})
        (is-trunc-map-comp _
          (ap sup)
          _
          (is-trunc-map-is-equiv _
            (is-equiv-map-equiv (equiv-ap (inv-equiv fixed-point-V) _ _)))
          (is-trunc-map-comp _
            (map-inv-equiv (equiv-eq-T-[ n ] _ _))
            _
            (is-trunc-map-is-equiv _ (is-equiv-map-inv-equiv (equiv-eq-T-[ n ] _ _)))
            (is-trunc-map-comp _
              (tot (Ξ» e β†’ ap (pr1 ordered-pairs ∘ map-Ξ£ _ (pr1 f) (pr1 ∘ g)) ∘_))
              (map-equiv (e Ο• ψ))
              (is-trunc-map-tot _ (Ξ» e β†’
                is-trunc-map-map-Ξ  _
                  (Ξ» a β†’ ap (pr1 ordered-pairs ∘ map-Ξ£ _ (pr1 f) (pr1 ∘ g)))
                  (Ξ» a β†’ is-trunc-map-ap-is-trunc-map _
                           (pr1 ordered-pairs ∘ map-Σ _ (pr1 f) (pr1 ∘ g))
                           (is-trunc-map-comp _
                             (pr1 ordered-pairs)
                             (map-Σ _ (pr1 f) (pr1 ∘ g))
                             (is-trunc-map-is-prop-map _
                               (is-prop-map-is-emb (pr2 ordered-pairs)))
                             (is-trunc-map-map-Ξ£ _ _
                               (pr2 f)
                               (pr2 ∘ g)))
                           (a , Ο• a)
                           (map-equiv e a , ψ (map-equiv e a)))))
              (is-trunc-map-is-equiv _ (is-equiv-map-equiv (e Ο• ψ)))))))
    where
      e : (Ο• ψ : βˆ€ a β†’ B a)
        β†’ (Ο• == ψ)
        ≃ Ξ£ (A ≃ A) (Ξ» e β†’
            (a : A) β†’ Id {A = Ξ£ A B} (a , Ο• a) (map-equiv e a , ψ (map-equiv e a)))
      e Ο• ψ =
        equivalence-reasoning
          (Ο• == ψ)

          ≃ (Ο• ~ ψ)                                    by equiv-funext

          ≃ Ξ£ (Ξ£ (A ≃ A) (Ξ» e β†’ id ~ map-equiv e))
              (Ξ» (e , r) β†’ βˆ€ a β†’ tr B (r a) (Ο• a)
                                 == ψ (map-equiv e a)) by inv-left-unit-law-Σ-is-contr
                                                            (is-torsorial-htpy-equiv id-equiv)
                                                            (id-equiv , refl-htpy)
          ≃ Ξ£ (A ≃ A) (Ξ» e β†’ Ξ£ (id ~ map-equiv e)
              Ξ» r β†’ βˆ€ a β†’ tr B (r a) (Ο• a)
                          == ψ (map-equiv e a))        by associative-Σ _ _ _

          ≃ Ξ£ (A ≃ A) (Ξ» e β†’ (a : A) β†’
            Ξ£ (a == map-equiv e a) Ξ» Ξ± β†’
              tr B Ξ± (Ο• a)
              == ψ (map-equiv e a))                    by equiv-tot (Ξ» e β†’ inv-distributive-Ξ -Ξ£)

          ≃ Ξ£ (A ≃ A) (Ξ» e β†’ (a : A) β†’
              (a , Ο• a) ==
              (map-equiv e a , ψ (map-equiv e a)))     by equiv-tot (Ξ» e β†’ equiv-Ξ -equiv-family (Ξ» a β†’
                                                            equiv-eq-pair-Ξ£ (a , Ο• a) (map-equiv e a , ψ (map-equiv e a))))

infix 70 _β‡’_
_β‡’_ : V β†’ V β†’ V
x β‡’ y = sup ((A β†’ B) , graph f (Ξ» _ β†’ g) , is-trunc-map-graph f (Ξ» _ β†’ g))
  where
    A = pr1 (desup x)
    B = pr1 (desup y)
    f = pr2 (desup x)
    g = pr2 (desup y)


∈-β‡’ : (a b z : V)
    β†’ (z ∈ a β‡’ b) ≃ Operation' a b z
∈-β‡’ a b z =
  equivalence-reasoning
    (z ∈ a β‡’ b)

      ≃ Ξ£ (A β†’ B) (Ξ» Ο• β†’ graph f (Ξ» _ β†’ g) Ο• == z)     by equiv-eq (∈-sup z)

      ≃ Ξ£ (A β†’ B) (Ξ» Ο• β†’ z == graph f (Ξ» _ β†’ g) Ο•)     by equiv-tot (Ξ» Ο• β†’ equiv-inv (graph f (Ξ» _ β†’ g) Ο•) z)

      ≃ Ξ£ (A β†’ B) (Ξ» Ο• β†’ (u : V) β†’
          (u ∈ z) ≃ (u ∈ graph f (Ξ» _ β†’ g) Ο•))         by equiv-tot (Ξ» Ο• β†’ equiv-extensionality)

      ≃ Ξ£ (A β†’ B) (Ξ» Ο• β†’ (u : V) β†’
          (u ∈ z) ≃
          Ξ£ A (Ξ» x β†’ ⟨ pr1 f x , pr1 g (Ο• x) ⟩ == u))  by equiv-tot (Ξ» Ο• β†’ equiv-Ξ -equiv-family (Ξ» u β†’
                                                            equiv-postcomp-equiv (equiv-eq (∈-sup u)) (u ∈ z)))
      ≃ Ξ£ (El a β†’ El b) (Ξ» Ο• β†’ (u : V) β†’
          (u ∈ z) ≃
          Ξ£ (El a) (Ξ» x β†’ ⟨ pr1 x , pr1 (Ο• x) ⟩ == u)) by equiv-Ξ£ _
                                                            (equiv-postcomp (El a) (inv-equiv-total-fiber (pr1 g)) ∘e
                                                             equiv-precomp (equiv-total-fiber (pr1 f)) B)
                                                            (Ξ» Ο• β†’ equiv-Ξ -equiv-family (Ξ» u β†’
                                                              equiv-postcomp-equiv
                                                                (equiv-Ξ£-equiv-base
                                                                  (Ξ» x β†’ ⟨ pr1 x , pr1 g (Ο• (pr1 (pr2 x))) ⟩ == u)
                                                                  (inv-equiv-total-fiber (pr1 f)))
                                                                (u ∈ z)))
      ≃ Operation' a b z                               by id-equiv

  where
    A = pr1 (desup a)
    B = pr1 (desup b)
    C = pr1 (desup z)
    f = pr2 (desup a)
    g = pr2 (desup b)
    h = pr2 (desup z)

exponentiation' : Exponentiation'
exponentiation' a b = (a β‡’ b , ∈-β‡’ a b)

exponentiation : Exponentiation
exponentiation =
  map-inv-equiv Exponentiation≃Exponentiation' exponentiation'