add some descriptions

src/Applicative.agda

@@ -2,6 +2,7 @@ open import 1Lab.Type
 open import 1Lab.Path
 open import 1Lab.HLevel
 
+-- Applicative fully determines the underlying Functor.
 module Applicative {ℓ} where
 
 private variable

src/CoherentlyConstant.agda

@@ -1,6 +1,7 @@
 open import 1Lab.Prelude hiding (∥_∥³; ∥-∥³-elim-set; ∥-∥³-elim-prop; ∥-∥³-rec; ∥-∥³-is-prop; ∥-∥-rec-groupoid)
 open import 1Lab.Path.Reasoning
 
+-- Coherently constant maps into groupoids, now at https://1lab.dev/1Lab.HIT.Truncation.html#maps-into-groupoids
 module CoherentlyConstant where
 
 data ∥_∥³ {ℓ} (A : Type ℓ) : Type ℓ where

src/DeMorKan.agda

@@ -1,7 +1,9 @@
-module DeMorKan where
-
 open import Cubical.Foundations.Prelude
 
+-- A silly attempt at implementing composition for the interval,
+-- for https://proofassistants.stackexchange.com/questions/2043/is-the-de-morgan-interval-kan
+module DeMorKan where
+
 -- The built-in I lives in its own "non-fibrant" universe, so Agda won't let
 -- us express partial elements and subtypes.
 -- Hence we define a "wrapper" HIT, but do not make use of its Kan structure!

src/MonoidalFibres.agda

@@ -4,6 +4,7 @@ open import Cat.Prelude
 open import Cat.Functor.Base
 open import Cat.Functor.Properties
 
+-- eso + full-on-isos functors have monoidal fibres.
 module MonoidalFibres where
 
 private variable

src/NatChurchMonoid.agda

@@ -5,6 +5,9 @@ open import Cubical.Data.Nat
 open import Cubical.Data.Sigma
 open import Cubical.Foundations.Everything
 
+-- ℕ ≃ (m : Monoid) → ⟨ m ⟩ → ⟨ m ⟩
+module NatChurchMonoid where
+
 MEndo : Type₁
 MEndo = (m : Monoid ℓ-zero) → ⟨ m ⟩ → ⟨ m ⟩
 

src/ObjectClassifier.agda

@@ -6,6 +6,7 @@ open import 1Lab.HLevel
 open import 1Lab.HLevel.Retracts
 open import 1Lab.Equiv
 
+-- Univalence from object classifiers in the sense of higher topos theory.
 module ObjectClassifier where
 
 -- The type of arrows/bundles/fibrations.

src/TangentBundles.agda

@@ -9,14 +9,13 @@ open import Homotopy.Space.Sphere
 
 open import Meta.Idiom
 
-module TangentBundles where
-
 {-
 A work-in-progress formalisation of the first part of https://www.youtube.com/watch?v=9T9B9XBjVpk
 by David Jaz Myers, Ulrik Buchholtz, Dan Christensen and Egbert Rijke, up until
 the proof of the hairy ball theorem (except I don't have enough homotopy theory yet
 to conclude that n-1 must be odd from flipΣⁿ ≡ id).
 -}
+module TangentBundles where
 
 id≃ : ∀ {ℓ} {A : Type ℓ} → A ≃ A
 id≃ = id , id-equiv

src/Untruncate.agda

@@ -1,5 +1,7 @@
 open import 1Lab.Prelude
 
+-- The identity function on homogeneous types "factors" through the propositional truncation
+-- (https://homotopytypetheory.org/2013/10/28/the-truncation-map-_-%E2%84%95-%E2%80%96%E2%84%95%E2%80%96-is-nearly-invertible)
 module Untruncate where
 
 point : ∀ {ℓ} (X : Type ℓ) → X → Type∙ ℓ
@@ -25,5 +27,5 @@ module _ {ℓ} (X : Type ℓ) (x : X) (hom : is-homogeneous X) where
   myst : (x : ∥ X ∥) → point′ x .fst
   myst x = point′ x .snd
 
-  factored : myst ∘ inc ≡ id
+  factored : myst ∘ inc ≡ id {A = X}
   factored = refl