Discussion of Homotopy Type Theory and Univalent Foundations
 help / Atom feed
* [HoTT] Construction of the circle in UniMath
@ 2019-02-25 15:03 Ulrik Buchholtz
  0 siblings, 0 replies; 1+ messages in thread
From: Ulrik Buchholtz @ 2019-02-25 15:03 UTC (permalink / raw)
  To: Homotopy Type Theory

[-- Attachment #1.1: Type: text/plain, Size: 1859 bytes --]

Some time ago (May 2014), there was a discussion on this list about 
defining the circle as the type of Z-torsors. Dan had formalized in UniMath 
that this type satisfies the recursion principle for the circle, and Mike 
posted a quick sketch showing how to extend the proof to give the induction 
principle:

    
https://groups.google.com/d/msg/homotopytypetheory/hE1eY-v_Kes/bdSoAxC9224J

We're now pleased to announce that this indeed works, with a detailed proof 
developed independently of Mike's sketch by Marc and Ulrik, and formalized 
in UniMath by Dan:

    
https://github.com/DanGrayson/UniMath/blob/circle/UniMath/SyntheticHomotopyTheory/Circle2.v

    Definition circle := B ℤ.
    Definition pt := basepoint circle.
    Theorem loops_circle : ℤ ≃ Ω circle.
    Definition loop := loops_circle 1 : Ω circle.
    Definition CircleInduction (circle : Type) (pt : circle) (loop : pt = 
pt) :=
      ∏ (X:circle->Type) (x:X pt) (p:PathOver x x loop),
        ∑ (f:∏ t:circle, X t) (r : f pt = x), apd f loop = r ⟤ p ⟥ !r.
    Theorem circle_induction : CircleInduction circle pt loop.

If the underlying type theory has propositional truncation with an 
eliminator that computes judgmentally on the point constructor, then the 
same is true for our circle, i.e., the 'r' above is a reflexivity path.

We're working on a detailed write-up of the proof; you'll find a 
preliminary version of this if you follow a link in the above formalization.

Marc Bezem, Ulrik Buchholtz, and Dan Grayson

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.2: Type: text/html, Size: 2312 bytes --]

^ permalink raw reply	[flat|nested] 1+ messages in thread

only message in thread, back to index

Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2019-02-25 15:03 [HoTT] Construction of the circle in UniMath Ulrik Buchholtz

Discussion of Homotopy Type Theory and Univalent Foundations

Archives are clonable: git clone --mirror http://inbox.vuxu.org/hott

Newsgroup available over NNTP:
	nntp://inbox.vuxu.org/vuxu.archive.hott


AGPL code for this site: git clone https://public-inbox.org/ public-inbox