Search results

Salvage work from #885

help wantedExtra attention is neededExtra attention is needed

refactoring

synthetic-homotopy-theory

Status: Open.

Feature

#1516 In UniMath/agda-unimath;

· fredrik-bakke opened on Sep 1, 2025

Refactor <code>synthetic-homotopy-theory.universal-cover-circle</code>

foundation

refactoring

synthetic-homotopy-theory

Status: Open.

Task

#1515 In UniMath/agda-unimath;

· fredrik-bakke opened on Sep 1, 2025

Formalize the smash product as a pushout of half-smash products

formalization-target

synthetic-homotopy-theory

Status: Open.

#1326 In UniMath/agda-unimath;

· fredrik-bakke opened on Feb 14, 2025

Postulating colimits

computational-behavior

refactoring

synthetic-homotopy-theory

Status: Open.

#1122 In UniMath/agda-unimath;

· fredrik-bakke opened on Apr 20, 2024

Construct <code>compute-glue-cogap</code> from appropriate infrastructure

synthetic-homotopy-theory

Status: Open.

#1120 In UniMath/agda-unimath;

· fredrik-bakke opened on Apr 19, 2024

Target: Sequential Colimits in Homotopy Type Theory

formalization-target

synthetic-homotopy-theory

Status: Open.

#1080 In UniMath/agda-unimath;

· VojtechStep opened on Mar 15, 2024

Project: Sheaves and excision with respect to regular cd-structures

formalization-target

orthogonal-factorization-systems

synthetic-homotopy-theory

Status: Open.

#930 In UniMath/agda-unimath;

· EgbertRijke opened on Nov 21, 2023

Stable homotopy groups

synthetic-homotopy-theory

Status: Open.

#842 In UniMath/agda-unimath;

· fredrik-bakke opened on Oct 14, 2023

The long exact sequence of homotopy groups

good first issueGood for newcomersGood for newcomers

synthetic-homotopy-theory

Status: Open.

#834 In UniMath/agda-unimath;

· fredrik-bakke opened on Oct 12, 2023

Define <code>ℂP∞</code> as the <code>2</code>-truncation of the <code>2</code>-sphere

good first issueGood for newcomersGood for newcomers

synthetic-homotopy-theory

Status: Open.

#742 In UniMath/agda-unimath;

· fredrik-bakke opened on Sep 10, 2023

Formalize the Hopf Fibration

formalization-target

synthetic-homotopy-theory

Status: Open.

#702 In UniMath/agda-unimath;

· morphismz opened on Aug 21, 2023

Formalize asserted connections between postulates in design principles

documentationImprovements or additions to documentationImprovements or additions to documentation

formalization-target

foundation

good first issueGood for newcomersGood for newcomers

group-theory

synthetic-homotopy-theory

Status: Open.

#637 In UniMath/agda-unimath;

· fredrik-bakke opened on Jun 4, 2023