# The interval

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-02-09.

module synthetic-homotopy-theory.interval-type where

Imports
open import foundation.action-on-identifications-dependent-functions
open import foundation.action-on-identifications-functions
open import foundation.commuting-squares-of-identifications
open import foundation.contractible-types
open import foundation.dependent-identifications
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.homotopies
open import foundation.identity-types
open import foundation.structure-identity-principle
open import foundation.transport-along-identifications
open import foundation.universe-levels


## Idea

The interval type is a higher inductive type with two points and an identification between them.

## Postulates

postulate

𝕀 : UU lzero

source-𝕀 : 𝕀

target-𝕀 : 𝕀

path-𝕀 : Id source-𝕀 target-𝕀

ind-𝕀 :
{l : Level} (P : 𝕀 → UU l) (u : P source-𝕀) (v : P target-𝕀)
(q : dependent-identification P path-𝕀 u v) → (x : 𝕀) → P x

compute-source-𝕀 :
{l : Level} {P : 𝕀 → UU l} (u : P source-𝕀) (v : P target-𝕀)
(q : dependent-identification P path-𝕀 u v) → Id (ind-𝕀 P u v q source-𝕀) u

compute-target-𝕀 :
{l : Level} {P : 𝕀 → UU l} (u : P source-𝕀) (v : P target-𝕀)
(q : dependent-identification P path-𝕀 u v) → Id (ind-𝕀 P u v q target-𝕀) v

compute-path-𝕀 :
{l : Level} {P : 𝕀 → UU l} (u : P source-𝕀) (v : P target-𝕀)
(q : dependent-identification P path-𝕀 u v) →
coherence-square-identifications
( ap (tr P path-𝕀) (compute-source-𝕀 u v q))
( apd (ind-𝕀 P u v q) path-𝕀)
( q)
( compute-target-𝕀 u v q)


## Properties

### The data that is used to apply the inductiopn principle of the interval

Data-𝕀 : {l : Level} → (𝕀 → UU l) → UU l
Data-𝕀 P =
Σ ( P source-𝕀)
( λ u →
Σ ( P target-𝕀) (dependent-identification P path-𝕀 u))

ev-𝕀 : {l : Level} {P : 𝕀 → UU l} → ((x : 𝕀) → P x) → Data-𝕀 P
ev-𝕀 f = triple (f source-𝕀) (f target-𝕀) (apd f path-𝕀)

module _
{l : Level} {P : 𝕀 → UU l}
where

Eq-Data-𝕀 : (x y : Data-𝕀 P) → UU l
Eq-Data-𝕀 x y =
Σ ( pr1 x ＝ pr1 y)
( λ α →
Σ ( pr1 (pr2 x) ＝ pr1 (pr2 y))
( λ β →
coherence-square-identifications
( ap (tr P path-𝕀) α)
( pr2 (pr2 x))
( pr2 (pr2 y))
( β)))

extensionality-Data-𝕀 : (x y : Data-𝕀 P) → Id x y ≃ Eq-Data-𝕀 x y
extensionality-Data-𝕀 (pair u (pair v α)) =
extensionality-Σ
( λ {u'} vα' p →
Σ ( v ＝ pr1 vα')
( λ q →
coherence-square-identifications
( ap (tr P path-𝕀) p)
( α)
( pr2 vα')
( q)))
( refl)
( pair refl right-unit)
( λ u' → id-equiv)
( extensionality-Σ
( λ {v'} α' q → Id (α ∙ q) α')
( refl)
( right-unit)
( λ v' → id-equiv)
( λ γ → equiv-concat right-unit γ))

refl-Eq-Data-𝕀 : (x : Data-𝕀 P) → Eq-Data-𝕀 x x
refl-Eq-Data-𝕀 x = triple refl refl right-unit

Eq-eq-Data-𝕀 : {x y : Data-𝕀 P} → Id x y → Eq-Data-𝕀 x y
Eq-eq-Data-𝕀 {x = x} refl = refl-Eq-Data-𝕀 x

eq-Eq-Data-𝕀' : {x y : Data-𝕀 P} → Eq-Data-𝕀 x y → Id x y
eq-Eq-Data-𝕀' {x} {y} = map-inv-equiv (extensionality-Data-𝕀 x y)

eq-Eq-Data-𝕀 :
{x y : Data-𝕀 P} (α : pr1 x ＝ pr1 y) (β : pr1 (pr2 x) ＝ pr1 (pr2 y))
(γ :
coherence-square-identifications
( ap (tr P path-𝕀) α)
( pr2 (pr2 x))
( pr2 (pr2 y))
( β)) →
x ＝ y
eq-Eq-Data-𝕀 α β γ = eq-Eq-Data-𝕀' (triple α β γ)


### The interval is contractible

inv-ev-𝕀 : {l : Level} {P : 𝕀 → UU l} → Data-𝕀 P → (x : 𝕀) → P x
inv-ev-𝕀 x = ind-𝕀 _ (pr1 x) (pr1 (pr2 x)) (pr2 (pr2 x))

is-section-inv-ev-𝕀 :
{l : Level} {P : 𝕀 → UU l} (x : Data-𝕀 P) → ev-𝕀 (inv-ev-𝕀 x) ＝ x
is-section-inv-ev-𝕀 (pair u (pair v q)) =
eq-Eq-Data-𝕀
( compute-source-𝕀 u v q)
( compute-target-𝕀 u v q)
( compute-path-𝕀 u v q)

tr-value :
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} (f g : (x : A) → B x) {x y : A}
(p : Id x y) (q : Id (f x) (g x)) (r : Id (f y) (g y)) →
Id (apd f p ∙ r) (ap (tr B p) q ∙ apd g p) →
Id (tr (λ x → Id (f x) (g x)) p q) r
tr-value f g refl q r s = (inv (ap-id q) ∙ inv right-unit) ∙ inv s

is-retraction-inv-ev-𝕀 :
{l : Level} {P : 𝕀 → UU l} (f : (x : 𝕀) → P x) → Id (inv-ev-𝕀 (ev-𝕀 f)) f
is-retraction-inv-ev-𝕀 {l} {P} f =
eq-htpy
( ind-𝕀
( eq-value (inv-ev-𝕀 (ev-𝕀 f)) f)
( compute-source-𝕀 (f source-𝕀) (f target-𝕀) (apd f path-𝕀))
( compute-target-𝕀 (f source-𝕀) (f target-𝕀) (apd f path-𝕀))
( map-compute-dependent-identification-eq-value
( inv-ev-𝕀 (ev-𝕀 f))
( f)
( path-𝕀)
( compute-source-𝕀 (f source-𝕀) (f target-𝕀) (apd f path-𝕀))
( compute-target-𝕀 (f source-𝕀) (f target-𝕀) (apd f path-𝕀))
( compute-path-𝕀 (f source-𝕀) (f target-𝕀) (apd f path-𝕀))))

abstract
is-equiv-ev-𝕀 :
{l : Level} (P : 𝕀 → UU l) → is-equiv (ev-𝕀 {P = P})
is-equiv-ev-𝕀 P =
is-equiv-is-invertible inv-ev-𝕀 is-section-inv-ev-𝕀 is-retraction-inv-ev-𝕀

contraction-𝕀 : (x : 𝕀) → Id source-𝕀 x
contraction-𝕀 =
ind-𝕀
( Id source-𝕀)
( refl)
( path-𝕀)
( tr-Id-right path-𝕀 refl)

abstract
is-contr-𝕀 : is-contr 𝕀
pr1 is-contr-𝕀 = source-𝕀
pr2 is-contr-𝕀 = contraction-𝕀