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

Write-up: pending

Formalisation: [y_and_j.v](y_and_j/tree/master/y_and_j.v)