14 lines
281 B
Agda
14 lines
281 B
Agda
|
{-# OPTIONS --cubical #-}
|
||
|
|
||
|
module HIT where
|
||
|
|
||
|
open import Cubical.Core.Everything
|
||
|
|
||
|
data S¹ : Set where
|
||
|
base : S¹
|
||
|
loop : base ≡ base
|
||
|
|
||
|
apd : {A : Set} {B : A → Set} (f : (x : A) → B x) {x y : A} (p : x ≡ y)
|
||
|
→ PathP (λ i → B (p i)) (f x) (f y)
|
||
|
apd f p i = f (p i)
|