4 lines
197 B
Plaintext
4 lines
197 B
Plaintext
|
let ap : Π (A : Type) Π (B : Type) Π (f : A → B)
|
||
|
|
Π (x : A) Π (y : A) Id A x y → Id B (f x) (f y)
|
||
|
|
≔ λA.λB.λf.λx.λy. J A x y (λa.λb.λ_. Id B (f a) (f b)) (refl B (f x))
|