clayrat

(* The basic theory of Lawvere-Tierney operators and sheafification in logical form.

   This formalization is based on:

   Barbara Veit: A proof of the associated sheaf theorem by means of categorical logic,
   The Journal of Symbolic Logic , Volume 46 , Issue 1 , March 1981 , pp. 45–55
   DOI: https://doi.org/10.2307/2273255
*)

Require Import Utf8.

clayrat

module GOI where

open import Prelude
open import Data.Nat
open import Data.List renaming (_++_ to _++ₗ_)
open import Data.List.Correspondences.Binary.Prefix
open import Data.Fin.Inductive
open import Data.Vec.Inductive
open import Data.Vec.Inductive.Operations as Vec
open import Data.Star

clayrat

-- adapted from https://gist.github.com/oisdk/037862acb385f30257a1c594fd5a616e

module ModArith where

open import Prelude

open import Data.Empty
open import Data.Nat
open import Data.Bool
open import Data.Reflects as Reflects

clayrat

{-# OPTIONS --safe #-}
module Test where

open import Prelude
open import Data.Unit
open import Data.Nat
open import Data.List

private variable
  ℓᵃ ℓᵇ : Level

clayrat

{-# OPTIONS --safe #-}
module Cograph where

open import Prelude

record Graph {A B : 𝒰} (f : A → B) : 𝒰 where
  field
    x : A
    y : B
    sub : f x ＝ y

clayrat

open import Prelude
open import Data.Empty
open import Data.Bool renaming (elim to elimᵇ ; rec to recᵇ)
open import Data.Maybe
open import Data.List
open import Data.List.Operations.Discrete
open import Data.List.Correspondences.Unary.All
open import Data.List.Correspondences.Unary.Has
open import Data.List.Correspondences.Unary.Related
open import Data.List.Correspondences.Binary.Perm

clayrat

module Div3DFA where

open import Prelude
open import Data.Bool
open import Data.Nat
open import Data.Nat.Order.Base
open import Data.Nat.DivMod
open import Data.Nat.DivMod.Base
open import Data.List
open import Data.Reflects

clayrat

{-# OPTIONS --safe #-}
module Order.SupLattice.Powerset where

open import Categories.Prelude
open import Meta.Prelude
open import Foundations.Equiv.Size

open import Data.Empty
open import Data.Unit
open import Data.Sum

clayrat

module DepPrism where

open import Prelude

open import Data.Empty
open import Data.Sum

private variable
  ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level
  X : 𝒰 ℓ₁

clayrat

{-# OPTIONS --safe --backtracking-instance-search #-}
module Bag where

open import Prelude
open import Data.Nat.Base
open import Data.Fin.Computational.Base
open import Data.Fin.Computational.Instances.Finite
open import Structures.FinSet
open import Bij