From 6d5689e6d54991921c69162ff5a91d6d48481f21 Mon Sep 17 00:00:00 2001 From: Johnson He Date: Thu, 8 Aug 2024 00:02:17 +0000 Subject: [PATCH 1/6] support literate agda (currently only markdown) --- ...{Conservativity.agda => Conservativity.lagda.md} | 13 +++++++++++++ Makefile | 11 ++++++++--- 2 files changed, 21 insertions(+), 3 deletions(-) rename Gluing/{Conservativity.agda => Conservativity.lagda.md} (98%) diff --git a/Gluing/Conservativity.agda b/Gluing/Conservativity.lagda.md similarity index 98% rename from Gluing/Conservativity.agda rename to Gluing/Conservativity.lagda.md index 0d0fd594..a792fb6a 100644 --- a/Gluing/Conservativity.agda +++ b/Gluing/Conservativity.lagda.md @@ -1,3 +1,8 @@ +--- +title: Conservativity +--- + +```agda {-# OPTIONS --safe #-} {-# OPTIONS --lossy-unification #-} module Gluing.Conservativity where @@ -49,13 +54,20 @@ open Section open NatTrans open Cubical.Categories.Constructions.Elements.Contravariant open CartesianOver +``` + +and test this markdown?? + +```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 +``` +```agda module _ (Q : Quiver ℓQ ℓQ') where private module Q = QuiverOver (Q .snd) @@ -161,3 +173,4 @@ module _ (Q : Quiver ℓQ ℓQ') where ⊆-FullyFaithful : isFullyFaithful ⊆ ⊆-FullyFaithful = isFull+Faithful→isFullyFaithful {F = ⊆} ⊆-Full ⊆-Faithful +``` diff --git a/Makefile b/Makefile index ed85a78e..b4be8741 100644 --- a/Makefile +++ b/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.*" \) 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 $(PANDOC) -f markdown '{}' -t html -o '$@'/Gluing.Conservativity.html --embed-resources --standalone --css='$@'/Agda.css \; + .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: From f9c17bd646edc935a913de39e2eb6e15ef9551d0 Mon Sep 17 00:00:00 2001 From: Johnson He Date: Thu, 8 Aug 2024 01:40:21 +0000 Subject: [PATCH 2/6] fix --highlight-occurrences for pandoc'd literate agda files --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index b4be8741..98285c9f 100644 --- a/Makefile +++ b/Makefile @@ -18,7 +18,7 @@ test: Everything.agda html: Everything.agda $(AGDA) --html --html-dir='$@' --highlight-occurrences --html-highlight=auto '$<' - find '$@' -name '*.md' -exec $(PANDOC) -f markdown '{}' -t html -o '$@'/Gluing.Conservativity.html --embed-resources --standalone --css='$@'/Agda.css \; + find '$@' -name '*.md' -exec bash -c "$(PANDOC) -f markdown '{}' -t html -o '$@'/Gluing.Conservativity.html --embed-resources --standalone --css='$@'/Agda.css --include-in-header=<(echo '')" \; .PHONY: test-and-report test-and-report: From 0c3c6a94c80812d948cd61f307bba9613ba6c6e0 Mon Sep 17 00:00:00 2001 From: Johnson He Date: Thu, 8 Aug 2024 08:57:08 +0000 Subject: [PATCH 3/6] fix Makefile --- .gitignore | 1 + Makefile | 5 +++-- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/.gitignore b/.gitignore index 827a100b..69a3022e 100644 --- a/.gitignore +++ b/.gitignore @@ -6,3 +6,4 @@ *.synctex.gz Everything.agda /env/ +*.swp diff --git a/Makefile b/Makefile index 98285c9f..3b24d9e6 100644 --- a/Makefile +++ b/Makefile @@ -3,7 +3,7 @@ PANDOC = pandoc FIX_WHITESPACE = fix-whitespace # Finds all .agda or .lagda.* files in the current directory and subdirectories -FIND_AGDA_FILES = find . \( -name "*.agda" -o -name "*.lagda.*" \) +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 @@ -18,7 +18,8 @@ test: Everything.agda html: Everything.agda $(AGDA) --html --html-dir='$@' --highlight-occurrences --html-highlight=auto '$<' - find '$@' -name '*.md' -exec bash -c "$(PANDOC) -f markdown '{}' -t html -o '$@'/Gluing.Conservativity.html --embed-resources --standalone --css='$@'/Agda.css --include-in-header=<(echo '')" \; + # TODO: Gluing.Conservativity.html is hardcoded right now + find '$@' -name '*.md' -exec bash -c "$(PANDOC) -f markdown \"\$$1\" -t html -o '$@'/Gluing.Conservativity.html --embed-resources --standalone --css='$@'/Agda.css --include-in-header=<(echo '')" bash '{}' \; .PHONY: test-and-report test-and-report: From 8652e7eb01932aeab5648e00ce219b43a1ebed42 Mon Sep 17 00:00:00 2001 From: Johnson He Date: Thu, 8 Aug 2024 18:03:09 +0000 Subject: [PATCH 4/6] remove Makefile path hardcoding in literate agda compilation --- Makefile | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Makefile b/Makefile index 3b24d9e6..e433e104 100644 --- a/Makefile +++ b/Makefile @@ -18,8 +18,7 @@ test: Everything.agda html: Everything.agda $(AGDA) --html --html-dir='$@' --highlight-occurrences --html-highlight=auto '$<' - # TODO: Gluing.Conservativity.html is hardcoded right now - find '$@' -name '*.md' -exec bash -c "$(PANDOC) -f markdown \"\$$1\" -t html -o '$@'/Gluing.Conservativity.html --embed-resources --standalone --css='$@'/Agda.css --include-in-header=<(echo '')" bash '{}' \; + 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 '')" bash '{}' \; .PHONY: test-and-report test-and-report: From b6b7ebe9719192a9b0b41e1e70150c7a5fcbd003 Mon Sep 17 00:00:00 2001 From: Johnson He Date: Thu, 8 Aug 2024 19:16:22 +0000 Subject: [PATCH 5/6] init lagda --- Gluing/Conservativity.lagda.md | 95 ++++++++++++++++++++++++---------- 1 file changed, 68 insertions(+), 27 deletions(-) diff --git a/Gluing/Conservativity.lagda.md b/Gluing/Conservativity.lagda.md index a792fb6a..98216f73 100644 --- a/Gluing/Conservativity.lagda.md +++ b/Gluing/Conservativity.lagda.md @@ -1,7 +1,20 @@ --- -title: Conservativity +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 of the free Q-category (free category over a quiver Q) + in the free Q-category with finite products (free category with finite products over a quiver Q) is fully faithful. + Viewing free categories as syntactic term languages, this states that adding finite product types is a conservative extension of type inhabitation of the base Q-theory. + +--- + --- +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` keeps the type checking time sufficiently interactive.) ```agda {-# OPTIONS --safe #-} {-# OPTIONS --lossy-unification #-} @@ -13,18 +26,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) @@ -35,30 +47,38 @@ 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 - +``` +Before doing anything, we declare some implicit universe levels that +parameterize this example. +So although there is no motive as of yet, we + +`ℓQ` of (the type of) Quiver objects, +`ℓQ'` of (the type of) Quiver edges, +`ℓC` of (the type of) Category objects, +and `ℓC'` of (the type of) Category morphisms. +```agda 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 ``` - -and test this markdown?? - - +A free category with finite products TODO ```agda Quiver→×Quiver : ∀{ℓ ℓ' : Level} → Quiver ℓ ℓ' → ×Quiver ℓ ℓ' Quiver→×Quiver Q .fst = Q .fst @@ -66,29 +86,38 @@ 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 ``` - +Everything is relative to a Quiver/Signature TODO ```agda module _ (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 _ , ⊤𝓟 _ _ , ×𝓟 _ _) @@ -113,9 +142,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 @@ -128,7 +159,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' @@ -137,7 +172,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) _ _) @@ -149,7 +184,7 @@ 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 _ _ ∙ @@ -157,12 +192,15 @@ module _ (Q : Quiver ℓQ ℓQ') where λ 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) @@ -171,6 +209,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 ``` From 24ee7e248d3d1eca0dbc21fab6f2c7f6d833ea79 Mon Sep 17 00:00:00 2001 From: Johnson He Date: Mon, 12 Aug 2024 22:42:15 +0000 Subject: [PATCH 6/6] abstract --- Gluing/Conservativity.lagda.md | 28 ++++++++++------------------ 1 file changed, 10 insertions(+), 18 deletions(-) diff --git a/Gluing/Conservativity.lagda.md b/Gluing/Conservativity.lagda.md index 98216f73..73d3d1fb 100644 --- a/Gluing/Conservativity.lagda.md +++ b/Gluing/Conservativity.lagda.md @@ -2,19 +2,23 @@ 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 of the free Q-category (free category over a quiver Q) - in the free Q-category with finite products (free category with finite products over a quiver Q) is fully faithful. - Viewing free categories as syntactic term languages, this states that adding finite product types is a conservative extension of type inhabitation of the base Q-theory. - + 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` keeps the type checking time sufficiently interactive.) +(`--lossy-unification` just keeps the type checking time sufficiently interactive.) ```agda {-# OPTIONS --safe #-} {-# OPTIONS --lossy-unification #-} @@ -56,18 +60,6 @@ open import Cubical.Categories.Displayed.Instances.Presheaf.Properties open import Cubical.Categories.Displayed.Constructions.Reindex.Properties open import Cubical.Categories.Displayed.Limits.BinProduct ``` -Before doing anything, we declare some implicit universe levels that -parameterize this example. -So although there is no motive as of yet, we - -`ℓQ` of (the type of) Quiver objects, -`ℓQ'` of (the type of) Quiver edges, -`ℓC` of (the type of) Category objects, -and `ℓC'` of (the type of) Category morphisms. -```agda -private - variable ℓQ ℓQ' ℓC ℓC' : Level -``` We open some frequently used namespaces for convenience. ```agda open Category @@ -88,7 +80,7 @@ Quiver→×Quiver Q .snd .ProductQuiver.cod = ↑_ ∘S Q .snd .QuiverOver.cod ``` Everything is relative to a Quiver/Signature TODO ```agda -module _ (Q : Quiver ℓQ ℓQ') where +module _ {ℓQ ℓQ'} (Q : Quiver ℓQ ℓQ') where private module Q = QuiverOver (Q .snd) ```