nLab circle type

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Contents

Idea

The circle type is an axiomatization of the homotopy type of the (shape of) the circle in the context of homotopy type theory.

Definition

There are two ways to define the circle type: one can define it in terms of explicit inference rules, or one can use the notion of higher inductive type. We will discuss both formulations.

With inference rules

Let a= Aba =_A b denote the identification type between elements a:Aa:A and b:Ab:A of type AA, and let y= x:A.B(x) (a,b,p)zy =_{x:A.B(x)}^{(a, b, p)} z denote the heterogeneous identification type between elements y:B(a)y:B(a) and z:B(b)z:B(b) of type family x:AB(x)x:A \vdash B(x), given elements a:Aa:A and b:Ab:A and identification p:a= Abp:a =_A b. Let apd f(a,b,p)\mathrm{apd}_f(a, b, p) denote the dependent function application of the dependent function f: x:AB(x)f:\prod_{x:A} B(x) to the identification p:a= Abp:a =_A b

In the natural deduction formulation of dependent type theory, the circle type is given by the following inference rules:

First the rule that defines the circle type itself in some context Γ\Gamma.

type formation

ΓctxΓS 1type\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash S^1 \; \mathrm{type}}

Now the basic “introduction” rule, which says that the circle type consists of a base point base:S 1\mathrm{base}:S^1 and a loop identification loop:base= S 1base\mathrm{loop}:\mathrm{base} =_{S^1} \mathrm{base}.

term introduction:

ΓctxΓbase:S 1ΓctxΓloop:base= S 1base\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{base}:S^1} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{loop}:\mathrm{base} =_{S^1} \mathrm{base}}

Induction principle

There are different induction principles associated with the circle type, depending on whether judgmental equalities or identifications are used; if the former are used, this results in strict circle types, and if the latter are used, this results in weak circle types.

The induction principle for strict circle types states that if:

  1. For all x:S 1x:S^1 we have a type C(x)C(x)

  2. For any term c base:C(base)c_\mathrm{base}:C(\mathrm{base}) and any heterogeneous identification c loop:c base= x:S 1.C(x) (base,base,loop)c basec_\mathrm{loop}:c_\mathrm{base} =_{x:S^1.C(x)}^{(\mathrm{base}, \mathrm{base}, \mathrm{loop})} c_\mathrm{base} that c basec_\mathrm{base} is equal to itself across loop\mathrm{loop}

then we have a dependent function c: x:S 1C(x)c:\prod_{x:S^1} C(x) such that evaluating cc at base\mathrm{base} results in c basec_\mathrm{base} and applying cc across loop\mathrm{loop} results in c loopc_\mathrm{loop}.

c(base)c baseapd c(base,base,loop)c loopc(\mathrm{base}) \equiv c_\mathrm{base} \qquad \mathrm{apd}_c(\mathrm{base}, \mathrm{base}, \mathrm{loop}) \equiv c_\mathrm{loop}

The induction principle for weak circle types states that if:

  1. For all x:S 1x:S^1 we have a type C(x)C(x)

  2. For any term c base:C(base)c_\mathrm{base}:C(\mathrm{base}) and any heterogeneous identification c loop:c base= x:S 1.C(x) (base,base,loop)c basec_\mathrm{loop}:c_\mathrm{base} =_{x:S^1.C(x)}^{(\mathrm{base}, \mathrm{base}, \mathrm{loop})} c_\mathrm{base} that c basec_\mathrm{base} is equal to itself across loop\mathrm{loop}

there exists a dependent function c: x:S 1C(x)c:\prod_{x:S^1} C(x) and an identification p:c(base)= C(base)c basep:c(\mathrm{base}) =_{C(\mathrm{base})} c_\mathrm{base} such that applying cc across loop\mathrm{loop} is equal to c loopc_\mathrm{loop} across pp.

ap c(base,base,loop)= z:C(base).z= x:S 1.C(x) (base,base,loop)z (c(base),c base,p)c loop\mathrm{ap}_c(\mathrm{base}, \mathrm{base}, \mathrm{loop}) =_{z:C(\mathrm{base}).z =_{x:S^1.C(x)}^{(\mathrm{base}, \mathrm{base}, \mathrm{loop})} z}^{(c(\mathrm{base}), c_\mathrm{base}, p)} c_\mathrm{loop}

These are both formalized via the elimination and computation rules for the circle type:

Elimination rules for the circle type:

