src/Cfe/Language/Construct/Single.agda


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28

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

open import Function
open import Relation.Binary
import Relation.Binary.PropositionalEquality as ≡

module Cfe.Language.Construct.Single
  {c ℓ} (over : Setoid c ℓ)
  where

open Setoid over renaming (Carrier to C)

open import Cfe.Language over hiding (_≈_)
open import Data.List
open import Data.Product as Product
open import Data.Unit
open import Level

｛_｝ : C → Language (c ⊔ ℓ) 0ℓ
｛ c ｝ = record
  { Carrier = λ l → ∃[ a ] (l ≡.≡ [ a ] × a ≈ c)
  ; _≈_ = λ _ _ → ⊤
  ; isEquivalence = record
    { refl = tt
    ; sym = λ _ → tt
    ; trans = λ _ _ → tt
    }
  }