open import 1Lab.Path.IdentitySystem
open import 1Lab.Function.Embedding
open import 1Lab.HLevel.Closure
open import 1Lab.Type.Sigma
open import 1Lab.Type.Pi
open import 1Lab.HLevel
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

module 1Lab.Type.Sigma.Basis where

Σ-bases of types🔗

Like most type formers, $Σ$ types have a universal property: for every pair of functions $f : X \to A,$ $g : (x : A) \to B (f x),$ there is a unique universal map $⟨ f, g ⟩ : X \to Σ A B$ that commutes with first and second projections. In other words, a $Σ$ type is the universal type equipped with a pair of projections $π_{1} : Σ A B \to A,$ $π_{2} : (ab : Σ A B) \to B (π_{1} ab) .$

This means that “being a $Σ$ type” is a property of a type $X$ equipped with a pair of functions $p_{1} : X \to A,$ $p_{2} : (x : X) \to B (p_{1} x) .$ This leads us to the following notion.

private variable
  ℓ ℓ' ℓ'' : Level
  T A A' X X' Y Y' Z Z' : Type ℓ
  B P Q : A → Type ℓ
  p₁ : X → A
  p₂ : (x : X) → B (p₁ x)

A pair of functions $p_{1} : X \to A,$ $p_{2} : (x : X) \to B (p_{1} x)$ form a $Σ -basis$ of $X$ when the induced map $⟨ p_{1}, p_{2} ⟩ : X \to Σ A B$ is an equivalence.

record is-Σ-basis
  {ℓa ℓb ℓx}
  (X : Type ℓx)
  (A : Type ℓa) (B : A → Type ℓb)
  (p₁ : X → A) (p₂ : (x : X) → B (p₁ x))
  : Type (ℓa ⊔ ℓb ⊔ ℓx) where
  field
    ⟨⟩-equiv : is-equiv {B = Σ A B} ⟨ p₁ , p₂ ⟩

The intuition behind the name “basis” is that a choice of $Σ -basis$ of $X$ allows us to write elements of $X$ as a sum of elements of $B (a) .$

  basis : X ≃ Σ A B
  basis = _ , ⟨⟩-equiv

  module basis = Equiv basis

Likewise, an $(A, B)$ $Σ -basis$ of $X$ consists of a pair of maps $p_{1} : X \to A, p_{2} : (x : X) \to B (p_{1} x)$ that form a $Σ -basis$ of $X .$

record Σ-basis
  {ℓa ℓb ℓx}
  (X : Type ℓx)
  (A : Type ℓa) (B : A → Type ℓb)
  : Type (ℓa ⊔ ℓb ⊔ ℓx) where
  field
    proj₁ : X → A
    proj₂ : (x : X) → B (proj₁ x)
    has-basis : is-Σ-basis X A B proj₁ proj₂

  open is-Σ-basis has-basis public

Note that we could have equivalently defined $Σ -bases$ in terms of a single map $X \to Σ A B .$

is-equiv→is-Σ-basis
  : ∀ {f : X → Σ A B}
  → is-equiv f
  → is-Σ-basis X A B (fst ∘ f) (snd ∘ f)
is-equiv→is-Σ-basis eqv .is-Σ-basis.⟨⟩-equiv .is-eqv ab = eqv .is-eqv ab

Equiv→Σ-basis
  : X ≃ Σ A B
  → Σ-basis X A B
Equiv→Σ-basis f .Σ-basis.proj₁ x = fst (Equiv.to f x)
Equiv→Σ-basis f .Σ-basis.proj₂ x = snd (Equiv.to f x)
Equiv→Σ-basis f .Σ-basis.has-basis = is-equiv→is-Σ-basis (f .snd)

is-iso→is-Σ-basis
  : {p₁ : X → A} {p₂ : (x : X) → B (p₁ x)}
  → is-iso {B = Σ A B} ⟨ p₁ , p₂ ⟩
  → is-Σ-basis X A B p₁ p₂
is-iso→is-Σ-basis isom .is-Σ-basis.⟨⟩-equiv = is-iso→is-equiv isom

is-Σ-basis→Σ-basis
  : {p₁ : X → A} {p₂ : (x : X) → B (p₁ x)}
  → is-Σ-basis X A B p₁ p₂
  → Σ-basis X A B
