Structured type duality

module foundation.structured-type-duality where
Imports
open import foundation.equivalences
open import foundation.structure
open import foundation.type-duality
open import foundation.type-theoretic-principle-of-choice
open import foundation.univalence

open import foundation-core.dependent-pair-types
open import foundation-core.fibers-of-maps
open import foundation-core.functions
open import foundation-core.functoriality-dependent-function-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.type-arithmetic-dependent-pair-types
open import foundation-core.universe-levels

Theorem

Structured type duality

Slice-structure :
  {l1 l2 : Level} (l : Level) (P : UU (l1  l)  UU l2) (B : UU l1) 
  UU (l1  l2  lsuc l)
Slice-structure l P B = Σ (UU l)  A  hom-structure P A B)

equiv-Fib-structure :
  {l1 l2 : Level} (l : Level) (P : UU (l1  l)  UU l2) (B : UU l1) 
  Slice-structure (l1  l) P B  fam-structure P B
equiv-Fib-structure {l1} {l3} l P B =
  ( ( inv-distributive-Π-Σ) ∘e
    ( equiv-Σ
      ( λ C  (b : B)  P (C b))
      ( equiv-Fib l B)
      ( λ f  equiv-map-Π  b  id-equiv)))) ∘e
  ( inv-associative-Σ
    ( UU (l1  l))
    ( λ A  A  B)
    ( λ f  structure-map P (pr2 f)))
equiv-fixed-Slice-structure :
  {l : Level} (P : UU l  UU l) (X : UU l) (A : UU l) 
  ( hom-structure P X A) 
  ( Σ (A  Σ (UU l)  Z  P (Z))) ( λ Y  X  (Σ A (pr1  Y))))
equiv-fixed-Slice-structure {l} P X A =
  ( ( equiv-Σ
      ( λ Y  X  Σ A (pr1  Y))
      ( equiv-Fib-structure l P A)
      ( λ s 
        inv-equiv (equiv-postcomp-equiv (equiv-total-fib (pr1 (pr2 s))) X))) ∘e
    ( ( equiv-right-swap-Σ) ∘e
      ( ( inv-left-unit-law-Σ-is-contr
          ( is-contr-total-equiv X)
          ( X , id-equiv)))))