Γ,x:S 1C(x)typeΓc base:C(base)Γc loop:c base= x:S 1.C(x) (base,base,loop)c baseΓind S 1(c base,c loop): x:S 1C(x)\frac{\Gamma, x:S^1 \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_\mathrm{base}:C(\mathrm{base}) \quad \Gamma \vdash c_\mathrm{loop}:c_\mathrm{base} =_{x:S^1.C(x)}^{(\mathrm{base}, \mathrm{base}, \mathrm{loop})} c_\mathrm{base}}{\Gamma \vdash \mathrm{ind}_{S^1}(c_\mathrm{base}, c_\mathrm{loop}):\prod_{x:S^1} C(x)}

Computation rules for the strict circle type

Γ,x:S 1C(x)typeΓc base:C(base)Γc loop:c base= x:S 1.C(x) (base,base,loop)c baseΓind S 1(c base,c loop)(base)c base:C(base)\frac{\Gamma, x:S^1 \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_\mathrm{base}:C(\mathrm{base}) \quad \Gamma \vdash c_\mathrm{loop}:c_\mathrm{base} =_{x:S^1.C(x)}^{(\mathrm{base}, \mathrm{base}, \mathrm{loop})} c_\mathrm{base}}{\Gamma \vdash \mathrm{ind}_{S^1}(c_\mathrm{base}, c_\mathrm{loop})(\mathrm{base}) \equiv c_\mathrm{base}:C(\mathrm{base})}
  • Judgmental path constructors
Γ,x:S 1C(x)typeΓc base:C(base)Γc loop:c base= x:S 1.C(x) (base,base,loop)c baseΓapd ind S 1(c base,c loop)(base,base,loop)c loop:c base= x:S 1.C(x) (base,base,loop)c base\frac{\Gamma, x:S^1 \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_\mathrm{base}:C(\mathrm{base}) \quad \Gamma \vdash c_\mathrm{loop}:c_\mathrm{base} =_{x:S^1.C(x)}^{(\mathrm{base}, \mathrm{base}, \mathrm{loop})} c_\mathrm{base}}{\Gamma \vdash \mathrm{apd}_{\mathrm{ind}_{S^1}(c_\mathrm{base}, c_\mathrm{loop})}(\mathrm{base}, \mathrm{base}, \mathrm{loop}) \equiv c_\mathrm{loop}:c_\mathrm{base} =_{x:S^1.C(x)}^{(\mathrm{base}, \mathrm{base}, \mathrm{loop})} c_\mathrm{base}}
  • Propositional path constructors
Γ,x:S 1C(x)typeΓc base:C(base)Γc loop:c base= x:S 1.C(x) (base,base,loop)c baseΓβ S 1 loop(c base,c loop):apd ind S 1(c base,c loop)(base,base,loop)= c base= x:S 1.C(x) (base,base,loop)c basec loop\frac{\Gamma, x:S^1 \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_\mathrm{base}:C(\mathrm{base}) \quad \Gamma \vdash c_\mathrm{loop}:c_\mathrm{base} =_{x:S^1.C(x)}^{(\mathrm{base}, \mathrm{base}, \mathrm{loop})} c_\mathrm{base}}{\Gamma \vdash \beta_{S^1}^{\mathrm{loop}}(c_\mathrm{base}, c_\mathrm{loop}):\mathrm{apd}_{\mathrm{ind}_{S^1}(c_\mathrm{base}, c_\mathrm{loop})}(\mathrm{base}, \mathrm{base}, \mathrm{loop}) =_{c_\mathrm{base} =_{x:S^1.C(x)}^{(\mathrm{base}, \mathrm{base}, \mathrm{loop})} c_\mathrm{base}} c_\mathrm{loop}}

Computation rules for the weak circle type

