Poslední dobou tu je nějak natrolleno, tak snad vážně míněný dotaz nezapadne. Máte někdo nějaký názorný příklad identitních typů v homotopické teorii typů? V teorii typů chápu všechno až po závislostní typy (které teď pozvolna pronikají do Haskellu), ale u identit mě nenapadá žádná instance kromě triviálního (extenziálního) porovnání. Přitom homotopií by měla být hromada. Uvítám také typy na jazyky, ve kterých se dá s identitami pracovat, ovšem primárně mi jde o příklad bez ohledu na jazyk.