Homotopies, equivalences, sets, and propositions#14

Merged

fizruk merged 15 commits intomainfrom 2.4-homotopies-are-equivalences

Dec 13, 2023

+1,037-2

Commits on Dec 13, 2023

Add definitions 2.4.1 to 2.4.3

Anatolay
authored and
fizruk
committed
Add most definitions for 2.4

Anatolay
authored and
fizruk
committed
Add 2.4.{4,7,8}

eyihluyc
authored and
fizruk
committed
Add 2.8 and 3.1.2

eyihluyc
authored and
fizruk
committed
Improve is-set-Unit

eyihluyc
authored and
fizruk
committed
Add is-set-prod (2.6.2 and 3.1.5)

eyihluyc
authored and
fizruk
committed
Apply autoformatting to 1.2.4
fizruk
committed
Refactor half of section 2.4
fizruk
committed
Fix navigation
fizruk
committed
Refactor equivalence-sym
fizruk
committed
Complete equivalence-trans
fizruk
committed
Prettify homotopy-id-swap a bit
fizruk
committed
Clean up Chapter 2 a bit
fizruk
committed
Split formalizations from seminar into proper files
fizruk
committed
Simplify isSet proofs by factoring out injective-equivalence
fizruk
committed