aboutsummaryrefslogtreecommitdiff
path: root/Category/Instance/Nat/FinitelyCocomplete.agda
blob: d5a9ec0838702ce09ebae4a0e0bd9a609549b754 (plain)
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
        }
    }