Add Makefile support for .lagda.md and make Gluing/Conservativity.agda (#101) literate

.gitignore

@@ -6,3 +6,4 @@
 *.synctex.gz
 Everything.agda
 /env/
+*.swp

Gluing/Conservativity.agda → Gluing/Conservativity.lagda.md

@@ -1,3 +1,25 @@
+---
+title: finite products are a conservative extension over the free category, via gluing of displayed categories
+abstract: >
+    To demonstate some facilities of this library,
+    we use a logical relations construction to show that the inclusion functor from the free category over a quiver Q,
+    to the free category with finite products over Q, is fully faithful.
+    Viewing free categories as proof-relevant syntactic theories of type inhabitation, this states that
+    the addition of finite product types is a conservative extension of the product-less Q-theory.
+    We normalize (potentially) product-ful Q-terms by lifting them into a normal-forms category displayed over the product-ful Q-theory,
+    where the normal-forms category is a gluing of the syntax with displayed presheaves.
+---
+
+---
+
+a.
+
+We start by importing everything we need from
+[the upstream cubical agda standard library](https://github.com/agda/cubical) and
+[this library](https://github.com/maxsnew/cubical-categorical-logic).
+
+(`--lossy-unification` just keeps the type checking time sufficiently interactive.)
+```agda
 {-# OPTIONS --safe #-}
 {-# OPTIONS --lossy-unification #-}
 module Gluing.Conservativity where
@@ -8,18 +30,17 @@ open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Structure
 open import Cubical.Data.Quiver.Base
 open import Cubical.Data.Sigma
-open import Cubical.Data.Unit
 open import Cubical.HITs.PropositionalTruncation
 
 open import Cubical.Categories.Category
 open import Cubical.Categories.Functor
 open import Cubical.Categories.Yoneda
 open import Cubical.Categories.Presheaf
+open import Cubical.Categories.Presheaf.CCC
 open import Cubical.Categories.Limits.Terminal
 open import Cubical.Categories.Limits.BinProduct
 open import Cubical.Categories.Limits.BinProduct.More
 open import Cubical.Categories.Limits.Cartesian.Base
-open import Cubical.Categories.Presheaf.CCC
 
 open import Cubical.Categories.Constructions.Free.Category.Quiver as FC
   hiding (rec)
@@ -30,53 +51,65 @@ open import
   hiding (_×_)
 import Cubical.Categories.Constructions.Elements
 open import Cubical.Categories.NaturalTransformation
-open import Cubical.Categories.Displayed.Fibration.Base
 
 open import Cubical.Categories.Displayed.Base
+open import Cubical.Categories.Displayed.Fibration.Base
 open import Cubical.Categories.Displayed.Section.Base
 open import Cubical.Categories.Displayed.Instances.Presheaf.Base
 open import Cubical.Categories.Displayed.Instances.Presheaf.Properties
 open import Cubical.Categories.Displayed.Constructions.Reindex.Properties
 open import Cubical.Categories.Displayed.Limits.BinProduct
-
-private
-  variable ℓQ ℓQ' ℓC ℓC' : Level
-
+```
+We open some frequently used namespaces for convenience.
+```agda
 open Category
 open Functor
-open Categoryᴰ
-open Section
 open NatTrans
 open Cubical.Categories.Constructions.Elements.Contravariant
+open Categoryᴰ
+open Section
 open CartesianOver
-
+```
+A free category with finite products TODO
+```agda
 Quiver→×Quiver : ∀{ℓ ℓ' : Level} → Quiver ℓ ℓ' → ×Quiver ℓ ℓ'
 Quiver→×Quiver Q .fst = Q .fst
 Quiver→×Quiver Q .snd .ProductQuiver.mor = Q .snd .QuiverOver.mor
 Quiver→×Quiver Q .snd .ProductQuiver.dom = ↑_ ∘S Q .snd .QuiverOver.dom
 Quiver→×Quiver Q .snd .ProductQuiver.cod = ↑_ ∘S Q .snd .QuiverOver.cod
-
-module _ (Q : Quiver ℓQ ℓQ') where
+```
+Everything is relative to a Quiver/Signature TODO
+```agda
+module _ {ℓQ ℓQ'} (Q : Quiver ℓQ ℓQ') where
   private module Q = QuiverOver (Q .snd)
 
+```
+Q-Category
+```agda
   FREE : Category _ _
   FREE = FreeCat Q
 
-  private
-    module 𝓟FREEᴰ = Categoryᴰ (PRESHEAFᴰ FREE (ℓ-max ℓQ ℓQ') (ℓ-max ℓQ ℓQ'))
-
+```
+Q-(Category with finite products)
+```agda
   FREE-1,× : CartesianCategory _ _
   FREE-1,× = FreeCartesianCategory (Quiver→×Quiver Q)
 
   ı : Interp Q (FREE-1,× .fst)
   ı ._$g_ = ↑_
   ı ._<$g>_ = ↑ₑ_
-
+```
+the "main culprit"
+```agda
   ⊆ : Functor FREE (FREE-1,× .fst)
   ⊆ = FC.rec Q ı
 
-  -- the use of rec to define the functor is just to save work, since no
-  -- specific behavior on non-atoms is required
+```
+the use of rec to define the functor is just to save work, since no specific
+behavior on non-atoms is required
+
+contrast this with `nerve` later
+```agda
   extension : Functor (FREE-1,× .fst) (PresheafCategory FREE _)
   extension = FCC.rec (Quiver→×Quiver Q)
     (PresheafCategory FREE _ , ⊤𝓟 _ _ , ×𝓟 _ _)
@@ -101,9 +134,11 @@ module _ (Q : Quiver ℓQ ℓQ') where
   ⊆-Faithful : isFaithful ⊆
   ⊆-Faithful = isFaithful-GF→isFaithful-F ⊆ extension comp-Faithful
 
-  -- same type as `extension` but very different usage, and now we *do* care
-  -- about the definitional behavior on non-atoms (ie F-hom), or else we get
-  -- stuck in ⊆-Full
+```
+same type as `extension` but very different usage, and now we *do* care about
+the definitional behavior on non-atoms (ie F-hom), or else we get stuck in
+⊆-Full
+```agda
   nerve : Functor (FREE-1,× .fst) (PresheafCategory FREE _)
   nerve .F-ob Γ .F-ob A =
     (FREE-1,× .fst) [ ⊆ ⟅ A ⟆ , Γ ] , FREE-1,× .fst .isSetHom
@@ -116,7 +151,11 @@ module _ (Q : Quiver ℓQ ℓQ') where
   nerve .F-seq _ _ = makeNatTransPath
     (funExt (λ _ → funExt (λ _ → sym (FREE-1,× .fst .⋆Assoc _ _ _))))
 
-  S : Section nerve (PRESHEAFᴰ FREE _ _)
+  private
+    𝓟ᴰFREE = PRESHEAFᴰ FREE (ℓ-max ℓQ ℓQ') (ℓ-max ℓQ ℓQ')
+    module 𝓟ᴰFREE = Categoryᴰ 𝓟ᴰFREE
+
+  S : Section nerve 𝓟ᴰFREE
   S = elimLocal' (Quiver→×Quiver Q)
     (LiftedTerminalReindex (PRESHEAFᴰ-VerticalTerminals FREE _ _ _))
     (LiftedBinProductsReindex'
@@ -125,7 +164,7 @@ module _ (Q : Quiver ℓQ ℓQ') where
     OB
     HOM
     where
-    OB : (o : FREE .ob) → Presheafᴰ FREE _ _ (nerve ⟅ ⊆ ⟅ o ⟆ ⟆)
+    OB : (o : FREE .ob) → Presheafᴰ _ _ _ (nerve ⟅ ⊆ ⟅ o ⟆ ⟆)
     OB o .F-ob (o' , o'→×o) = (Σ[ f ∈ FREE [ o' , o ] ] ⊆ ⟪ f ⟫ ≡ o'→×o) ,
       isSetΣ (FREE .isSetHom)
       (λ _ → isSet→isGroupoid (FREE-1,× .fst .isSetHom) _ _)
@@ -137,20 +176,23 @@ module _ (Q : Quiver ℓQ ℓQ') where
     OB o .F-seq _ _ = funExt (λ _ → ΣPathP (FREE .⋆Assoc _ _ _ ,
       isSet→SquareP (λ _ _ → FREE-1,× .fst .isSetHom) _ _ _ _))
     HOM : (e : Q.mor) →
-      𝓟FREEᴰ.Hom[ nerve ⟪ ⊆ ⟪ ↑ e ⟫ ⟫ ][ OB (Q.dom e) , OB (Q.cod e) ]
+      𝓟ᴰFREE.Hom[ nerve ⟪ ⊆ ⟪ ↑ e ⟫ ⟫ ][ OB (Q.dom e) , OB (Q.cod e) ]
     HOM e = natTrans
       (λ (o , o→×∙e) (witness-o→∙e , p) →
         ↑ e ∘⟨ FREE ⟩ witness-o→∙e , ⊆ .F-seq _ _ ∙
         congS (λ x → ⊆ ⟪ ↑ e ⟫ ∘⟨ FREE-1,× .fst ⟩ x) p)
       λ f → funExt (λ _ → ΣPathP (FREE .⋆Assoc _ _ _ ,
         isSet→SquareP (λ _ _ → FREE-1,× .fst .isSetHom) _ _ _ _))
 
+```
+instantiate gluing argument
+```agda
   ⊆-Full : isFull ⊆
   ⊆-Full o o' F[f] = ∣ f , p ∙ FREE-1,× .fst .⋆IdL _ ∣₁
     where
-    ⊆[→o'] : 𝓟FREEᴰ.ob[ nerve ⟅ ⊆ ⟅ o' ⟆ ⟆ ]
+    ⊆[→o'] : 𝓟ᴰFREE.ob[ nerve ⟅ ⊆ ⟅ o' ⟆ ⟆ ]
     ⊆[→o'] = S .F-obᴰ (⊆ ⟅ o' ⟆)
-    ⊆[→o']* : 𝓟FREEᴰ.ob[ nerve ⟅ ⊆ ⟅ o ⟆ ⟆ ]
+    ⊆[→o']* : 𝓟ᴰFREE.ob[ nerve ⟅ ⊆ ⟅ o ⟆ ⟆ ]
     ⊆[→o']* = PRESHEAFᴰ-AllCartesianOvers _ _ _ ⊆[→o'] (nerve ⟪ F[f] ⟫) .f*cᴰ'
     f,p : ⟨ ⊆[→o']* ⟅ o , FREE-1,× .fst .id ⟆ ⟩
     f,p = (S .F-homᴰ F[f] ⟦ o , FREE-1,× .fst .id ⟧) (FREE .id , refl)
@@ -159,5 +201,9 @@ module _ (Q : Quiver ℓQ ℓQ') where
     p : ⊆ ⟪ f ⟫ ≡ FREE-1,× .fst .id ⋆⟨ FREE-1,× .fst ⟩ F[f]
     p = f,p .snd
 
+```
+And finally,
+```agda
   ⊆-FullyFaithful : isFullyFaithful ⊆
   ⊆-FullyFaithful = isFull+Faithful→isFullyFaithful {F = ⊆} ⊆-Full ⊆-Faithful
+```

Makefile

@@ -1,8 +1,9 @@
 AGDA = agda +RTS -M6G -RTS
+PANDOC = pandoc
 FIX_WHITESPACE = fix-whitespace
 
-# Finds all .agda files in the current directory and subdirectories
-FIND_AGDA_FILES = find . -name "*.agda"
+# Finds all .agda or .lagda.* files in the current directory and subdirectories
+FIND_AGDA_FILES = find . \( -name "*.agda" -o -name "*.lagda.*" \) ! -exec git check-ignore -q '{}' \; -print
 AGDA_FILES = $(shell $(FIND_AGDA_FILES))
 
 # The targets are the .agdai files corresponding to the .agda files
@@ -15,6 +16,10 @@ all: test check-whitespace check-line-lengths
 test: Everything.agda
 	$(AGDA) $<
 
+html: Everything.agda
+	$(AGDA) --html --html-dir='$@' --highlight-occurrences --html-highlight=auto '$<'
+	find '$@' -name '*.md' -exec bash -c "$(PANDOC) -f markdown \"\$$1\" -t html -o \"\$${1%.md}.html\" --embed-resources --standalone --css='$@'/Agda.css --include-in-header=<(echo '<script>'; cat '$@'/highlight-hover.js; echo '</script>')" bash '{}' \;
+
 .PHONY: test-and-report
 test-and-report:
 	@failed=""; \
@@ -40,7 +45,7 @@ check-line-lengths:
 # PHONY in case agda files are created/deleted
 .PHONY: Everything.agda
 Everything.agda:
-	$(FIND_AGDA_FILES) ! -path './$@' | sed -e 's#/#.#g' -e 's/^\.*//' -e 's/.agda$$//' -e 's/^/import /' | LC_ALL=C sort > $@
+	$(FIND_AGDA_FILES) ! -path './$@' | sed -e 's#/#.#g' -e 's/^\.*//' -e 's/\.agda$$//' -e 's/\.lagda\..*$$//' -e 's/^/import /' | LC_ALL=C sort > $@
 
 .PHONY: clean
 clean: