open import Algebra.Prelude
open import Cat.Instances.Sets.Cocomplete
open import Cat.Instances.Functor.Limits
open import Cat.Instances.StrictCat
open import Cat.Diagram.Everything
open import Cat.Functor.Everything
open import Cat.Thin
open import Data.Fin
open import Topoi.Base
import Cat.Functor.Reasoning as Func
import Cat.Reasoning as CR
import Data.Nat as Nat
module wip.exact where
Δ : Precategory lzero lzero
Δ .Precategory.Ob = Nat
Δ .Precategory.Hom j k = Σ[ f ∈ (Fin j → Fin k) ] (∀ x y → x ≤ y → f x ≤ f y)
Δ .Precategory.Hom-set j k =
Σ-is-hlevel 2 (hlevel 2)
λ f → is-prop→is-set $ Π-is-hlevel 1 λ x → Π-is-hlevel 1 λ y →
fun-is-hlevel 1 (Nat.≤-prop (to-nat (f x)) (to-nat (f y)))
Δ .Precategory.id = (λ x → x) , λ x y i → i
Δ .Precategory._∘_ (f , p) (g , p′) = (f ⊙ g) , λ x y q → p _ _ (p′ _ _ q)
Δ .Precategory.idr f = refl
Δ .Precategory.idl f = refl
Δ .Precategory.assoc f g h = refl
open Functor
[_] : Nat → Proset lzero lzero
[ n ] = make-proset {A = Fin n} {R = _≤_}
Fin-is-set
(λ {x} → Nat.≤-refl (to-nat x))
(λ {x} {y} {z} p q → Nat.≤-trans (to-nat x) (to-nat y) (to-nat z) p q)
(λ {x} {y} → Nat.≤-prop (to-nat x) (to-nat y))
incl : Functor Δ (Strict-Cat lzero lzero)
incl .F₀ n = [ n ] .Proset.underlying , [ n ] .Proset.Ob-is-set
incl .F₁ x .F₀ = x .fst
incl .F₁ x .F₁ = x .snd _ _
incl .F₁ x .F-id {n} = Nat.≤-prop (to-nat (x .fst n)) _ _ _
incl .F₁ x .F-∘ {w} {y} {z} f g = Nat.≤-prop (to-nat (x .fst w)) _ _ _
incl .F-id = Functor-path (λ _ → refl) (λ _ → refl)
incl .F-∘ f g = Functor-path (λ _ → refl) (λ _ → refl)
Simplicial-nerve : Functor (Strict-Cat lzero lzero) (PSh lzero Δ)
Simplicial-nerve = Nerve incl