Γ,x:S 1C(x)typeΓc base:C(base)Γc loop:c base= x:S 1.C(x) (base,base,loop)c baseΓβ S 1 base(c base,c loop):ind S 1(c base,c loop)(base)= C(base)c base\frac{\Gamma, x:S^1 \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_\mathrm{base}:C(\mathrm{base}) \quad \Gamma \vdash c_\mathrm{loop}:c_\mathrm{base} =_{x:S^1.C(x)}^{(\mathrm{base}, \mathrm{base}, \mathrm{loop})} c_\mathrm{base}}{\Gamma \vdash \beta_{S^1}^{\mathrm{base}}(c_\mathrm{base}, c_\mathrm{loop}):\mathrm{ind}_{S^1}(c_\mathrm{base}, c_\mathrm{loop})(\mathrm{base}) =_{C(\mathrm{base})} c_\mathrm{base}}
Γ,x:S 1C(x)typeΓc base:C(base)Γc loop:c base= x:S 1.C(x) (base,base,loop)c baseΓβ S 1 loop(c base,c loop):apd ind S 1(c base,c loop)(base,base,loop)= z:C(base).z= x:S 1.C(x) (base,base,loop)z (ind S 1(c base,c loop)(base),c base,β S 1 base(c base,c loop))c loop\frac{\Gamma, x:S^1 \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_\mathrm{base}:C(\mathrm{base}) \quad \Gamma \vdash c_\mathrm{loop}:c_\mathrm{base} =_{x:S^1.C(x)}^{(\mathrm{base}, \mathrm{base}, \mathrm{loop})} c_\mathrm{base}}{\Gamma \vdash \beta_{S^1}^{\mathrm{loop}}(c_\mathrm{base}, c_\mathrm{loop}):\mathrm{apd}_{\mathrm{ind}_{S^1}(c_\mathrm{base}, c_\mathrm{loop})}(\mathrm{base}, \mathrm{base}, \mathrm{loop}) =_{z:C(\mathrm{base}).z =_{x:S^1.C(x)}^{(\mathrm{base}, \mathrm{base}, \mathrm{loop})} z}^{(\mathrm{ind}_{S^1}(c_\mathrm{base}, c_\mathrm{loop})(\mathrm{base}), c_\mathrm{base}, \beta_{S^1}^{\mathrm{base}}(c_\mathrm{base}, c_\mathrm{loop}))} c_\mathrm{loop}}

For weak circle types, we can package the elimination and propositional computation rules together using dependent sum types to get a single rule for the induction principle of the circle type:

Γ,x:S 1C(x)typeΓc base:C(base)Γc loop:c base= x:S 1.C(x) (base,base,loop)c baseΓind S 1 x:S 1.C(x)(c base,c loop): c: x:S 1C(x) p:c(base)= C(base)c baseapd c(base,base,loop)= z:C(base).z= x:S 1.C(x) (base,base,loop)z (c(base),c base,p)c loop\frac{\Gamma, x:S^1 \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_\mathrm{base}:C(\mathrm{base}) \quad \Gamma \vdash c_\mathrm{loop}:c_\mathrm{base} =_{x:S^1.C(x)}^{(\mathrm{base}, \mathrm{base}, \mathrm{loop})} c_\mathrm{base}}{\Gamma \vdash \mathrm{ind}_{S^1}^{x:S^1.C(x)}(c_\mathrm{base}, c_\mathrm{loop}):\sum_{c:\prod_{x:S^1} C(x)} \sum_{p:c(\mathrm{base}) =_{C(\mathrm{base})} c_\mathrm{base}} \mathrm{apd}_c(\mathrm{base}, \mathrm{base}, \mathrm{loop}) =_{z:C(\mathrm{base}).z =_{x:S^1.C(x)}^{(\mathrm{base}, \mathrm{base}, \mathrm{loop})} z}^{(c(\mathrm{base}), c_\mathrm{base}, p)} c_\mathrm{loop}}

Since the circle type is a positive type, it is not necessary to include a uniqueness rule for the induction principle circle types, since the propositional uniqueness rule can be proven from the the other inference rules for the circle type. Nevertheless, one can include the uniqueness rule in the combined single induction rule by turning the dependent sum type into a uniqueness quantifier, resulting in the dependent universal property of the circle type.

Γ,x:S 1C(x)typeΓc base:C(base)Γc loop:c base= x:S 1.C(x) (base,base,loop)c baseΓind S 1 x:S 1.C(x)(c base,c loop):!c: x:S 1C(x). p:c(base)= C(base)c baseapd c(base,base,loop)= z:C(base).z= x:S 1.C(x) (base,base,loop)z (c(base),c base,p)c loop\frac{\Gamma, x:S^1 \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_\mathrm{base}:C(\mathrm{base}) \quad \Gamma \vdash c_\mathrm{loop}:c_\mathrm{base} =_{x:S^1.C(x)}^{(\mathrm{base}, \mathrm{base}, \mathrm{loop})} c_\mathrm{base}}{\Gamma \vdash \mathrm{ind}_{S^1}^{x:S^1.C(x)}(c_\mathrm{base}, c_\mathrm{loop}):\exists!c:\prod_{x:S^1} C(x).\sum_{p:c(\mathrm{base}) =_{C(\mathrm{base})} c_\mathrm{base}} \mathrm{apd}_c(\mathrm{base}, \mathrm{base}, \mathrm{loop}) =_{z:C(\mathrm{base}).z =_{x:S^1.C(x)}^{(\mathrm{base}, \mathrm{base}, \mathrm{loop})} z}^{(c(\mathrm{base}), c_\mathrm{base}, p)} c_\mathrm{loop}}

