various small cosmetic changes (#4)

* various small cosmetic changes

* move Agda version comment

* fix comment

Colimit-code/README.md

@@ -52,7 +52,7 @@ check the entire development in a reasonable amount of time.
 
 1. Install Agda 2.6.3.
 2. Install the stripped, modified HoTT-Agda library under `../HoTT-Agda`.
-3. Type check the file `Main-Theorem/CosColim-Adjunction.agda`.
+3. Type-check the file `Main-Theorem/CosColim-Adjunction.agda`.
 
 ## License
 

Dockerfile

@@ -6,7 +6,7 @@ ARG GHC_VERSION=9.4.7
 FROM fossa/haskell-static-alpine:ghc-${GHC_VERSION} AS agda
 
 WORKDIR /build/agda
-ARG AGDA_VERSION=b499d12412bac32ab1af9f470463ed9dc54f8907
+ARG AGDA_VERSION=b499d12412bac32ab1af9f470463ed9dc54f8907 # Agda 2.6.3
 RUN \
   git init && \
   git remote add origin https://github.com/agda/agda.git && \
@@ -23,7 +23,7 @@ RUN \
   cabal v1-install --bindir=/dist --datadir=/dist --datasubdir=/dist/data --enable-executable-static
 
 ####################################################################################################
-# Type check Agda files
+# Type-check Agda files
 ####################################################################################################
 
 FROM alpine AS hottagda
@@ -37,7 +37,7 @@ COPY --from=agda /dist /dist
 COPY --from=hottagda /build /build
 
 COPY ["Pullback-stability", "/build/Pullback-stability"]
-COPY agdacheck.sh /
+COPY agda-html.sh /
 
 RUN echo "/build/Hott-Agda/hott-core.agda-lib" >> /dist/libraries
 RUN echo "/build/Colimit-code/cos-colim.agda-lib" >> /dist/libraries
@@ -86,6 +86,6 @@ RUN /dist/agda --library-file=/dist/libraries ./Stability.agda
 ####################################################################################################
 
 WORKDIR /build
-RUN ["chmod", "+x", "/agdacheck.sh"]
+RUN ["chmod", "+x", "/agda-html.sh"]
 
-CMD ["sh", "/agdacheck.sh"]
+CMD ["sh", "/agda-html.sh"]

HoTT-Agda/README.md

@@ -26,7 +26,7 @@ Structure of the source
 The main library is more or less divided into two parts.
 
 - The first part is exported in the module `lib.Basics` and contains everything needed to make the second
-  part compile
+  part compile.
 - The second part is found in `lib.types` and develops type formers.
 
 Note that our work on colimits makes extensive use of the `path-seq/` directory.