What is the behavior of I in the cubical definition of apd #16

New issue

Closed

opened 2024-05-23 16:38:00 +00:00 by michael · 1 comment

michael commented

2024-05-23 16:38:00 +00:00

Owner

Comparing the implementations of apd in:

non-cubical hott cubical hott

non-cubical hott	cubical hott
`apd : {l₁ l₂ : Level} {A : Set l₁} {P : A → Set l₂} {x y : A} → (f : (x : A) → P x) → (p : x ≡ y) → transport P p (f x) ≡ f y apd {l₁} {l₂} {A} {P} {x} {y} f p = J (λ x y p → transport P p (f x) ≡ f y) (λ x → refl) x y p`	`apd : ∀ {a b} {A : I → Type a} {B : (i : I) → A i → Type b} → (f : (i : I) → (a : A i) → B i a) → {x : A i0} → {y : A i1} → (p : PathP A x y) → PathP (λ i → B i (p i)) (f i0 x) (f i1 y) apd f p i = f i (p i)` Cribbed from 1lab

apd : {l₁ l₂ : Level} {A : Set l₁} {P : A → Set l₂} {x y : A}
  → (f : (x : A) → P x)
  → (p : x ≡ y)
  → transport P p (f x) ≡ f y
apd {l₁} {l₂} {A} {P} {x} {y} f p =
  J (λ x y p → transport P p (f x) ≡ f y) (λ x → refl) x y p

apd : ∀ {a b} {A : I → Type a} {B : (i : I) → A i → Type b}
  → (f : (i : I) → (a : A i) → B i a)
  → {x : A i0}
  → {y : A i1}
  → (p : PathP A x y)
  → PathP (λ i → B i (p i)) (f i0 x) (f i1 y)
apd f p i = f i (p i)

Cribbed from 1lab

Comparing the implementations of apd in: <table> <thead> <tr> <th>non-cubical hott</th> <th>cubical hott</th> </tr> </thead> <tbody> <tr> <td> ``` apd : {l₁ l₂ : Level} {A : Set l₁} {P : A → Set l₂} {x y : A} → (f : (x : A) → P x) → (p : x ≡ y) → transport P p (f x) ≡ f y apd {l₁} {l₂} {A} {P} {x} {y} f p = J (λ x y p → transport P p (f x) ≡ f y) (λ x → refl) x y p ``` </td> <td> ``` apd : ∀ {a b} {A : I → Type a} {B : (i : I) → A i → Type b} → (f : (i : I) → (a : A i) → B i a) → {x : A i0} → {y : A i1} → (p : PathP A x y) → PathP (λ i → B i (p i)) (f i0 x) (f i1 y) apd f p i = f i (p i) ``` Cribbed from [1lab](https://1lab.dev/1Lab.Path.html#46005) </td> </tbody> </table>