View Project

Norwegian AI Directory

Computational Aspects of Univalence


Description:

Et av resultatene i CAUs siste år er om symmetrier av sfærer i homotopi type teori med univalens (HoTT). Dette er kjente resultater i homotopi teori, og formålet med CAU er å finne ut hvordan å bevise slike resultater i HoTT slik at de kan bli verifisert av en datamaskin. Sfæren av dimension 1 er en sirkel. Sfæren av dimension 2 er grensen (overflaten) til en ball i 3D (sirkelen er faktisk grensen (randen) til en disk i 2D). Denne ideen kan generaliseres til å definere en sfære av dimension n, som vi angir med Sn. Det er en annen måte, mer tilpasset HoTT, å definere sfæren av dimension n>1. For S2 kan man forestille seg to poler, Nord og Sør, og en meridian, la oss si den til Greenwich. Nå dreier man meridianen ved å bevege punktet hvor den snitter ekvatoren langs ekvatoren. Ekvatoren er en sirkellinje, altså denne metoden beskriver hvordan man konstruerer S2 ved hjelp av S1. På samme måte kan man konstruere S3 ved hjelp av S2 (ikke like lett å forestille seg!), og så videre. Symmetrier er transformasjoner som kan reverseres og som bevarer objektets geometriske form. For eksempel, enhver rotasjon er en symmetri av sirkelen. Refleksjon er en annen symmetri av sirkelen. Symmetrier kan bli sammensatt til å gi andre symmetrier. Når det gjelder rotasjoner, så er det klart at man ikke trenger å dreie mer enn en full omdreining. Også, enhver rotasjon av sirkelen mot uret er lik en med uret. I HoTT med univalens har symmetrier av sfæren Sn typen Sn=Sn. Vi har bevist i HoTT at S1=S1 er ekvivalent med S1+S1. Venstre S1 i S1+S1 står for alle mulige rotasjoner, og høyre S1 står for alle mulige rotasjoner følgt av en refleksjon. Derimot er Sn=Sn ikke ekvivalent med Sn+Sn for n>1, symmetriene av S2, S3, ... er atskillig mer komplekse. Likevel har vi bevist i HoTT at Sn=Sn alltid kan underfordeles i to ekvivalente komponenter, en med og en uten reflekjson.


Project leader: Marc Bezem

Started: 2015

Ends: 2020

Category: Universiteter

Sector: UoH-sektor

Budget: 8615000

Institution: UNIVERSITETET I BERGEN

Address: NA