# A proof of Yoneda <-> Dependent path induction formalised in UniMath

Write-up: pending

Formalisation: [y_and_j.v](y\_and\_j.v)