Recursion principle

In general, given a type CC, by the weakening rule of dependent type theory, one can form the constant type family CC indexed by x:S 1x:S^1; then one can get the recursion principle of the circle type from the induction principle on CC regarded as a constant type family:

The recursion principle for strict circle types states that if:

  1. We have a type CC

  2. For any term c base:Cc_\mathrm{base}:C and any identification c loop:c base= Cc basec_\mathrm{loop}:c_\mathrm{base} =_{C} c_\mathrm{base} that c basec_\mathrm{base} is equal to itself

then we have a function c:S 1Cc:S^1 \to C such that evaluating cc at base\mathrm{base} results in c basec_\mathrm{base} and applying cc across loop\mathrm{loop} results in c loopc_\mathrm{loop}.

c(base)c baseap c(base,base,loop)c loopc(\mathrm{base}) \equiv c_\mathrm{base} \qquad \mathrm{ap}_c(\mathrm{base}, \mathrm{base}, \mathrm{loop}) \equiv c_\mathrm{loop}

The recursion principle for weak circle types states that if:

  1. We have a type CC

  2. For any term c base:Cc_\mathrm{base}:C and any identification c loop:c base= Cc basec_\mathrm{loop}:c_\mathrm{base} =_{C} c_\mathrm{base} that c basec_\mathrm{base} is equal to itself

there exists a function c:S 1Cc:S^1 \to C and an identification p:c(base)= C(base)c basep:c(\mathrm{base}) =_{C(\mathrm{base})} c_\mathrm{base} such that applying cc across loop\mathrm{loop} is equal to c loopc_\mathrm{loop} across pp.

ap c(base,base,loop)= z:C.z= Cz (c(base),c base,p)c loop\mathrm{ap}_c(\mathrm{base}, \mathrm{base}, \mathrm{loop}) =_{z:C.z =_{C} z}^{(c(\mathrm{base}), c_\mathrm{base}, p)} c_\mathrm{loop}

The recursion principle for weak circle types can be presented as a single rule via the use of a dependent sum type:

ΓCtypeΓc base:CΓc loop:c base= Cc baseΓrec S 1 C(c base,c loop): c:S 1C p:c(base)= C(base)c baseap c(base,base,loop)= z:C.z= Cz (c(base),c base,p)c loop\frac{\Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash c_\mathrm{base}:C \quad \Gamma \vdash c_\mathrm{loop}:c_\mathrm{base} =_{C} c_\mathrm{base}}{\Gamma \vdash \mathrm{rec}_{S^1}^{C}(c_\mathrm{base}, c_\mathrm{loop}):\sum_{c:S^1 \to C} \sum_{p:c(\mathrm{base}) =_{C(\mathrm{base})} c_\mathrm{base}} \mathrm{ap}_c(\mathrm{base}, \mathrm{base}, \mathrm{loop}) =_{z:C.z =_{C} z}^{(c(\mathrm{base}), c_\mathrm{base}, p)} c_\mathrm{loop}}

and similarly, the (non-dependent) universal property of the circle type is presented as a single rule by replacing the dependent sum type in the recursion principle with a uniqueness quantifier

ΓCtypeΓc base:CΓc loop:c base= Cc baseΓrec S 1 C(c base,c loop):!c:S 1C. p:c(base)= C(base)c baseap c(base,base,loop)= z:C.z= Cz (c(base),c base,p)c loop\frac{\Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash c_\mathrm{base}:C \quad \Gamma \vdash c_\mathrm{loop}:c_\mathrm{base} =_{C} c_\mathrm{base}}{\Gamma \vdash \mathrm{rec}_{S^1}^{C}(c_\mathrm{base}, c_\mathrm{loop}):\exists!c:S^1 \to C.\sum_{p:c(\mathrm{base}) =_{C(\mathrm{base})} c_\mathrm{base}} \mathrm{ap}_c(\mathrm{base}, \mathrm{base}, \mathrm{loop}) =_{z:C.z =_{C} z}^{(c(\mathrm{base}), c_\mathrm{base}, p)} c_\mathrm{loop}}

 In terms of higher inductive types

As a higher inductive type, the circle is given by

Inductive Circle : Type
  | base : Circle
  | loop : Id Circle base base

