Search results

Inconsistent notation for the type of pointed types

Status: Open.

#1197 In HoTT/book;

· Yosuke-Ito-345 opened on Jul 11, 2026

Nightly build can't find package gh

Status: Open.

#1195 In HoTT/book;

· mikeshulman opened on May 13, 2026

Clarification about judgmental unequality

Status: Open.

#1194 In HoTT/book;

· Yosuke-Ito-345 opened on Feb 14, 2026

Explanation of “fundamental group” is confusing

Status: Open.

#1190 In HoTT/book;

· Bolpat opened on Aug 27, 2025

Simplifications for Theorem 11.2.12 {RD-cauchy-complete}

Status: Open.

#1167 In HoTT/book;

· lowasser opened on Mar 27, 2025

Incorrect diagram for Example 8.7.16

Status: Open.

#1163 In HoTT/book;

· roconnor opened on Sep 2, 2024

Exercise 11.6 seems to need WLPO not LPO

Status: Open.

#1162 In HoTT/book;

· jkingdon opened on Aug 4, 2024

max and sup

Status: Open.

#1161 In HoTT/book;

· ncfavier opened on Jul 13, 2024

Switch to using truncated logic as default in the book

Status: Open.

#1160 In HoTT/book;

· ghost opened on Jun 19, 2024

real numbers in the introduction

Status: Open.

#1158 In HoTT/book;

· mikeshulman opened on Jun 15, 2024

cardinal numbers in the introduction

Status: Open.

#1157 In HoTT/book;

· mikeshulman opened on Jun 14, 2024

proof-theoretic consistency in the introduction

Status: Open.

#1156 In HoTT/book;

· mikeshulman opened on Jun 14, 2024