Sites and sheaves (#369)

Stuff from C2.1 in the elephant

Author: plt-amy

src/1Lab/Membership.agda

@@ -16,11 +16,12 @@ module 1Lab.Membership where
 -- propositions, either. In practice, both of these conditions are
 -- satisfied.
 
-record Membership {ℓ ℓe} (A : Type ℓe) (ℙA : Type ℓ) ℓm : Type (ℓ ⊔ lsuc (ℓe ⊔ ℓm)) where
+record Membership {ℓ ℓe} (A : Type ℓe) (ℙA : Type ℓ) ℓm : Type (ℓ ⊔ ℓe ⊔ lsuc ℓm) where
   field _∈_ : A → ℙA → Type ℓm
   infix 30 _∈_
 
 open Membership ⦃ ... ⦄ using (_∈_) public
+{-# DISPLAY Membership._∈_ i a b = a ∈ b #-}
 
 -- The prototypical instance is given by functions into a universe:
 
@@ -38,17 +39,37 @@ _∉_ : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {ℙA : Type ℓ'} ⦃ m : Membershi
     → A → ℙA → Type ℓ''
 x ∉ y = ¬ (x ∈ y)
 
--- Inclusion relative to the _∈_ projection.
-
-_⊆_ : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {ℙA : Type ℓ'} ⦃ m : Membership A ℙA ℓ'' ⦄
-    → ℙA → ℙA → Type (ℓ ⊔ ℓ'')
-_⊆_ {A = A} S T = (a : A) → a ∈ S → a ∈ T
+infix 30 _∉_
 
 -- Total space of a predicate.
-
 ∫ₚ
   : ∀ {ℓ ℓ' ℓ''} {X : Type ℓ} {ℙX : Type ℓ'} ⦃ m : Membership X ℙX ℓ'' ⦄
   → ℙX → Type _
 ∫ₚ {X = X} P = Σ[ x ∈ X ] (x ∈ P)
 
-infix 30 _∉_ _⊆_
+-- Notation typeclass for _⊆_. We could always define
+--
+--   S ⊆ T = ∀ x → x ∈ S → x ∈ T
+--
+-- but this doesn't work too well for collections where the element type
+-- is more polymorphic than the collection type, e.g. sieves, where we
+-- would instead like
+--
+--  S ⊆ T = ∀ {i} (x : F i) → x ∈ S → x ∈ T
+--
+-- Instead we can define _⊆_ as its own class, then write a default
+-- instance in terms of _∈_.
+
+record Inclusion {ℓ} (ℙA : Type ℓ) ℓi : Type (ℓ ⊔ lsuc (ℓi)) where
+  field _⊆_ : ℙA → ℙA → Type ℓi
+  infix 30 _⊆_
+
+open Inclusion ⦃ ... ⦄ using (_⊆_) public
+{-# DISPLAY Inclusion._⊆_ i a b = a ⊆ b #-}
+
+instance
+  Inclusion-default
+    : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {ℙA : Type ℓ'} ⦃ m : Membership A ℙA ℓ'' ⦄
+    → Inclusion ℙA (ℓ ⊔ ℓ'')
+  Inclusion-default {A = A} = record { _⊆_ = λ S T → (a : A) → a ∈ S → a ∈ T }
+  {-# INCOHERENT Inclusion-default #-}

src/1Lab/Path.lagda.md

@@ -1100,21 +1100,6 @@ J-refl {x = x} P prefl i = transport-filler (λ i → P _ (λ j → x)) prefl (~
 ```agda
 inspect : ∀ {a} {A : Type a} (x : A) → Singleton x
 inspect x = x , refl
-
-record Recall
-  {a b} {A : Type a} {B : A → Type b}
-  (f : (x : A) → B x) (x : A) (y : B x)
-  : Type (a ⊔ b)
-  where
-    constructor ⟪_⟫
-    field
-      eq : f x ≡ y
-
-recall
-  : ∀ {a b} {A : Type a} {B : A → Type b}
-  → (f : (x : A) → B x) (x : A)
-  → Recall f x (f x)
-recall f x = ⟪ refl ⟫
 ```
 -->
 

src/1Lab/Prelude.agda

@@ -13,6 +13,7 @@ open import 1Lab.Path.Groupoid public
 open import 1Lab.Path.IdentitySystem public
 open import 1Lab.Path.IdentitySystem.Interface public
 
+open import Meta.Brackets public
 open import Meta.Append public
 open import Meta.Idiom public
 open import Meta.Bind public

src/Algebra/Ring/Solver.agda

@@ -175,11 +175,16 @@ module Impl {ℓ} {R : Type ℓ} (cring : CRing-on R) where
   sem [+] = R._+_
   sem [*] = R._*_
 
-  ⟦_⟧ : ∀ {n} → Polynomial n → Vec R n → R
-  ⟦ op o p₁ p₂ ⟧ ρ = sem o (⟦ p₁ ⟧ ρ) (⟦ p₂ ⟧ ρ)
-  ⟦ con c      ⟧ ρ = embed-coe (lift c)
-  ⟦ var x      ⟧ ρ = lookup ρ x
-  ⟦ :- p       ⟧ ρ = R.- ⟦ p ⟧ ρ
+  eval : ∀ {n} → Polynomial n → Vec R n → R
+
+  instance
+    ⟦⟧-Polynomial : ∀ {n} → ⟦⟧-notation (Polynomial n)
+    ⟦⟧-Polynomial = brackets _ eval
+
+  eval (op o p₁ p₂) ρ = sem o (⟦ p₁ ⟧ ρ) (⟦ p₂ ⟧ ρ)
+  eval (con c)      ρ = embed-coe (lift c)
+  eval (var x)      ρ = lookup ρ x
+  eval (:- p)       ρ = R.- ⟦ p ⟧ ρ
 
   ---
 

src/Cat/Base.lagda.md

@@ -592,5 +592,12 @@ instance
     sa .idsᵉ .to-path (x i)
   Extensional-natural-transformation {D = D} ⦃ sa ⦄ .idsᵉ .to-path-over h =
     is-prop→pathp (λ i → Π-is-hlevel 1 λ _ → Pathᵉ-is-hlevel 1 sa (hlevel 2)) _ _
+
+_⟪_⟫_
+  : ∀ {o ℓ o' ℓ'} {C : Precategory o ℓ} {D : Precategory o' ℓ'}
+  → (F : Functor C D) {U V : ⌞ C ⌟}
+  → C .Precategory.Hom U V
+  → D .Precategory.Hom (F # U) (F # V)
+_⟪_⟫_ F f = Functor.F₁ F f
 ```
 -->

src/Cat/CartesianClosed/Instances/PSh.agda

@@ -176,30 +176,32 @@ module _ {κ} {C : Precategory κ κ} where
     module C = Cat.Reasoning C
     module PSh = Cat.Reasoning (PSh κ C)
 
+  open Binary-products (PSh κ C) (PSh-products {C = C})
+
+  PSh[_,_] : PSh.Ob → PSh.Ob → PSh.Ob
+  PSh[ A , B ] = F module psh-exp where
+    module A = Functor A
+    module B = Functor B
+
+    F : PSh.Ob
+    F .F₀ c = el ((よ₀ C c ⊗₀ A) => B) Nat-is-set
+    F .F₁ f nt .η i (g , x) = nt .η i (f C.∘ g , x)
+    F .F₁ f nt .is-natural x y g = funext λ o →
+      ap (nt .η y) (Σ-pathp (C.assoc _ _ _) refl) ∙ happly (nt .is-natural _ _ _) _
+    F .F-id = ext λ f i g x →
+      ap (f .η i) (Σ-pathp (C.idl _) refl)
+    F .F-∘ f g = ext λ h i j x →
+      ap (h .η i) (Σ-pathp (sym (C.assoc _ _ _)) refl)
+
+  {-# DISPLAY psh-exp.F A B = PSh[ A , B ] #-}
+
   PSh-closed : Cartesian-closed (PSh κ C) (PSh-products {C = C}) (PSh-terminal {C = C})
   PSh-closed = cc where
     cat = PSh κ C
 
-    open Binary-products cat (PSh-products {C = C}) public
-
     module _ (A : PSh.Ob) where
-      module A = Functor A
-
-      hom₀ : PSh.Ob → PSh.Ob
-      hom₀ B = F where
-        module B = Functor B
-        F : PSh.Ob
-        F .F₀ c = el ((よ₀ C c ⊗₀ A) => B) Nat-is-set
-        F .F₁ f nt .η i (g , x) = nt .η i (f C.∘ g , x)
-        F .F₁ f nt .is-natural x y g = funext λ o →
-          ap (nt .η y) (Σ-pathp (C.assoc _ _ _) refl) ∙ happly (nt .is-natural _ _ _) _
-        F .F-id = ext λ f i g x →
-          ap (f .η i) (Σ-pathp (C.idl _) refl)
-        F .F-∘ f g = ext λ h i j x →
-          ap (h .η i) (Σ-pathp (sym (C.assoc _ _ _)) refl)
-
       func : Functor (PSh κ C) (PSh κ C)
-      func .F₀ = hom₀
+      func .F₀ = PSh[ A ,_]
       func .F₁ f .η i g .η j (h , x) = f .η _ (g .η _ (h , x))
       func .F₁ f .η i g .is-natural x y h = funext λ x →
         ap (f .η _) (happly (g .is-natural _ _ _) _) ∙ happly (f .is-natural _ _ _) _

src/Cat/Diagram/Colimit/Base.lagda.md

@@ -646,7 +646,7 @@ is-cocontinuous oshape hshape {C = C} F =
   → preserves-colimit F Diagram
 ```
 
-# Cocompleteness
+# Cocompleteness {defines="cocomplete-category"}
 
 A category is **cocomplete** if it admits colimits for diagrams of arbitrary shape.
 However, in the presence of excluded middle, if a category admits

src/Cat/Diagram/Colimit/Cocone.lagda.md

@@ -22,7 +22,7 @@ open _=>_
 ```
 -->
 
-# Colimits via cocones
+# Colimits via cocones {defines="cocone"}
 
 As noted in the main page on [[colimits]], most introductory texts opt
 to define colimits via categorical gadgets called **cocones**. A

src/Cat/Diagram/Monad/Limits.lagda.md

@@ -31,7 +31,7 @@ open Algebra-on
 ```
 -->
 
-# Limits in categories of algebras
+# Limits in categories of algebras {defines="limits-in-categories-of-algebras"}
 
 Suppose that $\cC$ be a category, $M$ be a [monad] on $\cC$, and
 $F$ be a $\cJ$-shaped diagram of [$M$-algebras][malg] (that is, a