Equality of dependent pair types

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Eléonore Mangel, Vojtěch Štěpančík, Julian KG, fernabnor, louismntnu and maybemabeline.

Created on 2022-01-26.
Last modified on 2025-01-07.

module foundation.equality-dependent-pair-types where

open import foundation-core.equality-dependent-pair-types public

Imports

open import foundation.action-on-identifications-dependent-functions
open import foundation.action-on-identifications-functions
open import foundation.dependent-identifications
open import foundation.dependent-pair-types
open import foundation.transport-along-identifications
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels

open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.identity-types

Idea

The operation eq-pair-Σ can be seen as a “vertical composition” operation that combines an identification and a dependent identification over it into a single identification. This operation preserves, in the appropriate sense, the groupoidal structure on dependent identifications.

Properties

Interchange law of concatenation and `eq-pair-Σ`

module _
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
  where

  interchange-concat-eq-pair-Σ :
    {x y z : A} (p : x ＝ y) (q : y ＝ z) {x' : B x} {y' : B y} {z' : B z} →
    (p' : dependent-identification B p x' y')
    (q' : dependent-identification B q y' z') →
    eq-pair-Σ (p ∙ q) (concat-dependent-identification B p q p' q') ＝
    ( eq-pair-Σ p p' ∙ eq-pair-Σ q q')
  interchange-concat-eq-pair-Σ refl q refl q' = refl

Interchange law for concatenation and `pair-eq-Σ`

module _
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
  where

  interchange-concat-pair-eq-Σ :
    {x y z : Σ A B} (p : x ＝ y) (q : y ＝ z) →
    pair-eq-Σ (p ∙ q) ＝
    ( pr1 (pair-eq-Σ p) ∙ pr1 (pair-eq-Σ q) ,
      concat-dependent-identification B
        ( pr1 (pair-eq-Σ p))
        ( pr1 (pair-eq-Σ q))
        ( pr2 (pair-eq-Σ p))
        ( pr2 (pair-eq-Σ q)))
  interchange-concat-pair-eq-Σ refl q = refl

  pr1-interchange-concat-pair-eq-Σ :
    {x y z : Σ A B} (p : x ＝ y) (q : y ＝ z) →
    pr1 (pair-eq-Σ (p ∙ q)) ＝ (pr1 (pair-eq-Σ p) ∙ pr1 (pair-eq-Σ q))
  pr1-interchange-concat-pair-eq-Σ p q =
    ap pr1 (interchange-concat-pair-eq-Σ p q)

Distributivity of `inv` over `eq-pair-Σ`

module _
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
  where

  distributive-inv-eq-pair-Σ :
    {x y : A} (p : x ＝ y) {x' : B x} {y' : B y}
    (p' : dependent-identification B p x' y') →
    inv (eq-pair-Σ p p') ＝
    eq-pair-Σ (inv p) (inv-dependent-identification B p p')
  distributive-inv-eq-pair-Σ refl refl = refl

  distributive-inv-eq-pair-Σ-refl :
    {x : A} {x' y' : B x} (p' : x' ＝ y') →
    inv (eq-pair-eq-fiber p') ＝ eq-pair-Σ {A = A} {B = B} refl (inv p')
  distributive-inv-eq-pair-Σ-refl refl = refl

Computing `pair-eq-Σ` at an identification of the form `ap f p`

module _
  {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : A → UU l3} (f : X → Σ A B)
  where

  pair-eq-Σ-ap :
    {x y : X} (p : x ＝ y) →
    pair-eq-Σ (ap f p) ＝
    ( ( ap (pr1 ∘ f) p) ,
      ( substitution-law-tr B (pr1 ∘ f) p ∙ apd (pr2 ∘ f) p))
  pair-eq-Σ-ap refl = refl

  pr1-pair-eq-Σ-ap :
    {x y : X} (p : x ＝ y) →
    pr1 (pair-eq-Σ (ap f p)) ＝ ap (pr1 ∘ f) p
  pr1-pair-eq-Σ-ap refl = refl

Computing action of functions on identifications of the form `eq-pair-Σ p q`

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {Y : UU l3} (f : Σ A B → Y)
  where

  compute-ap-eq-pair-Σ :
    { x y : A} (p : x ＝ y) {b : B x} {b' : B y} →
    ( q : dependent-identification B p b b') →
    ap f (eq-pair-Σ p q) ＝ (ap f (eq-pair-Σ p refl) ∙ ap (ev-pair f y) q)
  compute-ap-eq-pair-Σ refl refl = refl