~tslil/y_and_j

A formalisation of the logical equivalence of the Yoneda lemma and dependent path induciton
2c93da3b — tslil clingman 11 months ago 
Markdown formatting
29cfc1b3 — tslil clingman 11 months ago 
Fixed link
e7eb1863 — tslil clingman 11 months ago 
Init

refs

master
browse  log 

clone

read-only
https://git.sr.ht/~tslil/y_and_j
read/write
git@git.sr.ht:~tslil/y_and_j

You can also use your local clone with git send-email.

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

Write-up: pending

Formalisation: yandj.v