add remarks about missing contents

src/commutative-algebra/maximal-ideals-commutative-rings.lagda.md

@@ -18,3 +18,5 @@ module commutative-algebra.maximal-ideals-commutative-rings where
 ideal `J` such that `I ⊆ J` satisfies `1 ∉ J ⇒ I ＝ J`.
 
 ## Definition
+
+This remains to be defined.

src/foundation/partial-elements.lagda.md

@@ -42,3 +42,5 @@ pr2 (unit-partial-element x) y = x
 ## Properties
 
 ### The type of partial elements is a directed complete poset
+
+This remains to be shown.

src/foundation/products-of-tuples-of-types.lagda.md

@@ -49,5 +49,3 @@ equiv-universal-property-product-tuple-types A i =
   {!!}
   -}
 ```
-
-## Properties

src/foundation/surjective-maps.lagda.md

@@ -720,3 +720,5 @@ module _
 ```
 
 ### The type of surjections `A ↠ B` is equivalent to the type of families `P` of inhabited types over `B` equipped with an equivalence `A ≃ Σ B P`
+
+This remains to be shown.

src/foundation/truncated-equality.lagda.md

@@ -23,5 +23,3 @@ open import foundation-core.universe-levels
 trunc-eq : {l : Level} (k : 𝕋) {A : UU l} → A → A → Truncated-Type l k
 trunc-eq k x y = trunc k (x ＝ y)
 ```
-
-## Properties

src/graph-theory/edge-coloured-undirected-graphs.lagda.md

@@ -99,5 +99,3 @@ module _
   is-emb-colouring-Edge-Coloured-Undirected-Graph =
     pr2 (pr2 G)
 ```
-
-## Properties

src/group-theory/isomorphisms-concrete-groups.lagda.md

@@ -33,3 +33,5 @@ iso-Concrete-Group = iso-Large-Precategory Concrete-Group-Large-Precategory
 ## Properties
 
 ### Equivalences of concrete groups are isomorphisms of concrete groups
+
+This remains to be shown.

src/group-theory/symmetric-concrete-groups.lagda.md

@@ -99,3 +99,5 @@ module _
 ```
 
 ### Equivalent sets have isomorphic symmetric concrete groups
+
+This remains to be shown.

src/ring-theory/algebras-rings.lagda.md

@@ -31,7 +31,7 @@ operation `x y ↦ xy : M → M → M` such that
   x(y+z) = xy+xz
 ```
 
-## Definition
+## Definitions
 
 ### Non-unital algebras over a ring
 
@@ -200,3 +200,5 @@ module _
 ```
 
 ### Unital algebras over a ring
+
+This remains to be defined.

src/ring-theory/maximal-ideals-rings.lagda.md

@@ -18,3 +18,5 @@ A maximal ideal in a ring `R` is a proper ideal `I` of `R` such that for any
 ideal `J` containing `I` is either `I` or the entire ring `R`.
 
 ## Definition
+
+This remains to be defined.

src/ring-theory/quotient-rings.lagda.md

@@ -68,3 +68,5 @@ sim-congruence-ideal-Ring R I x y =
 ### The quotient ring
 
 #### The universal property of the quotient ring
+
+This remains to be defined.

src/species/unlabeled-structures-species.lagda.md

@@ -67,4 +67,6 @@ module _
   structure-unlabeled-structure-species-types = pr2 X
 ```
 
-### Equivalences of unlabeled structures of a speces
+### Equivalences of unlabeled structures of a species
+
+This remains to be defined.

src/structured-types/h-spaces.lagda.md

@@ -81,5 +81,3 @@ module _
     (x : type-H-Space) → Id (mul-H-Space x point-H-Space) x
   right-unit-law-mul-H-Space = pr2 unit-laws-mul-H-Space
 ```
-
-## Properties

src/structured-types/types-equipped-with-automorphisms.lagda.md

@@ -2,6 +2,11 @@
 
 ```agda
 module structured-types.types-equipped-with-automorphisms where
+
+open import foundation.universe-levels
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.automorphisms
 ```
 
 <details><summary>Imports</summary>
@@ -18,3 +23,24 @@ A type equipped with an automorphism is a pair consisting of a type `A` and an
 automorphism on `A`.
 
 ## Definition
+
+```agda
+Type-Aut : (l : Level) → UU (lsuc l)
+Type-Aut l = Σ (UU l) (Aut)
+
+type-Type-Aut : {l : Level} → Type-Aut l → UU l
+type-Type-Aut (X , e) = X
+
+aut-Type-Aut : {l : Level} (A : Type-Aut l) → Aut (type-Type-Aut A)
+aut-Type-Aut (X , e) = e
+```
+
+## Properties
+
+### Every type can be equipped with the identity automorpism
+
+```agda
+id-Type-Aut : {l : Level} → UU l → Type-Aut l
+pr1 (id-Type-Aut X) = X
+pr2 (id-Type-Aut X) = id-equiv
+```

src/synthetic-homotopy-theory/infinite-complex-projective-space.lagda.md

@@ -30,4 +30,6 @@ pr1 point-ℂP∞ = 𝕊¹
 pr2 point-ℂP∞ = unit-trunc-Set id-equiv
 ```
 
-### ℂP∞ as the 2-truncation of the 2-sphere
+### `ℂP∞` as the 2-truncation of the 2-sphere
+
+This remains to be defined.

src/univalent-combinatorics/complements-isolated-points.lagda.md

@@ -121,3 +121,5 @@ equiv-complement-point-UU-Fin
 ## Properties
 
 ### The map from a pointed `k+1`-element type to the complement of the point is an equivalence
+
+This remains to be shown.

src/univalent-combinatorics/decidable-equivalence-relations.lagda.md

@@ -247,7 +247,9 @@ is-finite-Decidable-Equivalence-Relation-𝔽 :
 is-finite-Decidable-Equivalence-Relation-𝔽 A =
   is-finite-Σ
     ( is-finite-Decidable-Relation-𝔽 A)
-    ( λ R → is-finite-is-equivalence-Dec-Rel-Prop-𝔽 A R)
+    ( is-finite-is-equivalence-Dec-Rel-Prop-𝔽 A)
 ```
 
 ### The number of decidable equivalence relations on a finite type is a Stirling number of the second kind
+
+This remains to be characterized.

src/univalent-combinatorics/unlabeled-rooted-trees.lagda.md

@@ -17,3 +17,5 @@ module univalent-combinatorics.unlabeled-rooted-trees where
 An unlabelled rooted tree is an unlabelled tree equipped with a vertex.
 
 ## Definition
+
+This remains to be defined.

src/univalent-combinatorics/unlabeled-trees.lagda.md

@@ -16,5 +16,3 @@ module univalent-combinatorics.unlabeled-trees where
 
 An unlabelled tree is an undirected graph `G` such that any cycle in `G` must
 have length 1.
-
-## Definition