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

open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.cartesian-product-types
open import foundation.contractible-maps
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.equivalences
open import foundation.fibers-of-maps
open import foundation.function-types
open import foundation.function-extensionality
open import foundation.functoriality-cartesian-product-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.logical-equivalences
open import foundation.postcomposition-functions
open import foundation.propositions
open import foundation.raising-universe-levels
open import foundation.slice
open import foundation.small-types
open import foundation.structure-identity-principle
open import foundation.subtypes
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)
open import foundation.type-arithmetic-cartesian-product-types
open import foundation.type-arithmetic-dependent-function-types
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.type-duality
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 e-structure.core
open import functor.n-slice
open import functor.slice
open import notation

module e-structure.u-like where

_-like_ : {i j : Level} (k : Level) → Σ (UU i) (λ M → M → M → UU j) → UU (i ⊔ j ⊔ lsuc k)
k -like (M , _∈_) = (x : M) → is-small k (Σ M λ y → y ∈ x)

is-prop-U-like : {i j : Level} (k : Level) (s : Σ (UU i) (λ M → M → M → UU j))
               → is-prop (k -like s)
is-prop-U-like k (M , _∈_) = is-prop-Π (λ x → is-prop-is-small k (Σ M λ y → y ∈ x))


-- Having a T∞-coalgebra structure on M is the same as having
-- a U-like binary relation on M
module _ {i} (M : UU i) (k : Level) where

  equiv-T∞-Coalg-U-like : (M → T∞ k M)
                       ≃ Σ (M → M → UU (i ⊔ k)) (λ _∈_ → k -like (M , _∈_))
  equiv-T∞-Coalg-U-like =
    equivalence-reasoning

      (M → T∞ k M)

        ≃ (M → Σ (UU k) λ X →
               Σ (UU (i ⊔ k)) (λ X' →
                 (X' ≃ X) × (X' → M)))        by equiv-postcomp M
                                                   (equiv-tot (λ X →
                                                     associative-Σ _ _ _ ∘e
                                                     (inv-left-unit-law-Σ-is-contr
                                                       (is-contr-equiv _
                                                         (equiv-tot (λ X' → equiv-postcomp-equiv (compute-raise (i ⊔ k) X) X'))
                                                         (is-torsorial-equiv' (raise (i ⊔ k) X)))
                                                       (raise (i ⊔ k) X , inv-equiv (compute-raise (i ⊔ k) X)) ∘e
                                                     equiv-precomp (inv-equiv (compute-raise (i ⊔ k) X)) M)))
        ≃ (M → Σ (T∞ (i ⊔ k) M) (λ (X' , _) →
                 is-small k X'))              by equiv-postcomp M
                                                   (inv-associative-Σ _ _ _ ∘e
                                                   (equiv-tot (λ X' → equiv-left-swap-Σ ∘e equiv-tot (λ X → commutative-prod)) ∘e
                                                   equiv-left-swap-Σ))
        ≃ (M → Σ (M → UU (i ⊔ k)) (λ F →
                 is-small k (Σ M F)))         by equiv-postcomp M
                                                   (equiv-Σ _
                                                     (equiv-Fiber k M)
                                                     (λ (X , f) → equiv-tot (equiv-precomp-equiv (equiv-total-fiber f))))
        ≃ Σ (M → M → UU (i ⊔ k)) (λ R →
            (x : M) → is-small k (Σ M (R x))) by distributive-Π-Σ

        ≃ Σ (M → M → UU (i ⊔ k)) (λ _∈_ →
            k -like (M , _∈_))                by equiv-Σ-equiv-base _ equiv-swap-Π

  comp-equiv-T∞-Coalg-U-like' : (m : M → T∞ k M)
                             → map-equiv equiv-T∞-Coalg-U-like m
                             == ((λ y x → fiber (pr2 (m x) ∘ map-inv-raise {i ⊔ k}) y) ,
                                 (λ x → (pr1 (m x)) , (inv-equiv (compute-raise (i ⊔ k) (pr1 (m x))) ∘e equiv-total-fiber (pr2 (m x) ∘ map-inv-raise))))
  comp-equiv-T∞-Coalg-U-like' m = refl

  comp-equiv-T∞-Coalg-U-like : (m : M → T∞ k M) (x y : M)
                            → pr1 (map-equiv equiv-T∞-Coalg-U-like m) y x
                            ≃ fiber (pr2 (m x)) y
  comp-equiv-T∞-Coalg-U-like m x y =
    equiv-pr1 (λ a →
      is-contr-map-is-equiv
        (is-equiv-is-invertible
          map-raise
          (is-retraction-map-inv-raise {i ⊔ k})
          is-section-map-inv-raise)
        (pr1 a)) ∘e
    compute-fiber-comp (pr2 (m x)) (map-inv-raise {i ⊔ k}) y

  -- The T∞-coalgebra is an embedding if and only if
  -- the corresponding binary relation is extensional
  module _ (m : M → T∞ k M) where

    equiv-eq-T∞-extensionality-∈ : {x y : M}
                                → (m x == m y)
                                ≃ ((z : M) → fiber (pr2 (m x)) z ≃ fiber (pr2 (m y)) z)
    equiv-eq-T∞-extensionality-∈ {x} {y} =
      equiv-fam-equiv-equiv-slice (pr2 (m x)) (pr2 (m y)) ∘e
      equiv-eq-T∞ (m x) (m y)

    comp-equiv-eq-T∞-extensionality-∈ : {x : M}
                                     → map-equiv (equiv-eq-T∞-extensionality-∈ {x} {x}) refl
                                     == (λ z → id-equiv)
    comp-equiv-eq-T∞-extensionality-∈ =
      eq-htpy (λ z → eq-type-subtype is-equiv-Prop (eq-htpy (α z)))
      where
        α : {x : M} (z : M)
          → pr1 (map-equiv (equiv-fam-equiv-equiv-slice (pr2 (m x)) (pr2 (m x))) (id-equiv , refl-htpy) z)
          ~ id
        α {x} .(pr2 (m x) a) (a , refl) = refl

    htpy-ap-map-extensionality : {x y : M}
                               → (map-equiv (equiv-eq-T∞-extensionality-∈ {x} {y}) ∘ ap m)
                               ~ map-extensionality M (λ y x → fiber (pr2 (m x)) y)
    htpy-ap-map-extensionality refl = comp-equiv-eq-T∞-extensionality-∈

    is-extensional-∈-is-emb-T∞-Coalg : is-emb m
                                     → is-extensional (λ y x → fiber (pr2 (m x)) y)
    is-extensional-∈-is-emb-T∞-Coalg H {x} {y} =
      is-equiv-htpy
       (map-equiv (equiv-eq-T∞-extensionality-∈ {x} {y}) ∘ ap m)
       (inv-htpy htpy-ap-map-extensionality)
       (is-equiv-comp
         (map-equiv equiv-eq-T∞-extensionality-∈)
         (ap m)
         (H x y)
         (is-equiv-map-equiv equiv-eq-T∞-extensionality-∈))

    is-emb-T∞-Coalg-is-extensional-∈ : is-extensional (λ y x → fiber (pr2 (m x)) y)
                                     → is-emb m
    is-emb-T∞-Coalg-is-extensional-∈ H x y =
      is-equiv-right-factor
        (map-equiv (equiv-eq-T∞-extensionality-∈ {x} {y}))
        (ap m)
        (is-equiv-map-equiv equiv-eq-T∞-extensionality-∈)
        (is-equiv-htpy
          (map-extensionality M (λ y x → fiber (pr2 (m x)) y))
          htpy-ap-map-extensionality
          (H {x} {y}))

  equiv-T∞-Coalg-emb-∈-structure : (M ↪ T∞ k M)
                                 ≃ Σ (M → M → UU (i ⊔ k))
                                     (λ _∈_ → (k -like (M , _∈_)) × is-extensional _∈_)
  equiv-T∞-Coalg-emb-∈-structure =
    associative-Σ _ _ _ ∘e
    equiv-subtype-equiv
      equiv-T∞-Coalg-U-like
      is-emb-Prop
      (λ (_∈_ , _) → is-extensional-Prop _∈_)
      (λ m →
        inv-tr
          (λ R → is-emb m ↔ is-extensional R)
          (eq-htpy (λ y → eq-htpy (λ x → eq-equiv _ _ (comp-equiv-T∞-Coalg-U-like m x y))))
          (is-extensional-∈-is-emb-T∞-Coalg m , is-emb-T∞-Coalg-is-extensional-∈ m))

-- Having a Tⁿ-coalgebra structure on M is the same as having
-- a U-like binary relation on M which is (n-1)-truncated
equiv-T-[_]-Coalg-emb-∈-structure : (n : ℕ)
                                  → {i : Level} (M : UU i) (k : Level)
                                  → (M ↪ T-[ n ] k M)
                                  ≃ Σ (M → M → UU (i ⊔ k))
                                      (λ _∈_ → ((k -like (M , _∈_)) × is-extensional _∈_)
                                             × (∀ x y → is-trunc (minus-one n) (y ∈ x)))
equiv-T-[ n ]-Coalg-emb-∈-structure {i} M k =
  equivalence-reasoning
    M ↪ T-[ n ] k M
      ≃ M ↪ Σ (T∞ k M) (λ (A , f) → is-trunc-map (minus-one n) f)     by equiv-Σ _
                                                                           (equiv-postcomp _ (inv-associative-Σ _ _ _))
                                                                           (λ m →
                                                                             equiv-iff
                                                                               (is-emb-Prop m)
                                                                               (is-emb-Prop _)
                                                                               (is-emb-comp (map-inv-associative-Σ _ _ _) m
                                                                                 (is-emb-is-equiv
                                                                                   (is-equiv-map-equiv (inv-associative-Σ _ _ _))))
                                                                               (is-emb-right-factor (map-inv-associative-Σ _ _ _) m
                                                                                 (is-emb-is-equiv
                                                                                   (is-equiv-map-equiv (inv-associative-Σ _ _ _)))))
      ≃ Σ (M ↪ T∞ k M)
          (λ m → ∀ x → is-trunc-map (minus-one n) (pr2 (m 〈 x 〉)))   by inv-equiv
                                                                           (equiv-emb-into-subtype
                                                                             (λ (A , f) → is-trunc-map-Prop (minus-one n) f))
      ≃ Σ (Σ (M → M → UU (i ⊔ k)) (λ _∈_ →
          (k -like (M , _∈_)) × is-extensional _∈_)) (λ (_∈_ , _) →
          ∀ x y → is-trunc (minus-one n) (y ∈ x))                     by equiv-Σ _
                                                                           (equiv-T∞-Coalg-emb-∈-structure M k)
                                                                           (λ m → equiv-Π-equiv-family
                                                                             (λ x → equiv-Π-equiv-family
                                                                               (λ y → equiv-eq (ap (is-trunc (minus-one n))
                                                                                 (eq-equiv _ _
                                                                                   (inv-equiv (comp-equiv-T∞-Coalg-U-like M k (pr1 m) x y)))))))
      ≃ Σ (M → M → UU (i ⊔ k)) (λ _∈_ →
          ((k -like (M , _∈_)) × is-extensional _∈_)
          × (∀ x y → is-trunc (minus-one n) (y ∈ x)))                 by associative-Σ _ _ _