This says that the type is inductively constructed from

  1. a term of circle type whose interpretation is as the base point of the circle,

  2. a term of the identification type between these two terms, whose interpretation is as the 1-cell of the circle

    baseloopbase base \stackrel{loop}{\to} base \,

    Hence as a non-constant path from the base point to itself.

Properties

 Relation to axiom K

Theorem

Suppose that the strict circle type has an identification K:refl S 1(base)=loopK:\mathrm{refl}_{S^1}(\mathrm{base}) = \mathrm{loop}. Then every type is a set.

Proof

For all types AA, terms x:Ax:A, and self-identifications p:x= Axp:x =_A x, by the recursion principle of the strict circle type, we have the function rec S 1(x,p):S 1A\mathrm{rec}_{S^1}(x, p):S^1 \to A such that rec S 1(x,p)(base)x\mathrm{rec}_{S^1}(x, p)(\mathrm{base}) \equiv x and ap rec S 1 A(x,p)(base,base,loop)p\mathrm{ap}_{\mathrm{rec}_{S^1}^A(x, p)}(\mathrm{base}, \mathrm{base}, \mathrm{loop}) \equiv p. We also have by definition of ap rec S 1(x,p)\mathrm{ap}_{\mathrm{rec}_{S^1}(x, p)} that

ap rec S 1(x,p)(base,base,refl S 1(base))refl A(rec S 1(x,p)(base))refl A(x)\mathrm{ap}_{\mathrm{rec}_{S^1}(x, p)}(\mathrm{base}, \mathrm{base}, \mathrm{refl}_{S^1}(\mathrm{base})) \equiv \mathrm{refl}_{A}(\mathrm{rec}_{S^1}(x, p)(\mathrm{base})) \equiv \mathrm{refl}_A(x)

By applying ap rec S 1(x,p)(base,base)\mathrm{ap}_{\mathrm{rec}_{S^1}(x, p)}(\mathrm{base}, \mathrm{base}) to KK, we have identification

ap ap rec S 1(x,p)(base,base)(refl S 1(base),loop,K):ap rec S 1(x,p)(base,base,refl S 1(base))=ap rec S 1(x,p)(base,base,loop)\mathrm{ap}_{\mathrm{ap}_{\mathrm{rec}_{S^1}(x, p)}(\mathrm{base}, \mathrm{base})}(\mathrm{refl}_{S^1}(\mathrm{base}), \mathrm{loop}, K):\mathrm{ap}_{\mathrm{rec}_{S^1}(x, p)}(\mathrm{base}, \mathrm{base}, \mathrm{refl}_{S^1}(\mathrm{base})) = \mathrm{ap}_{\mathrm{rec}_{S^1}(x, p)}(\mathrm{base}, \mathrm{base}, \mathrm{loop})

which reduces down to

ap ap rec S 1(x,p)(base,base)(refl S 1(base),loop,K):refl A(x)=p\mathrm{ap}_{\mathrm{ap}_{\mathrm{rec}_{S^1}(x, p)}(\mathrm{base}, \mathrm{base})}(\mathrm{refl}_{S^1}(\mathrm{base}), \mathrm{loop}, K):\mathrm{refl}_{A}(x) = p

which is precisely axiom K for type AA. Thus every type AA is a set.

Theorem

Suppose that the loop of the circle is judgmentally equal to reflexivity of the base of the circle refl S 1(base)loop:base= S 1base\mathrm{refl}_{S^1}(\mathrm{base}) \equiv \mathrm{loop}:\mathrm{base} =_{S^1} \mathrm{base}. Then the judgmental K rule holds.

Proof

For all types AA, terms x:Ax:A, and self-identifications p:x= Axp:x =_A x, by the recursion principle of the strict circle type, we have the function rec S 1(x,p):S 1A\mathrm{rec}_{S^1}(x, p):S^1 \to A such that rec S 1(x,p)(base)x\mathrm{rec}_{S^1}(x, p)(\mathrm{base}) \equiv x and ap rec S 1 A(x,p)(base,base,loop)p\mathrm{ap}_{\mathrm{rec}_{S^1}^A(x, p)}(\mathrm{base}, \mathrm{base}, \mathrm{loop}) \equiv p. We also have by definition of ap rec S 1(x,p)\mathrm{ap}_{\mathrm{rec}_{S^1}(x, p)} that

ap rec S 1(x,p)(base,base,refl S 1(base))refl A(rec S 1(x,p)(base))refl A(x)\mathrm{ap}_{\mathrm{rec}_{S^1}(x, p)}(\mathrm{base}, \mathrm{base}, \mathrm{refl}_{S^1}(\mathrm{base})) \equiv \mathrm{refl}_{A}(\mathrm{rec}_{S^1}(x, p)(\mathrm{base})) \equiv \mathrm{refl}_A(x)

