From ba81ea67260362c9a0b457410d62d64441ee7a7a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia=20Liao?= Date: Fri, 21 Jun 2024 12:04:00 -0300 Subject: [PATCH] use copatterns to define Sheaves; fully eta-expand --- src/1Lab/Reflection/Copattern.agda | 104 ++++++++++-------- src/1Lab/Reflection/Signature.agda | 12 ++ src/1Lab/Reflection/Subst.agda | 2 +- src/Cat/Abelian/Images.lagda.md | 12 +- .../Diagram/Equaliser/RegularMono.lagda.md | 14 +-- src/Cat/Diagram/Image.lagda.md | 8 +- src/Cat/Functor/Algebra.lagda.md | 2 +- src/Cat/Functor/FullSubcategory.lagda.md | 42 ++----- src/Cat/Instances/Sheaves.lagda.md | 1 + .../Diagram/Monoid/Representable.lagda.md | 15 ++- src/Cat/Morphism/StrongEpi.lagda.md | 4 +- src/Cat/Site/Base.lagda.md | 13 +-- src/Data/Reflection/Term.agda | 20 +++- 13 files changed, 135 insertions(+), 114 deletions(-) diff --git a/src/1Lab/Reflection/Copattern.agda b/src/1Lab/Reflection/Copattern.agda index e899e2c72..bef34de02 100644 --- a/src/1Lab/Reflection/Copattern.agda +++ b/src/1Lab/Reflection/Copattern.agda @@ -29,31 +29,40 @@ make-copattern declare? def-name tm tp = do -- Agda will insert implicits when defining copatterns even -- with 'withExpandLast true', so we need to do implicit instantiation - -- by hand. First, we strip off all leading implicits from the field type. - let (implicit-tele , tp) = pi-impl-view field-tp - let nimplicits = length implicit-tele - let clause-tele = tele ++ implicit-tele - - -- Construct the pattern portion of the clause, making sure to bind - -- all implicit variables. Note that copattern projections are always visible. - let pat = - tel→pats nimplicits tele ++ - arg (set-visibility visible field-info) (proj field-name) ∷ - tel→pats 0 implicit-tele - - -- Construct the body of the clause, making sure to apply all arguments - -- bound outside the copattern match, and instantiate all implicit arguments. - -- We also need to apply all of the implicit arguments to 'tm'. + -- by hand. There are also cases where it's better to fully + -- eta-expand than not (e.g. the 'helper' we're expanding has a + -- field defined by lazy matching, which does not reduce unless + -- applied, and would cause duplication of the big input term). So + -- we fully eta-expand clauses here. + -- First, we strip off all leading quantifiers from the field + -- type. + let + (field-tele , tp) = pi-view field-tp + nargs = length field-tele + clause-tele = tele ++ field-tele + + -- Construct the pattern portion of the clause, making sure to + -- bind all variables. Note that copattern projections are always + -- visible. + let + pat = tel→pats nargs tele ++ + arg (set-visibility visible field-info) (proj field-name) ∷ + tel→pats 0 field-tele + + -- Construct the body of the clause, making sure to apply all + -- arguments bound outside the copattern match, and apply the + -- eta-expanded arguments. We also need to apply all of the + -- implicit arguments to 'tm'. body ← in-context (reverse clause-tele) $ - reduce (def field-name (argN (raise nimplicits inst-tm) ∷ tel→args 0 implicit-tele)) + reduce (def field-name (raise nargs inst-tm v∷ tel→args 0 field-tele)) -- Construct the final clause. pure $ clause clause-tele pat body -- Define a copattern binding, and predeclare its type if required. case declare? of λ where - true → declare (argN def-name) tp + true → declare (argN def-name) tp <|> pure tt false → pure tt -- Construct the final copattern. @@ -82,6 +91,17 @@ repack-record tm tp = do -- Builld a pointwise repacking. pure (tel→lam tele (con ctor args)) +-- Helper for the 'define' macros; Unifies the given goal with the type +-- of the given function, if it has been defined. If the function has +-- not been defined, and the first argument is 'false', then an error is +-- raised. +type-for : String → Bool → Name → Term → TC ⊤ +type-for tac decl? fun goal with decl? +... | true = (unify goal =<< get-type fun) <|> pure tt +... | false = (unify goal =<< get-type fun) <|> typeError + [ "define-" , strErr tac , ": the function " , nameErr fun , " should already have been declared." + ] + -------------------------------------------------------------------------------- -- Usage @@ -94,8 +114,10 @@ If you wish to give the binding a type annotation, you can also use > copat : Your-type > unquoteDecl copat = declare-copattern copat thing-to-be-expanded -All features of non-recursive records are supported, including instance -fields and fields with implicit arguments. +Note that, in this case, the thing-to-be-expanded must have exactly the +same type as the binding `copat`. All features of non-recursive records +are supported, including instance fields and fields with implicit +arguments. These macros also allow you to lift functions 'A → some-record-type' into copattern definitions. Note that Agda will generate meta for @@ -109,10 +131,13 @@ declare-copattern {A = A} nm x = do `A ← quoteTC A make-copattern true nm `x `A -define-copattern : ∀ {ℓ} {A : Type ℓ} → Name → A → TC ⊤ -define-copattern {A = A} nm x = do - `x ← quoteTC x +define-copattern + : ∀ {ℓ} (nm : Name) + → {@(tactic (type-for "copattern" true nm)) A : Type ℓ} + → A → TC ⊤ +define-copattern nm {A = A} x = do `A ← quoteTC A + `x ← define-abbrev nm "value" `A =<< quoteTC x make-copattern false nm `x `A {- @@ -121,32 +146,19 @@ they cannot be quoted into any `Type ℓ`. With this in mind, we also provide a pair of macros that work over `Typeω` instead. -} --- Helper for the 'define' macros; Unifies the given goal with the type --- of the given function, if it has been defined. If the function has --- not been defined, and the first argument is 'false', then an error is --- raised. -type-for : Bool → Name → Term → TC ⊤ -type-for decl? fun goal with decl? -... | true = (unify goal =<< get-type fun) <|> pure tt -... | false = (unify goal =<< get-type fun) <|> typeError - [ "define-copattern-levels: the function " , nameErr fun , " should already have been declared." - ] - -declare-copattern-levels - : (nm : Name) {@(tactic (type-for true nm)) U : Typeω} - → U → TC ⊤ -declare-copattern-levels nm A = do +declare-copatternω : ∀ {U : Typeω} → Name → U → TC ⊤ +declare-copatternω nm A = do `A ← quoteωTC A -- Cannot quote things in type Typeω, but we can infer their type. `U ← infer-type `A make-copattern true nm `A `U -define-copattern-levels - : (nm : Name) {@(tactic (type-for false nm)) U : Typeω} +define-copatternω + : (nm : Name) {@(tactic (type-for "copatternω" false nm)) U : Typeω} → U → TC ⊤ -define-copattern-levels nm A = do - `A ← quoteωTC A +define-copatternω nm A = do `U ← get-type nm + `A ← define-abbrev nm "value" `U =<< quoteωTC A make-copattern false nm `A `U {- @@ -206,7 +218,11 @@ private module Test where zero-unused-param = record { actual = 0 } one-unused-param : ∀ {n} → Unused n - unquoteDef one-unused-param = define-copattern one-unused-param zero-unused-param + unquoteDef one-unused-param = declare-copattern one-unused-param zero-unused-param + -- This is a type error: + -- unquoteDef one-unused-param = define-copattern one-unused-param zero-unused-param + -- because the 'define' macro propagates the type of the thing being + -- defined inwards. -- Functions into records that are universe polymorphic neat : ∀ {ℓ} {A : Type ℓ} → A → Record A @@ -217,11 +233,11 @@ private module Test where -- Implicit insertion is correct for the define- macro, since the type -- of the function is given. cool : ∀ {ℓ} {A : Type ℓ} → A → Record A - unquoteDef cool = define-copattern-levels cool neat + unquoteDef cool = define-copatternω cool neat -- Eta-expanders expander : ∀ {m n : Nat} → Unused m → Unused n unquoteDef expander = define-eta-expansion expander -- Raises a type error: the function should have a declaration. - -- unquoteDecl uncool = define-copattern-levels uncool neat + -- unquoteDecl uncool = define-copatternω uncool neat diff --git a/src/1Lab/Reflection/Signature.agda b/src/1Lab/Reflection/Signature.agda index 222931d7d..c2c766998 100644 --- a/src/1Lab/Reflection/Signature.agda +++ b/src/1Lab/Reflection/Signature.agda @@ -211,6 +211,18 @@ helper-function def-nm suf ty cls = do _ → define-function nm cls pure nm +-- Given a well-typed `val : ty`, return a definitionally-equal atomic +-- term equal to `val`, potentially by lifting it into the signature. +-- See 'helper-function' for the naming scheme. +define-abbrev : Name → String → Term → Term → TC Term +define-abbrev def-nm suf ty val with is-atomic-tree? val +... | true = pure val +... | false = do + let (tel , _) = pi-impl-view ty + nm ← helper-function def-nm suf ty + [ clause tel (tel→pats 0 tel) (apply-tm* val (tel→args 0 tel)) ] + pure (def₀ nm) + private make-args : Nat → List (Arg Nat) → List (Arg Term) make-args n xs = reverse $ map (λ (arg ai i) → arg ai (var (n - i - 1) [])) xs diff --git a/src/1Lab/Reflection/Subst.agda b/src/1Lab/Reflection/Subst.agda index f0315037f..fd1b84c4e 100644 --- a/src/1Lab/Reflection/Subst.agda +++ b/src/1Lab/Reflection/Subst.agda @@ -142,7 +142,7 @@ subst-tm ρ (agda-sort s) with s subst-tel ρ [] = [] subst-tel ρ ((x , arg ai t) ∷ xs) = (x , arg ai (subst-tm ρ t)) ∷ subst-tel (liftS 1 ρ) xs -subst-clause σ (clause tel ps t) = clause (subst-tel σ tel) ps (subst-tm (wkS (length tel) σ) t) +subst-clause σ (clause tel ps t) = clause (subst-tel σ tel) ps (subst-tm (liftS (length tel) σ) t) subst-clause σ (absurd-clause tel ps) = absurd-clause (subst-tel σ tel) ps _<#>_ : Term → Arg Term → Term diff --git a/src/Cat/Abelian/Images.lagda.md b/src/Cat/Abelian/Images.lagda.md index 7f7581774..2643fb589 100644 --- a/src/Cat/Abelian/Images.lagda.md +++ b/src/Cat/Abelian/Images.lagda.md @@ -53,8 +53,8 @@ images : ∀ {A B} (f : Hom A B) → Image C f images f = im where the-img : ↓Obj (const! (cut f)) Forget-full-subcat the-img .x = tt - the-img .y .object = cut (Ker.kernel (Coker.coeq f)) - the-img .y .witness {c} = kernels-are-subobjects C ∅ _ (Ker.has-is-kernel _) + the-img .y .fst = cut (Ker.kernel (Coker.coeq f)) + the-img .y .snd {c} = kernels-are-subobjects C ∅ _ (Ker.has-is-kernel _) ``` Break $f$ down as an epi $p : A \epi \ker (\coker f)$ followed by a mono @@ -128,7 +128,7 @@ a (unique) map $\coker (\ker f) \to X$ s.t. the triangle above commutes! where abstract path : other .map .map ∘ 0m ≡ other .map .map ∘ kernel f .Kernel.kernel path = - other .y .witness _ _ $ sym $ + other .y .snd _ _ $ sym $ pulll (other .map .commutes) ·· Ker.equal f ·· ∅.zero-∘r _ @@ -154,14 +154,14 @@ is the image of $f$. (coker-ker≃ker-coker f .is-invertible.invr))) refl ∙ pullr (Coker.factors _) ∙ other .map .commutes) (sym (decompose f .snd ∙ assoc _ _ _)) - factor .sq = /-Hom-path $ sym $ other .y .witness _ _ $ + factor .sq = /-Hom-path $ sym $ other .y .snd _ _ $ pulll (factor .β .commutes) ∙ the-img .map .commutes ·· sym (other .map .commutes) - ·· ap (other .y .object .map ∘_) (intror refl) + ·· ap (other .y .fst .map ∘_) (intror refl) unique : ∀ x → factor ≡ x - unique x = ↓Hom-path _ _ refl $ /-Hom-path $ other .y .witness _ _ $ + unique x = ↓Hom-path _ _ refl $ /-Hom-path $ other .y .snd _ _ $ sym (x .β .commutes ∙ sym (factor .β .commutes)) ``` diff --git a/src/Cat/Diagram/Equaliser/RegularMono.lagda.md b/src/Cat/Diagram/Equaliser/RegularMono.lagda.md index 36771ad51..4a6d3780c 100644 --- a/src/Cat/Diagram/Equaliser/RegularMono.lagda.md +++ b/src/Cat/Diagram/Equaliser/RegularMono.lagda.md @@ -43,7 +43,7 @@ is an [[equaliser]] of some pair of arrows $g, h : b \to c$. {c} : Ob arr₁ arr₂ : Hom b c has-is-eq : is-equaliser C arr₁ arr₂ f - + open is-equaliser has-is-eq public ``` @@ -53,7 +53,7 @@ are in fact monomorphisms: ```agda is-regular-mono→is-mono : is-monic f is-regular-mono→is-mono = is-equaliser→is-monic _ has-is-eq - + open is-regular-mono using (is-regular-mono→is-mono) public ``` @@ -126,7 +126,7 @@ $\phi \circ i_2 = \rm{arr_2}$. ```agda phi : Hom f⊔f.coapex reg.c phi = f⊔f.universal reg.equal - + open is-effective-mono mon : is-effective-mono C f mon .cokernel = f⊔f.coapex @@ -201,12 +201,12 @@ the code below demonstrates. → M-image C (is-regular-mono C , is-regular-mono→is-mono) f is-effective-mono→image {f = f} mon = im where module eff = is-effective-mono mon - + itself : ↓Obj _ _ itself .x = tt - itself .y = restrict (cut f) eff.is-effective-mono→is-regular-mono + itself .y = cut f , eff.is-effective-mono→is-regular-mono itself .map = record { map = id ; commutes = idr _ } - + im : Initial _ im .bot = itself im .has⊥ other = contr hom unique where @@ -214,7 +214,7 @@ the code below demonstrates. hom .α = tt hom .β = other .map hom .sq = trivial! - + unique : ∀ x → hom ≡ x unique x = ↓Hom-path _ _ refl (ext (intror refl ∙ ap map (x .sq) ∙ elimr refl)) diff --git a/src/Cat/Diagram/Image.lagda.md b/src/Cat/Diagram/Image.lagda.md index 7fa346144..7e7ad719c 100644 --- a/src/Cat/Diagram/Image.lagda.md +++ b/src/Cat/Diagram/Image.lagda.md @@ -124,10 +124,10 @@ is the image object, and $m$ is the inclusion map: ```agda Im : Ob - Im = im .bot .y .object .domain + Im = im .bot .y .fst .domain Im→codomain : Hom Im b - Im→codomain = im .bot .y .object .map + Im→codomain = im .bot .y .fst .map ``` Furthermore, this map is both an inclusion (since $M$ is a class of @@ -135,7 +135,7 @@ monomorphisms), and an $M$-inclusion at that: ```agda Im→codomain-is-M : M .fst Im→codomain - Im→codomain-is-M = im .bot .y .witness + Im→codomain-is-M = im .bot .y .snd Im→codomain-is-monic : is-monic Im→codomain Im→codomain-is-monic = M .snd Im→codomain-is-M @@ -175,7 +175,7 @@ through $k$: universal m M i p = im .has⊥ obj .centre .β .map where obj : ↓Obj _ _ obj .x = tt - obj .y = restrict (cut m) M + obj .y = cut m , M obj .map = record { map = i ; commutes = p } universal-factors diff --git a/src/Cat/Functor/Algebra.lagda.md b/src/Cat/Functor/Algebra.lagda.md index 5f1b02592..dfc3e56ab 100644 --- a/src/Cat/Functor/Algebra.lagda.md +++ b/src/Cat/Functor/Algebra.lagda.md @@ -603,7 +603,7 @@ forms a full subcategory of $\cC$. private module Free-algebras = Cat.Reasoning Free-algebras module Free-alg (α : Free-algebras.Ob) where -- Rexport stuff in a more user-friendly format - open Free-object (α .witness) public + open Free-object (α .snd) public ob : Ob ob = free .fst diff --git a/src/Cat/Functor/FullSubcategory.lagda.md b/src/Cat/Functor/FullSubcategory.lagda.md index a024ce242..cb9853a59 100644 --- a/src/Cat/Functor/FullSubcategory.lagda.md +++ b/src/Cat/Functor/FullSubcategory.lagda.md @@ -34,18 +34,9 @@ subgraphs" of the categorical world: Keep only some of the vertices (objects), but all of the arrows (arrows) between them. ```agda -record Restrict-ob (P : C.Ob → Type ℓ) : Type (o ⊔ ℓ) where - no-eta-equality - constructor restrict - field - object : C.Ob - witness : P object - -open Restrict-ob public - Restrict : (P : C.Ob → Type ℓ) → Precategory (o ⊔ ℓ) h -Restrict P .Ob = Restrict-ob P -Restrict P .Hom A B = C.Hom (A .object) (B .object) +Restrict P .Ob = Σ[ O ∈ C ] (P O) +Restrict P .Hom A B = C.Hom (A .fst) (B .fst) Restrict P .Hom-set _ _ = C.Hom-set _ _ Restrict P .id = C.id Restrict P ._∘_ = C._∘_ @@ -54,19 +45,6 @@ Restrict P .idl = C.idl Restrict P .assoc = C.assoc ``` - - A very important property of full subcategories (`Restrict`{.Agda}ions) is that _any full subcategory of a [[univalent category]] is univalent_. The argument is roughly as follows: Since $\cC$ is univalent, an @@ -85,11 +63,11 @@ $\cR$ here) and in $\cC$, which can be done by destructuring and reassembling: ```agda - sub-iso→super-iso : ∀ {A B : Restrict-ob P} → (A R.≅ B) → (A .object C.≅ B .object) + sub-iso→super-iso : ∀ {A B : Σ _ P} → (A R.≅ B) → (A .fst C.≅ B .fst) sub-iso→super-iso x = C.make-iso x.to x.from x.invl x.invr where module x = R._≅_ x - super-iso→sub-iso : ∀ {A B : Restrict-ob P} → (A .object C.≅ B .object) → (A R.≅ B) + super-iso→sub-iso : ∀ {A B : Σ _ P} → (A .fst C.≅ B .fst) → (A R.≅ B) super-iso→sub-iso y = R.make-iso y.to y.from y.invl y.invr where module y = C._≅_ y ``` @@ -108,10 +86,10 @@ is $\cR$. ```agda Restrict-is-category : is-category C → is-category (Restrict P) Restrict-is-category cids = λ where - .to-path im i .object → Univalent.iso→path cids (sub-iso→super-iso P im) i - .to-path {a = a} {b = b} im i .witness → is-prop→pathp + .to-path im i .fst → Univalent.iso→path cids (sub-iso→super-iso P im) i + .to-path {a = a} {b = b} im i .snd → is-prop→pathp (λ i → pprop (cids .to-path (sub-iso→super-iso P im) i)) - (a .witness) (b .witness) i + (a .snd) (b .snd) i .to-path-over p → R.≅-pathp _ _ λ i → cids .to-path-over (sub-iso→super-iso P p) i .C.to ``` @@ -140,7 +118,7 @@ functor from $\cD$. This functor is actually just $F$ again: ```agda Ff-domain→Full-subcat : Functor D Full-inclusion→Full-subcat - Ff-domain→Full-subcat .Functor.F₀ x = restrict (F₀ x) (inc (x , C.id-iso)) + Ff-domain→Full-subcat .Functor.F₀ x = F₀ x , inc (x , C.id-iso) Ff-domain→Full-subcat .Functor.F₁ = F₁ Ff-domain→Full-subcat .Functor.F-id = F-id Ff-domain→Full-subcat .Functor.F-∘ = F-∘ @@ -151,7 +129,7 @@ functor from $\cD$. This functor is actually just $F$ again: is-eso-domain→Full-subcat : is-eso Ff-domain→Full-subcat is-eso-domain→Full-subcat yo = ∥-∥-map (λ (preimg , isom) → preimg , super-iso→sub-iso _ isom) - (yo .witness) + (yo .snd) ``` Up to weak equivalence, admitting a full inclusion is equivalent to @@ -162,7 +140,7 @@ morphisms by the identity function. ```agda module _ {P : C.Ob → Type ℓ} where Forget-full-subcat : Functor (Restrict P) C - Forget-full-subcat .Functor.F₀ = object + Forget-full-subcat .Functor.F₀ = fst Forget-full-subcat .Functor.F₁ f = f Forget-full-subcat .Functor.F-id = refl Forget-full-subcat .Functor.F-∘ f g i = f C.∘ g diff --git a/src/Cat/Instances/Sheaves.lagda.md b/src/Cat/Instances/Sheaves.lagda.md index bf5d37e9a..6baa7e4da 100644 --- a/src/Cat/Instances/Sheaves.lagda.md +++ b/src/Cat/Instances/Sheaves.lagda.md @@ -9,6 +9,7 @@ open import Cat.Instances.Sets.Cocomplete open import Cat.Instances.Functor.Limits open import Cat.Instances.Sheaves.Limits open import Cat.Functor.Adjoint.Monadic +open import Cat.Functor.FullSubcategory open import Cat.Instances.Sets.Complete open import Cat.Diagram.Limit.Product open import Cat.Diagram.Colimit.Base diff --git a/src/Cat/Monoidal/Diagram/Monoid/Representable.lagda.md b/src/Cat/Monoidal/Diagram/Monoid/Representable.lagda.md index 83e02ddcd..acd55af48 100644 --- a/src/Cat/Monoidal/Diagram/Monoid/Representable.lagda.md +++ b/src/Cat/Monoidal/Diagram/Monoid/Representable.lagda.md @@ -257,8 +257,8 @@ homomorphism $f : M \to N$ is a natural transformation $\hom(-, M) \to ```agda Mon→RepPShMon : Functor Mon[C] RepPShMon - Mon→RepPShMon .F₀ (m , mon) .object = Mon→PshMon mon - Mon→RepPShMon .F₀ (m , mon) .witness = Mon→PshMon-rep mon + Mon→RepPShMon .F₀ (m , mon) .fst = Mon→PshMon mon + Mon→RepPShMon .F₀ (m , mon) .snd = Mon→PshMon-rep mon Mon→RepPShMon .F₁ f .η x .hom = f .hom ∘_ Mon→RepPShMon .F₁ f .η x .preserves = @@ -493,13 +493,12 @@ monoids isomorphic to the one we started with. ```agda Mon→RepPShMon-is-split-eso : is-split-eso Mon→RepPShMon - Mon→RepPShMon-is-split-eso P .fst = - P .witness .rep , RepPshMon→Mon (P .object) (P .witness) - Mon→RepPShMon-is-split-eso P .snd = super-iso→sub-iso _ $ to-natural-iso ni where + Mon→RepPShMon-is-split-eso (P , pm) .fst = pm .rep , RepPshMon→Mon P pm + Mon→RepPShMon-is-split-eso (P , pm) .snd = super-iso→sub-iso _ $ to-natural-iso ni where open make-natural-iso - open RepPshMon→Mon (P .object) (P .witness) + open RepPshMon→Mon P pm open PMon using (identity; _⋆_) - module P = Functor (P .object) + module P = Functor P ```
@@ -507,7 +506,7 @@ monoids isomorphic to the one we started with. expand this `
` element. ```agda - ni : make-natural-iso (Mon→PshMon (RepPshMon→Mon (P .object) (P .witness))) (P .object) + ni : make-natural-iso (Mon→PshMon (RepPshMon→Mon P pm)) P ni .eta x .hom = repr.from .η x ni .inv x .hom = repr.to .η x diff --git a/src/Cat/Morphism/StrongEpi.lagda.md b/src/Cat/Morphism/StrongEpi.lagda.md index fa21214f3..e5961d5a4 100644 --- a/src/Cat/Morphism/StrongEpi.lagda.md +++ b/src/Cat/Morphism/StrongEpi.lagda.md @@ -283,7 +283,7 @@ strong-epi-mono→image f a→im (_ , str-epi) im→b mono fact = go where obj : ↓Obj (Const (cut f)) (Forget-full-subcat {P = is-monic ⊙ map}) obj .x = tt - obj .y = restrict (cut im→b) mono + obj .y = cut im→b , mono obj .map = record { map = a→im ; commutes = fact } ``` @@ -300,7 +300,7 @@ in the relevant comma categories. the-lifting = str-epi - (record { monic = o.y .witness }) + (record { monic = o.y .snd }) {u = o.map .map} {v = im→b} (sym (o.map .commutes ∙ sym fact)) diff --git a/src/Cat/Site/Base.lagda.md b/src/Cat/Site/Base.lagda.md index 05cfb5d4c..c0a2696be 100644 --- a/src/Cat/Site/Base.lagda.md +++ b/src/Cat/Site/Base.lagda.md @@ -1,5 +1,8 @@