Category/Instance/Nat/FinitelyCocomplete.agda


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

{-# OPTIONS --without-K --safe #-}

module Category.Instance.Nat.FinitelyCocomplete where

open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
open import Categories.Category.Instance.Nat using (Nat; Nat-Cocartesian)
open import Level using (0ℓ)
open import Nat.Properties using (Coeq)

Nat-FinitelyCocomplete : FinitelyCocompleteCategory 0ℓ 0ℓ 0ℓ
Nat-FinitelyCocomplete = record
    { U = Nat
    ; finCo = record
        { cocartesian = Nat-Cocartesian
        ; coequalizer = Coeq
        }
    }