Journal Part III
In this journal we will use Cubical Agda, to use it we have to use the the following flag.
module journal-part-III wherePlan
Journal Part-I contains our introduction to Agda.
Journal Part-II contains our introduction to MLTT in Agda.
Let us discuss some basics concepts of DTT and HoTT (e.g. type judgments)
Now, let us param. the interval in the real line. This serves as the intuition behind the interval type (path type) and the identity type.
Recall there is no inductive definition for (=), there is instead a primary notion of path, and an equality is a non-dependent path. As path stands for heterogeneous equalities.
Path behaves similar as pathovers in HoTT.
The type of paths is denoted by inline_formula not implemented and its endpoints are inline_formula not implemented and inline_formula not implemented.
open import Cubical.Core.Everything_ : (A : Set) (a b : A) → Set_ = PathPaths are (special) lambdas, which makes sense as a path can be seen as a function.
The identity type is denoted by `Path : (A : Set) (a b : A) → Set`.
The interval type comes with structure that forms a bounded distr. lattice.
We have (I, 0,1, ∨, ∧ ), and additionally, an involution operation (¬)
that holds the following equations, of a De Morgan algebra.
This is mentioned in the Cubical Agda documentation.
i0 ∨ i = ii ∨ i1 = i1i ∨ j = j ∨ ii0 ∧ i = i0i1 ∧ i = ii ∧ j = j ∧ i~ (~ i) = ii0 = ~ i1~ (i ∨ j) = ~ i ∧ ~ j~ (i ∧ j) = ~ i ∨ ~ jTo keep short some definitions below, let us define some recurrent variables.
variable ℓ ℓ₁ ℓ₂ ℓ₃ : Level A A' : Type ℓ₁ B : Type ℓ₂ C : Type ℓ₃Reflexivity
This is our first task, first theorem to show. The Path type holds the reflexivity property, and as we will see later, the symmetry and transitivity properties hold as well. So, Path forms as expect an equiv. relation on any type.
refl' : (x : A) → x ≡ xrefl' x i = xReverse
reverse : ∀ {x y : A} → x ≡ y → y ≡ xreverse p = λ i → p (~ i) -- ~ refers to 1-i, recall the invertal I is the inverval [0,1].symInv : {x y : A} (p : x ≡ y) → reverse (reverse p) ≡ psymInv p = refl' pCongruence
formula not implemented
cong' : {x y : A} → (f : A → B) → x ≡ y → f x ≡ f ycong' {x}{y} f p = λ i → f (p i)ap = cong'{--- * Dependent path type. (Path over Path)-- PathP : ∀ {ℓ} (A : I → Type ℓ) → A i0 → A i1 → Type ℓ-}congDep : ∀ {A : Set}{B : A → Set} (f : (x : A) → B x) → ∀ x y → (p : x ≡ y) → PathP (λ i → B (p i)) (f x) (f y)congDep f x y p = λ i → f (p i)apd = congDepcong-refl : (f : A → B) {x : A} → cong' f (refl' x) ≡ refl' (f x)cong-refl f {x} = λ i → refl' (f x)id : ∀ {A : Set} → A → Aid x = xcongId : {x y : A} → (p : x ≡ y) → cong' id p ≡ pcongId p = refl' p_∘_ : (g : B → C) (f : A → B) → A → C(g ∘ f) x = g (f x)cong-comp : (f : A → B) (g : B → C) {x y : A} (p : x ≡ y) → cong' (g ∘ f) p ≡ cong' g (cong' f p)cong-comp f g p = λ _ j → g (f (p j))Function extensionality
funExt : (f g : A → B) → ((x : A) → f x ≡ g x) → (f ≡ g)funExt f g p i = λ x → p x ifunExtDep : ∀ {A : Set}{B : A → Set} (f g : (x : A) → B x) → ((x : A) → f x ≡ g x) → f ≡ gfunExtDep f g p = λ i → λ x → p x iTransport
transport' : A ≡ B → A → Btransport' p a = transp (λ i → p i) i0 a
subst : (B : A → Type ℓ) {x x' : A} → x ≡ x' → B x → B x'subst B u y = transport' (λ i → B (u i)) yConnection square
J : {x : A} → (P : ∀ y → x ≡ y → Type ℓ) → P x (refl' x) → ∀ y → (p : x ≡ y) → P y pJ {x = x} P d y p = transport' (λ i → P (p i) (λ j → p (i ∧ j))) d where {- Connection square p (i ∧ j). -}The corresponding connection square for the maximum operator is:
Path composition
path-comp : ∀ {ℓ}{A : Type ℓ}{x y z : A} → x ≡ y → y ≡ z → x ≡ zpath-comp {A = A}{x = x} p q = subst (λ a → x ≡ a) q p-- There must be a reason why people don't define path-comp as above.-- The proof might have some trade-offs, I don't see at the moment.-- It's important as we are in a proof-relevant theory, so pay attention.path-comp' : ∀ {ℓ}{A : Type ℓ}{x y z : A} → x ≡ y → y ≡ z → x ≡ zpath-comp' {x = x} p q i = hcomp (λ j → λ {(i = i0) → x ; (i = i1) → q j} ) (p i)