Non-Wellfounded Sets in Homotopy Type Theory

Introduction

Notation

• $W\; (a\; :\; A)\; B(a),\; sup\; :\; (a\; :\; A)\; \to \; (A\; \to \; W\; (a\; :\; A)\; B(a))\; \to \; W\; (a\; :\; A)\; B(a),$
• $M\; (a\; :\; A)\; B(a),\; desup\; :\; W\; (a\; :\; A)\; B(a)\; \to \; (a\; :\; A)\; \times \; (A\; \to \; W\; (a\; :\; A)\; B(a))\; \to \; W\; (a\; :\; A)\; B(a),$
• $A\; \hookrightarrow \; B\; \equiv \; (f\; :\; A\; \to \; B)\; \times \; is-prop\; f^[-1],\; (embeddings)$
• $A\; \twoheadrightarrow \; B\; \equiv \; (f\; :\; A\; \to \; B)\; \times \; (b\; :\; B)\; \to \; ||(a\; :\; A)\; \times \; f\; a\; =\; b||.\; (surjections)$

Images Of Small Types – An Additional Assumption

f : A → B: a subtype of B or a quotient of A?

U-Powersets

Definition 3

Lemma 2

Equality in powersets is fiberwise.

Lemma 3

The powerset is a set.

∈-Structures

U-Likeness

Lemma 7

∈-structures are coalgebras.

Fixed-Point Models

Definition 26

Membership.

– which is a proposition since f is an embedding. Note that since V is locally U-small, x ∈ y is essentially U-small.

Theorem 2 (Extensionality)

Theorem 3 (Restricted separation)

Theorem 4 (Union-replacement)

Theorem 5 (Paring)

Theorem 6 (Exponentiation)

Theorem 7 (Natural numbers)

Constructing the Terminal P_U-Coalgebra

Anti-Foundation in the Terminal P_U-Coalgebra

Example 3 (Conatural Numbers)

As an M-type:

As the terminal coalgebra for the polynomial: