UniAgda.Core.PathSpaces.Nat

Table of Contents

1 Prelude

2 Paths in Nat

nat-code :     Type lzero
nat-code zero zero = Unit
nat-code zero (suc m) = Empty
nat-code (suc n) zero = Empty
nat-code (suc n) (suc m) = nat-code n m

nat-r : (n : )  nat-code n n
nat-r zero = tt
nat-r (suc n) = nat-r n

nat-encode : (m n : )  m  n  nat-code m n
nat-encode m n p = transport (nat-code m) p (nat-r m)

nat-decode : (m n : )  nat-code m n  m  n
nat-decode zero zero x = refl
nat-decode (suc m) (suc n) x = ap suc (nat-decode m n x)

nat-decode-encode-id : (m n : )  nat-encode m n o nat-decode m n ~ id
nat-decode-encode-id zero zero tt = refl
nat-decode-encode-id (suc m) (suc n) c = (tr-Pf  x  nat-code (suc m) x) suc (nat-decode m n c) (nat-r m)) ^  nat-decode-encode-id m n c


nat-encode-decode-id : (m n : )  nat-decode m n o nat-encode m n ~ id
nat-encode-decode-id zero .zero refl = refl
nat-encode-decode-id (suc m) .(suc m) refl = ap (ap suc ) (nat-encode-decode-id m m refl)

thm2-13-1 : (m n : )  (m  n)  nat-code m n
thm2-13-1 m n = equiv-adjointify (nat-encode m n , (nat-decode m n) ,
                                 nat-decode-encode-id m n , nat-encode-decode-id m n)

coprod-code : {i j : Level} {A : Type i} {B : Type j} (a₀ : A) → A + B → Type (i ⊔ j) coprod-code {i} {j} a₀ (inl a) = raise j (a₀ ≡ a) coprod-code {i} {j} a₀ (inr b) = raise _ Empty

coprod-encode : {i j : Level} {A : Type i} {B : Type j} (a₀ : A) → (x : A + B) (p : inl a₀ ≡ x) → coprod-code a₀ x coprod-encode a₀ x p = transport (coprod-code a₀) p (map-raise refl)

coprod-decode : {i j : Level} {A : Type i} {B : Type j} (a₀ : A) → (x : A + B) (c : coprod-code a₀ x) → (inl a₀ ≡ x) coprod-decode a₀ (inl x) c = ap inl (map-inv-raise c) coprod-decode a₀ (inr x) (map-raise ())

coprod-encode-decode-id : {i j : Level} {A : Type i} {B : Type j} (a₀ : A) → (x : A + B) → coprod-encode a₀ x o coprod-decode a₀ x ~ id coprod-encode-decode-id a₀ (inl a) = λ { (map-raise refl) → refl} coprod-encode-decode-id a₀ (inr b) = λ { (map-raise ())}

coprod-decode-encode-id : {i j : Level} {A : Type i} {B : Type j} (a₀ : A) → (x : A + B) → coprod-decode a₀ x o coprod-encode a₀ x ~ id coprod-decode-encode-id a₀ (inl a) = λ { refl → refl} coprod-decode-encode-id a₀ (inr b) = λ { ()}

thm2-12-5 : {i j : Level} {A : Type i} {B : Type j} (a₀ : A) → (x : A + B) → (inl a₀ ≡ x) ≃ coprod-code a₀ x thm2-12-5 a₀ x = equiv-adjointify (coprod-encode a₀ x , coprod-decode a₀ x , coprod-encode-decode-id a₀ x , coprod-decode-encode-id a₀ x)

Author: James Leslie

Created: 2021-03-27 Sat 10:47