Since functions preserve judgmental equality, by applying the function ap rec S 1(x,p)(base,base)\mathrm{ap}_{\mathrm{rec}_{S^1}(x, p)}(\mathrm{base}, \mathrm{base}) to the judgmental equality refl S 1(base)loop:base= S 1base\mathrm{refl}_{S^1}(\mathrm{base}) \equiv \mathrm{loop}:\mathrm{base} =_{S^1} \mathrm{base}, we have a judgmental equality

ap rec S 1(x,p)(base,base,loop)ap rec S 1(x,p)(base,base,refl S 1(base)):x= Ax\mathrm{ap}_{\mathrm{rec}_{S^1}(x, p)}(\mathrm{base}, \mathrm{base}, \mathrm{loop}) \equiv \mathrm{ap}_{\mathrm{rec}_{S^1}(x, p)}(\mathrm{base}, \mathrm{base}, \mathrm{refl}_{S^1}(\mathrm{base})):x =_A x

which reduces down to

prefl A(x):x= Axp \equiv \mathrm{refl}_A(x):x =_A x

which is precisely the judgmental K rule for type AA.

Types equivalent to the circle type

The circle type is equivalent to the following types

11S 1\mathbf{1} \rightrightarrows \mathbf{1} \to S^1
A 1sid A 1A 1S 1 A^1\underoverset{\quad s \quad}{\mathrm{id}_{A^1}}{\rightrightarrows}A^1 \to S^1
  • Given a univalent universe UU, the type of UU-small \mathbb{Z}-torsors. One can then prove that this type satisfies the same induction principle (propositionally). This is due to Dan Grayson.

Induction principle without heterogeneous identifications

There is a version of the induction principle which uses a type CC and a function f:CS 1f:C \to S^1 instead of a type family P(x)P(x) indexed by x:S 1x:S^1. It has the benefit of not requiring that one has first defined heterogeneous identification types, whether as an inductive family of types or by using transport.

The induction principle of the circle type says that given a type CC and a function f:CS 1f:C \to S^1, as well as

  • an element c base:Cc_\mathrm{base}:C

  • identifications c loop:c base= Cc basec_\mathrm{loop}:c_\mathrm{base} =_C c_\mathrm{base} and p base:f(c base)= S 1basep_\mathrm{base}:f(c_\mathrm{base}) =_{S^1} \mathrm{base} such that ap f(c loop)\mathrm{ap}_f(c_\mathrm{loop}), p basep_\mathrm{base}, p basep_\mathrm{base}, and loop\mathrm{loop} form a square

f(c base) =ap f(c loop) f(c base) p base p base base =loop base \begin{array}{c} & f(c_\mathrm{base}) & \overset{\mathrm{ap}_{f}(c_\mathrm{loop})}= & f(c_\mathrm{base}) & \\ p_\mathrm{base} & \Vert & & \Vert & p_\mathrm{base}\\ & \mathrm{base} & \underset{\mathrm{loop}}= & \mathrm{base} & \\ \end{array}
  • an identification saying that the square commutes
p loop:ap f(c loop)p base= f(c base)= S 1loopp baseloopp_\mathrm{loop}:\mathrm{ap}_f(c_\mathrm{loop}) \bullet p_\mathrm{base} =_{f(c_\mathrm{base}) =_{S^1} \mathrm{loop}} p_\mathrm{base} \bullet \mathrm{loop}

one can construct

  • a function
g:S 1Cg:S^1 \to C
  • a homotopy witnessing that gg is a section of ff:
sec g: x:S 1f(g(x))= S 1x\mathrm{sec}_g:\prod_{x:S^1} f(g(x)) =_{S^1} x

such that

g(base)c basesec g(base)p baseap g(loop)c loopg(\mathrm{base}) \equiv c_\mathrm{base} \quad \mathrm{sec}_g(\mathrm{base}) \equiv p_\mathrm{base} \quad \mathrm{ap}_{g}(\mathrm{loop}) \equiv c_\mathrm{loop}
ind =(λx:S 1.refl f(g(x))= S 1x(sec g(x)),base,base,loop)p loop\mathrm{ind}_{=}\left(\lambda x:S^1.\mathrm{refl}_{f(g(x)) =_{S^1} x}(\mathrm{sec}_g(x)), \mathrm{base}, \mathrm{base}, \mathrm{loop}\right) \equiv p_\mathrm{loop}

