Agda good first issues

This issue points out that the dependent universal property of colimits can be formally derived from its non-dependent counterpart, making an explicit derivation unnecessary. It also notes the equivalence of these properties to the dependent evaluation function having a section, a stronger condition than just a section of the non-dependent evaluation function.

This issue proposes adding a 'random page' button to the web interface, similar to one found in the agda-unimath project. This enhancement would provide users with a way to discover new content by navigating to a random page within the application.

This issue proposes to establish an equivalence between the concept of quasi-coherence and a generalized version of Phoa's principle. The core of the task involves proving Theorem 7.3 from a provided arXiv paper, which is likely a significant mathematical result within abstract algebra or a related field.

This issue proposes to prove a mathematical lemma (Lemma 7.6 from a specific arXiv paper) stating that finitely generated free I-algebras are quasicoherent. The proof is expected to be relatively straightforward, building upon existing concepts in abstract algebra and category theory.

This issue proposes defining the concept of an 'n-coskeletal type' within a formal system. The definition is tied to a specific inclusion of simplicial sets ($\partial\Delta^{n+1} \hookrightarrow \Delta^{n+1}$) and is known to align with an external definition from a provided arXiv paper.

This issue proposes formalizing the proof that the universe of n-types (`n-Type ℓ n`) does not have h-level `n`. While proving that `Set ℓ` is not a set is simple, this related proof is more complex and is suggested as a good first issue for contributors.

This issue proposes to establish a theoretical equivalence between 'quasicoherence' and the 'monotonicity of every endomap'. This connection is identified as a missing piece needed to prove the disjunction and conjunction properties within an algebraic context.

This issue proposes exploring the concept of localisations of synthetic categories. It's tagged as a 'good first issue', suggesting it's intended for newcomers to the project and likely involves foundational understanding or implementation of a specific aspect of synthetic categories.

This issue proposes that the mathematical concept of Δⁿ (likely referring to a finite difference operator or a similar structure) can be formally represented as a category. The goal is to establish this categorical structure within the project.

This issue proposes a theoretical proof regarding the covariance of families in a category-theoretic context. Specifically, it suggests that a covariant family remains covariant when exponentiated by another covariant family, and more generally, that covariant families are closed under exponentiation by contravariant families. This is expected to follow from a known property of left-anodyne maps and right-fibrations.

This issue proposes to demonstrate the parametricity of the category of spaces. Specifically, it states that for any object T in this category, the constant map from T to the functor mapping to T is an equivalence. This concept is further elaborated in a linked research paper.

This issue proposes to prove that left orthogonal maps are closed under pushouts in the arrow category. This is a theoretical result within category theory, likely requiring a deep understanding of abstract algebraic structures and their properties.

This issue proposes the implementation of the "structure homomorphism principle" within the project. The principle likely relates to how structures are preserved or transformed under homomorphisms, a fundamental concept in abstract algebra and category theory.

This issue aims to formally prove all equivalences for the definition of a 'Lex' modality in Homotopy Type Theory, building upon existing formalizations in a related issue. It involves translating a significant theoretical result into formal proofs within a proof assistant.

This issue proposes refactoring code related to wedge sums by leveraging the mathematical concept of a pushout product. The core idea is that the inclusion of a wedge sum into a product can be viewed as a pushout product of two points, which could lead to code deduplication and simplification.

This issue states that no subuniverse of synthetic categories can be considered Segal, and therefore cannot be a category. This conclusion is derived from a specific section of a provided arXiv paper.

This issue identifies a lack of infrastructure surrounding the existing definition of (transposing) adjunctions in the library. The core task is to implement several missing properties and characterizations of adjunctions, such as composition closure, proving equivalences are adjoints, and establishing adjoint uniqueness. This will involve significant theoretical development and implementation within the synthetic categories library.

This issue addresses a potential inconsistency in naming conventions within the `agda-synthetic-categories` repository. It specifically questions the distinction between `tr-cov-idH` and `tr-cov-hom-idH`, suggesting a cleanup to ensure clarity and uniformity in the codebase. The goal is to streamline the naming and potentially remove redundancy.