is-Σ-basis→Σ-basis p₁-p₂-basis = record { has-basis = p₁-p₂-basis }
{-# INLINE is-Σ-basis→Σ-basis #-}

Iso→Σ-basis
  : Iso X (Σ A B)
  → Σ-basis X A B
Iso→Σ-basis f = Equiv→Σ-basis (Iso→Equiv f)
{-# INLINE Iso→Σ-basis #-}

Examples of Σ-bases🔗

module _ where
  open is-Σ-basis

The first and second projections out of $Σ A B$ form an $(A, B)$ $Σ -basis.$

  fst-snd-is-Σ-basis : is-Σ-basis (Σ A B) A B fst snd
  fst-snd-is-Σ-basis .⟨⟩-equiv = id-equiv

More interestingly, if $p_{1} : X \to A, p_{2} : (x : X) \to B (p_{1} x)$ form a $Σ -basis$ of $X,$ then $ap p_{1}$ and $ap p_{2}$ form a $Σ -basis$ for the path space of $X .$

  ap-is-Σ-basis
    : {p₁ : X → A} {p₂ : (x : X) → B (p₁ x)}
    → ∀ {x y : X}
    → is-Σ-basis X A B p₁ p₂
    → is-Σ-basis (x ≡ y) (p₁ x ≡ p₁ y) (λ p → PathP (λ i → B (p i)) (p₂ x) (p₂ y))
        (ap p₁)
        (ap p₂)

The proof is a nice equivalence chase. Our ultimate goal is to show that $⟨ ap p_{1}, ap p_{2} ⟩ : Path X x y \to Path Σ A B p_{1} x, p_{2} x p_{1} y, p_{2} y$ is an equivalence. However, we know that paths in $Σ$ types are equivalent to pairs of paths, so we can use 2-for-3 for equivalences to reduce the problem to showing that $ap ⟨ p_{1}, p_{2} ⟩ : Path X x y \to Σ (p : Path A p_{1} x p_{1} y) PathP λi B (p i) p_{2} x p_{2} y$ is an equivalence. This just is another way of asking that $⟨ p_{1}, p_{2} ⟩$ is an embedding, and every equivalence is an embedding!

  ap-is-Σ-basis {p₁ = p₁} {p₂ = p₂} {x = x} {y = y} ΣX .⟨⟩-equiv =
    is-equiv ⟨ ap p₁ , ap p₂ ⟩ ←⟨ equiv-cancell (Σ-pathp≃ .snd) ⟩
    is-equiv (ap ⟨ p₁ , p₂ ⟩)  ←⟨ equiv→cancellable ⟩
    is-equiv ⟨ p₁ , p₂ ⟩       ←⟨ ΣX .⟨⟩-equiv ⟩∎

We can also lift $Σ -bases$ to function types: if $p_{1} : Y \to A, p_{2} : (y : Y) \to B (p_{1} y)$ form a $Σ -basis$ for $Y,$ then $p_{1} \circ (-) : (X \to Y) \to (X \to Y)$ and $p_{2} \circ (-) : (f : X \to Y) \to (X \to B (f x))$ form a $Σ -basis$ for $X \to Y .$

  postcompose-is-Σ-basis
    : {p₁ : Y → A} {p₂ : (y : Y) → B (p₁ y)}
    → is-Σ-basis Y A B p₁ p₂
    → is-Σ-basis (X → Y) (X → A) (λ f → (x : X) → B (f x)) (p₁ ∘_) (p₂ ∘_)

This follows a similar line of reasoning as the previous proof. We start by using 2-for-3 for equivalences to distribute the postcomposition out of the universal map. Next, precomposition by an equivalence is itself an equivalence, so it suffices to show that $⟨ p_{1}, p_{2} ⟩$ is an equivalence, which is exactly our hypothesis.

  postcompose-is-Σ-basis {Y = Y} {A = A} {B = B} {X = X} {p₁ = p₁} {p₂ = p₂} ΣY .⟨⟩-equiv =
    is-equiv ⟨ p₁ ∘_ , p₂ ∘_ ⟩ ←⟨ equiv-cancell (inverse-is-equiv (Σ-Π-distrib .snd)) ⟩
    is-equiv (⟨ p₁ , p₂ ⟩ ∘_)  ←⟨ precompose-is-equiv ⟩
    is-equiv ⟨ p₁ , p₂ ⟩       ←⟨ ΣY .⟨⟩-equiv ⟩∎

Combining Σ-bases🔗

The following series of lemmas describe various ways we can combine $Σ -bases.$

module _
  {ℓx ℓp ℓa ℓb ℓc ℓd}
  {X : Type ℓx} {P : X → Type ℓp}
  {A : Type ℓa} {B : A → Type ℓb}
  {C : (a : A) → Type ℓc} {D : (a : A) → B a → C a → Type ℓd}
  where
  open Σ-basis

If $X : Type$ has a $(A, B)$ $Σ -basis,$ and $P : X \to Type$ has a $(C (p_{1} x), D (p_{1} x))$ $Σ -basis$ for every $x : X,$ then $Σ XP$ can be equipped with a $(a, c) : Σ A C, B a \times D a c$ $Σ$ basis.

  Σ-basis-swap₂
    : (ΣX : Σ-basis X A B)
    → (ΣP : ∀ x → Σ-basis (P x) (C (ΣX .proj₁ x)) (D (ΣX .proj₁ x) (ΣX .proj₂ x)))
    → Σ-basis (Σ X P) (Σ A C) (λ ac → Σ[ b ∈ B (ac .fst) ] D (ac .fst) b (ac .snd))

The key here is that the $Σ$ basis of $P x$ is only allowed depend on the first component of the $Σ -basis$ of $X,$ so we can commute the $B a$ and $C a$ components of the iterated $Σ$ type we get after expanding out $Σ XP .$

  Σ-basis-swap₂ ΣX ΣP =
    Equiv→Σ-basis $
      Σ X P                                        ≃⟨ Σ-ap (basis ΣX) (λ x → basis (ΣP x)) ⟩
      Σ[ (a , b) ∈ Σ A B ] Σ[ c ∈ C a ] D a b c    ≃˘⟨ Σ-assoc ⟩
      Σ[ a ∈ A ] Σ[ b ∈ B a ] Σ[ c ∈ C a ] D a b c ≃⟨ Σ-ap-snd (λ a → Σ-swap₂) ⟩
      Σ[ a ∈ A ] Σ[ c ∈ C a ] Σ[ b ∈ B a ] D a b c ≃⟨ Σ-assoc ⟩
      Σ[ (a , c) ∈ Σ A C ] Σ[ b ∈ B a ] D a b c    ≃∎

module _
  {ℓx ℓa ℓb ℓy ℓc ℓd ℓz ℓe ℓf}
  {X : Type ℓx} {A : Type ℓa} {B : A → Type ℓb}
  {Y : Type ℓy} {C : Type ℓc} {D : C → Type ℓd}
  {Z : Y → Type ℓz} {E : (c : C) → Type ℓe} {F : (c : C) → D c → E c → Type ℓf}
  where
  open Σ-basis

Our previous lemma gives us a useful technique for constructing $Σ -bases.$ To show that $X$ has a $(Y, Z)$ $Σ -basis,$ it suffices to show that:

$X$ has a $(A, B)$ basis; and
$Y$ has a $(C, E)$ basis; and
For every $y : Y,$ $Z y$ has a $(d : D (p_{1} y), F (p_{1} y) d (p_{2} y))$ basis; and
$A$ has a $(C, D)$ basis; and finally
for every $a : A,$ $B a$ has a $(e : E a, F (p_{1} a) (p_{2} a) e) .$

This is particularly useful for constructing $Σ -bases$ of record types whose first and second components are also record types: the first three $Σ$ bases for $X,$ $Y,$ and $Z$ let us give decompositions of record types into $Σ$ types, and the final two $Σ$ bases let us re-arrange the components of those decompositions back into place.

  Σ-basis-shuffle
     : (ΣX : Σ-basis X A B)
     → (ΣY : Σ-basis Y C E)
     → (ΣZ : ∀ {y} → Σ-basis (Z y) (D (ΣY .proj₁ y)) (λ d → F (ΣY .proj₁ y) d (ΣY .proj₂ y)))
     → (ΣA : Σ-basis A C D)
     → (ΣB : ∀ {a} → Σ-basis (B a) (E (ΣA .proj₁ a)) λ e → F (ΣA .proj₁ a) (ΣA .proj₂ a) e)
     → Σ-basis X Y Z
  Σ-basis-shuffle ΣX ΣY ΣZ ΣA ΣB =
    Equiv→Σ-basis $
      X                                         ≃⟨ basis ΣX ⟩
      Σ A B                                     ≃⟨ basis (Σ-basis-swap₂ ΣA (λ a → ΣB)) ⟩
      Σ[ (c , e) ∈ Σ C E ] Σ[ d ∈ D c ] F c d e ≃˘⟨ Σ-ap (basis ΣY) (λ _ → basis ΣZ) ⟩
      Σ Y Z                                     ≃∎

-- Bundled forms of is-Σ-basis results.
module _ where
  open Σ-basis

  Σ-Σ-basis : Σ-basis (Σ A B) A B
  Σ-Σ-basis = is-Σ-basis→Σ-basis fst-snd-is-Σ-basis
  {-# INLINE Σ-Σ-basis #-}

  Path-Σ-basis
    : {x y : X}
    → (ΣX : Σ-basis X A B)
    → Σ-basis (x ≡ y)
        (ΣX .proj₁ x ≡ ΣX .proj₁ y)
        (λ p → PathP (λ i → B (p i)) (ΣX .proj₂ x) (ΣX .proj₂ y))
  Path-Σ-basis ΣX = is-Σ-basis→Σ-basis (ap-is-Σ-basis (ΣX .has-basis))
  {-# INLINE Path-Σ-basis #-}

Σ-bases and h-levels🔗

A $Σ -basis$ is an encoding of an equivalence $X ≃ Σ A B,$ so we can use them to characterise the h-levels of types.

  Σ-basis→is-hlevel
    : (n : Nat)
    → Σ-basis X A B
    → (is-hlevel A n)
    → (∀ (a : A) → is-hlevel (B a) n)
    → is-hlevel X n

  Σ-basis→is-contr
    : Σ-basis X A B
    → (A-contr : is-contr A)
    → (B-contr : is-contr (B (A-contr .centre)))
    → is-contr X

The proofs of these facts are straightforward: h-levels are invariant under equivalences, and we can characterise the h-levels of $Σ$ types via their components.

  Σ-basis→is-hlevel n ΣX A-hl B-hl =
    Equiv→is-hlevel n (basis ΣX) $
    Σ-is-hlevel n A-hl B-hl

  Σ-basis→is-contr ΣX A-contr B-contr =
    Equiv→is-hlevel 0 (basis ΣX) (Σ-is-contr A-contr B-contr)

Σ-bases and identity systems🔗

Every $(A, B)$ $Σ -basis$ for a type induces an identity system on $X,$ where paths are coded by a path in $A$ and a path over that path in $B .$

  is-Σ-basis→identity-system
    : {p₁ : X → A} {p₂ : (x : X) → B (p₁ x)}
    → is-Σ-basis X A B p₁ p₂
    → is-identity-system
        (λ x y → Σ[ p ∈ p₁ x ≡ p₁ y ] PathP (λ i → B (p i)) (p₂ x) (p₂ y))
        (λ x → refl , refl)
  is-Σ-basis→identity-system {p₁ = p₁} {p₂ = p₂} ΣX =
    equiv-path→identity-system $
    (⟨ ap p₁ , ap p₂ ⟩ , ap-is-Σ-basis ΣX .is-Σ-basis.⟨⟩-equiv) e⁻¹

module _
  {R : X → X → Type ℓ} {S : A → A → Type ℓ'} {T : ∀ {a a'} → B a → B a' → S a a' → Type ℓ''}
  {r : (x : X) → R x x} {s : (a : A) → S a a}
  where
  open Σ-basis

We can generalize the previous lemma to get a general strategy for forming identity systems via $Σ -bases.$ To start, let $X$ be a type with an $(A, B)$ $Σ -basis,$ and $R : X \to X \to Type$ be a correspondence on $X$ that has an $(S (p_{1} x) (p_{1} y), T (p_{1} x) (p_{1} y) (p_{2} x) (p_{2} y))$ $Σ -basis,$ where $S : A \to A \to Type$ and $T : (a a^{'} : A) \to B a \to B a^{'} \to S a a^{'} \to Type .$

If there is some $s : (a : A) \to S a a$ such that $(S, s)$ is an identity system and $Σ (b^{'} : B a^{'}), T a a^{'} b b^{'} p$ is a proposition for all $a, a^{'} : A$ and $p : S a a^{'},$ then $(R, r)$ is an identity system on $X .$

  Σ-basis→total-identity-system
    : (ΣX : Σ-basis X A B)
    → (ΣR : ∀ {x y} → Σ-basis (R x y) (S (ΣX .proj₁ x) (ΣX .proj₁ y)) (T (ΣX .proj₂ x) (ΣX .proj₂ y)))
    → is-identity-system S s
    → (∀ {a a'} → (p : S a a') (b : B a) → is-prop (Σ[ b' ∈ B a' ] T b b' p))
    → is-identity-system R r

The type signature of this lemma is scarier than the proof. To start, recall that $(R, r)$ is an identity system on $X$ if and only if the type $Σ (y : X), (R x y)$ is a proposition for every $x : X .$ We shall proceed by constructing a $Σ$ basis on $Σ (y : X), (R x y) .$

Our assumptions state that $X$ has a $Σ -basis,$ and $R x y$ has a $Σ -base$ for every $y : X .$ Moreover, the first component of the basis of $R x y$ is $S (p_{1} x) (p_{1} y),$ which does not depend on the second component of the basis of $X .$ This means that $(Σ (a : A), (S (p_{1} x) a)), λ (a, p) \to Σ (b : B a), (T (p_{1} x) a (p_{2} x) b p)$ forms a $Σ -basis$ for $Σ (y : X), R x y .$ Finally, $(Σ (a : A), (S (p_{1} x) a))$ is contractible, as $(S, s)$ is an identity system, and $Σ (b : B a), (T (p_{1} x) (p_{1} x) (p_{2} x) (p_{2} x) (s (p_{1} x)))$ is a proposition by our assumptions, so $(Σ (a : A), (S (p_{1} x) a)), λ (a, p) \to Σ (b : B a), (T (p_{1} x) a (p_{2} x) b p)$ must be a proposition, which in turn implies that must $Σ (y : X), R x y$ also be a proposition.

  Σ-basis→total-identity-system ΣX ΣR ids idt =
    singleton-prop→identity-system λ {x} →
    Σ-basis→is-hlevel 1
      (R-singleton-Σ-basis x)
      (is-contr→is-prop (is-contr-ΣR ids))
      (λ as → idt (as .snd) (ΣX .proj₂ x))
    where
      R-singleton-Σ-basis
        : ∀ (x : X)
        → Σ-basis (Σ X (R x))
           (Σ[ a ∈ A ] S (ΣX .proj₁ x) a)
           (λ (a , c) → Σ[ b ∈ B a ] T (ΣX .proj₂ x) b c)
      R-singleton-Σ-basis x = Σ-basis-swap₂ ΣX (λ y → ΣR {x} {y})

Reasoning🔗

module _ {ℓx ℓa ℓb} {X : Type ℓx} {A : Type ℓa} {B : A → Type ℓb} where
  open Σ-basis

  record Σ-basis-path (ΣX : Σ-basis X A B) {a a' : A} (b : B a) (b' : B a') : Type ℓx where
    no-eta-equality
    field
      path : basis.from ΣX (a , b) ≡ basis.from ΣX (a' , b')

    base : a ≡ a'
    base = ap fst $ Equiv.injective (basis ΣX e⁻¹) path

    over : PathP (λ i → B (base i)) b b'
    over = ap snd $ Equiv.injective (basis ΣX e⁻¹) path

  open Σ-basis-path

  via-Σ-basis
    : {a a' : A} {b : B a} {b' : B a'}
    → (ΣX : Σ-basis X A B)
    → (p : Σ-basis-path ΣX b b')
    → PathP (λ i → B (base p i)) b b'
  via-Σ-basis ΣX p = over p

  Σ-basis-path-step
    : {ΣX : Σ-basis X A B}
    → ∀ {a a' a''} {b' : B a'} {b'' : B a''}
    → (b : B a)
    → Σ-basis-path ΣX b' b''
    → basis.from ΣX (a , b) ≡ basis.from ΣX (a' , b')
    → Σ-basis-path ΣX b b''
  Σ-basis-path-step {ΣX = ΣX} b q p .Σ-basis-path.path = p ∙ q .path

  _∎Σ : ∀ {ΣX : Σ-basis X A B} {a : A} (b : B a) → Σ-basis-path ΣX b b
  b ∎Σ = record { path = refl }

  syntax Σ-basis-path-step b q p = b ≡Σ⟨ p ⟩ q

  infixr 2 Σ-basis-path-step
  infix 3 _∎Σ