The last condition needs some explanation. Since gg is a section of ff, the composite fgf \circ g is the identity function on the circle type, up to identification. Now, given any identity function on the circle type i:S 1S 1i:S^1 \to S^1 with homotopy

j: x:S 1i(x)= S 1xj:\prod_{x:S^1} i(x) =_{S^1} x

we have the following square for all x:S 1x:S^1, y:S 1y:S^1, and q:x= S 1yq:x =_{S^1} y:

i(x) =ap i(q) i(y) j(x) j(y) x =q y \begin{array}{c} & i(x) & \overset{\mathrm{ap}_{i}(q)}= & i(y) & \\ j(x) & \Vert & & \Vert & j(y)\\ & x & \underset{q}= & y & \\ \end{array}

This square commutes via the J rule: it suffices to construct an element of

ap i(refl S 1(x))j(x)= i(x)= S 1xj(x)refl S 1(x)\mathrm{ap}_{i}(\mathrm{refl}_{S^1}(x)) \bullet j(x) =_{i(x) =_{S^1} x} j(x) \bullet \mathrm{refl}_{S^1}(x)

But ap i(refl S 1(x))j(x)\mathrm{ap}_{i}(\mathrm{refl}_{S^1}(x)) \bullet j(x) reduces down to j(x)j(x) via

ap i(refl S 1(x))j(x)refl S 1(i(x))j(x)j(x)\mathrm{ap}_{i}(\mathrm{refl}_{S^1}(x)) \bullet j(x) \equiv \mathrm{refl}_{S^1}(i(x)) \bullet j(x) \equiv j(x)

and similarly j(x)refl S 1(x)j(x) \bullet \mathrm{refl}_{S^1}(x) reduces down to j(x)j(x), so just take reflexivity of j(x)j(x).

So the naturality square is inductively defined by

ind =(λx:S 1.refl i(x)= S 1x(j(x)),x,y,q):ap i(q)j(y)= i(x)= S 1yj(x)q\mathrm{ind}_{=}\left(\lambda x:S^1.\mathrm{refl}_{i(x) =_{S^1} x}(j(x)), x, y, q\right):\mathrm{ap}_{i}(q) \bullet j(y) =_{i(x) =_{S^1} y} j(x) \bullet q

When ifgi \coloneqq f \circ g, jsec gj \coloneqq \mathrm{sec}_g, xbasex \coloneqq \mathrm{base}, ybasey \coloneqq \mathrm{base}, and qloopq \coloneqq \mathrm{loop}, this results in the identification

ind =(λx:S 1.refl f(g(x))= S 1x(sec g(x)),base,base,loop)\mathrm{ind}_{=}\left(\lambda x:S^1.\mathrm{refl}_{f(g(x)) =_{S^1} x}(\mathrm{sec}_g(x)), \mathrm{base}, \mathrm{base}, \mathrm{loop}\right)

which is of the same type as p loopp_\mathrm{loop} due to the judgmental equalities in the other computation rules.

One gets back the usual induction principle of the interval type when C x:S 1P(x)C \equiv \sum_{x:S^1} P(x) and fπ 1f \equiv \pi_1 the first projection function of the dependent sum type, and one gets back the recursion principle of the interval type when CS 1×PC \equiv S^1 \times P and fπ 1f \equiv \pi_1 the first projection function of the product type.

Extensionality principle of the circle type

The extensionality principle of the circle type says that there is an equivalence of types between the identification type base= S 1base\mathrm{base} =_{S^1} \mathrm{base} and the type of integers \mathbb{Z}:

ext S 1:(base= S 1base)\mathrm{ext}_{S^1}:(\mathrm{base} =_{S^1} \mathrm{base}) \simeq \mathbb{Z}

Equivalently, that the loop space type Ω(S 1,base)\Omega(S^1, \mathrm{base}) is equivalent to the integers.

Thus, the extensionality principle of the circle type implies that the integers and thus the natural numbers are contractible types if axiom K or uniqueness of identity proofs hold for the entire type theory. If the extensionality principle of the natural numbers also hold in the type theory, then every type is contractible.

One can prove the extensionality principle of the circle type, given a univalent universe where the circle is small relative to the universe. The HoTT book provides a number of such proofs.

If one doesn’t have a type of integers or a type universe, then the extensionality principle of the circle type says that the identity types base= S 1base\mathrm{base} =_{S^1} \mathrm{base} satisfy the dependent universal property of the integers type with respect to the element refl S 1(base):base= S 1base\mathrm{refl}_{S^1}(\mathrm{base}):\mathrm{base} =_{S^1} \mathrm{base} and the equivalence

