Identity v homotopické teorii typů

Russell

Identity v homotopické teorii typů
« kdy: 06. 03. 2018, 10:20:33 »
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.


Jester

Re:Identity v homotopické teorii typů
« Odpověď #1 kdy: 06. 03. 2018, 13:48:18 »
názorný příklad identitních typů v homotopické teorii typů?
Jak na to tak koukám, tak s "normální" (tj. matematickou) homotopií to moc společného nemá, až na hierarchii.

Labrat

Re:Identity v homotopické teorii typů
« Odpověď #2 kdy: 07. 03. 2018, 15:31:37 »
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.
Id typy se v programování nepoužívají, protože mají v příčetných typových systémech nanejvýš jeden prvek, čímž tak nějak ztrácejí na atraktivitě. Netriviální příklad systému, kde mají víc členů, jsou grupoidy a isomorfismy mezi nimi. To ovšem není ani v Haskellu.