# Transport-split type families

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2024-01-31.

module foundation.transport-split-type-families where

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

open import foundation.action-on-equivalences-functions
open import foundation.action-on-identifications-functions
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.equivalence-extensionality
open import foundation.equivalence-injective-type-families
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.fundamental-theorem-of-identity-types
open import foundation.iterated-dependent-product-types
open import foundation.transport-along-identifications
open import foundation.unit-type
open import foundation.univalent-type-families
open import foundation.universal-property-identity-systems
open import foundation.universe-levels

open import foundation-core.embeddings
open import foundation-core.identity-types
open import foundation-core.propositions
open import foundation-core.sections
open import foundation-core.torsorial-type-families


## Idea

A type family B over A is said to be transport-split if the map

  equiv-tr B : x ＝ y → B x ≃ B y


admits a section for every x y : A. By a corollary of the fundamental theorem of identity types every transport-split type family is univalent, meaning that equiv-tr B is in fact an equivalence for all x y : A.

## Definition

### Transport-split type families

is-transport-split :
{l1 l2 : Level} {A : UU l1} → (A → UU l2) → UU (l1 ⊔ l2)
is-transport-split {A = A} B =
(x y : A) → section (λ (p : x ＝ y) → equiv-tr B p)


## Properties

### Transport-split type families are equivalence injective

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

is-equivalence-injective-is-transport-split :
is-transport-split B → is-equivalence-injective B
is-equivalence-injective-is-transport-split s {x} {y} =
map-section (equiv-tr B) (s x y)


### Transport-split type families are univalent

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

is-transport-split-is-univalent :
is-univalent B → is-transport-split B
is-transport-split-is-univalent U x y = section-is-equiv (U x y)

is-univalent-is-transport-split :
is-transport-split B → is-univalent B
is-univalent-is-transport-split s x =
fundamental-theorem-id-section x (λ y → equiv-tr B) (s x)


### The type is-transport-split is a proposition

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

is-proof-irrelevant-is-transport-split :
is-proof-irrelevant (is-transport-split B)
is-proof-irrelevant-is-transport-split s =
is-contr-iterated-Π 2
( λ x y →
is-contr-section-is-equiv (is-univalent-is-transport-split s x y))

is-prop-is-transport-split :
is-prop (is-transport-split B)
is-prop-is-transport-split =
is-prop-is-proof-irrelevant is-proof-irrelevant-is-transport-split


### Assuming the univalence axiom, type families are transport-split if and only if they are embeddings as maps

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

is-emb-is-transport-split : is-transport-split B → is-emb B
is-emb-is-transport-split s =
is-emb-is-univalent (is-univalent-is-transport-split s)

is-transport-split-is-emb : is-emb B → is-transport-split B
is-transport-split-is-emb H =
is-transport-split-is-univalent (is-univalent-is-emb H)


### Transport-split type families satisfy equivalence induction

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2}
(s : is-transport-split B)
where

is-torsorial-fam-equiv-is-transport-split :
{x : A} → is-torsorial (λ y → B x ≃ B y)
is-torsorial-fam-equiv-is-transport-split =
is-torsorial-fam-equiv-is-univalent (is-univalent-is-transport-split s)

dependent-universal-property-identity-system-fam-equiv-is-transport-split :
{x : A} →
dependent-universal-property-identity-system (λ y → B x ≃ B y) id-equiv
dependent-universal-property-identity-system-fam-equiv-is-transport-split =
dependent-universal-property-identity-system-is-torsorial
( id-equiv)
( is-torsorial-fam-equiv-is-transport-split)