Primerjava teorije množic in teorije tipov kot temeljev matematikeJazbec, Matej (Avtor) Simpson, Alex (Mentor) teorija množicteorija tipovtipizomorfizemidentični tipizjaveaksiom univalentnostigrupemnožicekonstruktivna logikarelevantnost dokazovprincip strukturne identiteteBesedilo obravnava razlike v zasnovi teorije množic in teorije tipov kot temeljev matematike. Za vodilo nam služi primer bolj ali manj upravičenega enačenja izomorfnih matematičnih struktur, specifično grup. Osvežimo potrebno znanje teorije množic in se dlje časa posvečamo predstavitvi Martin-Löfove teorije tipov: spoznamo elementarne koncepte, kot so tipi in pravila, po katerih se vedejo, konstruktivno logiko, ki jo implicira interpretacija tipov kot izjav, ter podrobno razdelamo identične tipe, s katerimi implementiramo pojem izjavne enakosti (ki se razlikuje od trivialne sodbene). Konstruiramo tip, katerega elementi so grupe. Predstavimo tehnično konstrukcijo univalentnega tipa in vpeljemo aksiom univalentnosti, ki nam omogoča, da izomorfne matematične strukture formalno smatramo za enake. Kjer so prisotne, navajamo razlike med obravnavanima temeljnima teorijama. Navedemo klasifikacijo tipov glede na kompleksnost njihovih identičnih tipov ter izpostavimo obnašanje dveh skupin tipov analogno množicam oz. izjavam.20222022-07-22 08:15:02Delo diplomskega seminarja/zaključno seminarsko delo/naloga138470sl