GV20 assurance

GV20 is statically satisfied because ProjectId has exactly one inhabitant and the canonical project value is that inhabitant.

{-# OPTIONS --safe #-}

module Govenv.Assurance.GV20 where

open import Agda.Builtin.Equality using (_≡_; refl)
open import Govenv.Kernel.Assurance using (StaticEvidence; staticEvidence)
open import Govenv.Project using (ProjectId; govenv; project)

onlyGovenv : (identity : ProjectId) → identity ≡ govenv
onlyGovenv govenv = refl

record Proposition : Set where
  constructor satisfied
  field
    canonical : project ≡ govenv
    unique : (identity : ProjectId) → identity ≡ govenv

proposition : Set
proposition = Proposition

evidence : StaticEvidence 20
evidence = staticEvidence proposition (satisfied refl onlyGovenv)