λp:base= S 1base.ploop:(base= S 1base)(base= S 1base)\lambda p:\mathrm{base} =_{S^1} \mathrm{base}.p \bullet \mathrm{loop}:(\mathrm{base} =_{S^1} \mathrm{base}) \simeq (\mathrm{base} =_{S^1} \mathrm{base})

This is a special case of the extensionality principle of coequalizer types and pushout types as detailed in Kraus and Raumer (2019).

The circle type and infinity

The extensionality principle of the circle type says that the loop space of the circle at its base point Ω(S 1,base)\Omega(S^1, \mathrm{base}) is a denumerable set. However, there is a weaker axiom that one can add to the circle type: that Ω(S 1,base)\Omega(S^1, \mathrm{base}) is an infinite type.

By the recursion principle of the natural numbers, there is a function

rec (refl S 1(base),λl:Ω(S 1,base).lloop):Ω(S 1,base)\mathrm{rec}_{\mathbb{N}}(\mathrm{refl}_{S^1}(\mathrm{base}), \lambda l:\Omega(S^1, \mathrm{base}).l \bullet \mathrm{loop}):\mathbb{N} \to \Omega(S^1, \mathrm{base})

which takes zero to reflexivity of base\mathrm{base} and the successor function to concatenation of a self-identification by loop\mathrm{loop}. That Ω(S 1,base)\Omega(S^1, \mathrm{base}) is an infinite set, states that the above function is an embedding of types,

inf S 1:isEmbed(rec (refl S 1(base),λl:Ω(S 1,base).lloop))\mathrm{inf}_{S^1}:\mathrm{isEmbed}\left(\mathrm{rec}_{\mathbb{N}}(\mathrm{refl}_{S^1}(\mathrm{base}), \lambda l:\Omega(S^1, \mathrm{base}).l \bullet \mathrm{loop})\right)

or equivalently that application of the above function is an equivalence for all natural numbers m:m:\mathbb{N}, n:n:\mathbb{N}

inf S 1: m: n:isEquiv(ap rec (refl S 1(base),λl:Ω(S 1,base).lloop)(m,n))\mathrm{inf}_{S^1}:\prod_{m:\mathbb{N}} \prod_{n:\mathbb{N}} \mathrm{isEquiv}\left(\mathrm{ap}_{\mathrm{rec}_{\mathbb{N}}(\mathrm{refl}_{S^1}(\mathrm{base}), \lambda l:\Omega(S^1, \mathrm{base}).l \bullet \mathrm{loop})}(m, n)\right)

If one doesn’t have a natural numbers type, the loop space Ω(S 1,base)\Omega(S^1, \mathrm{base}) of the circle type at its base point base:S 1\mathrm{base}:S^1 is an infinite set if and only if Ω(S 1,base)\Omega(S^1, \mathrm{base}) is equivalent to the sum type Ω(S 1,base)+Ω(S 1,base)\Omega(S^1, \mathrm{base}) + \Omega(S^1, \mathrm{base}).

inf S 1:Ω(S 1,base)(Ω(S 1,base)+Ω(S 1,base))\mathrm{inf}_{S^1}:\Omega(S^1, \mathrm{base}) \simeq (\Omega(S^1, \mathrm{base}) + \Omega(S^1, \mathrm{base}))

See Rasekh 21 for proving this statement in the presence of the univalence axiom.

Kuratowski-finiteness

The circle type is Kuratowski-finite. (Cf Frumin et al. 18)

H-space structures on the circle type

The type of H-spaces on the circle type is a contractible type.

References

The formalization of the shape homotopy type ʃS 1Bʃ S^1 \simeq \mathbf{B}\mathbb{Z} of the circle as a higher inductive type in homotopy type theory, along with a proof that ΩʃS 1\Omega ʃS^1\simeq {\mathbb{Z}} (and hence π 1(ʃS 1)\pi_1(ʃS^1) \simeq \mathbb{Z}):

Formalization in proof assistants:

in Coq:

in Agda:

Exposition and review:

Alternative construction of the circle type as the type of \mathbb{Z}-torsors:

Alternative construction of the circle type as a coequalizer:

For the fact that the type of H-space structures on a circle type is contractible:

For the fact that the circle type is Kuratowski-finite:

For the fact that one can construct a natural numbers type from the circle type:

For the induction principle of the identity types of the circle type:

Last revised on June 21, 2024 at 13:35:50. See the history of this page for a list of all contributions to it.