/
Sum.agda
68 lines (50 loc) · 1.79 KB
/
Sum.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
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
------------------------------------------------------------------------
-- The Agda standard library
--
-- Sums (disjoint unions)
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Sum where
open import Agda.Builtin.Equality
open import Data.Bool.Base using (true; false)
open import Data.Unit.Polymorphic.Base using (⊤; tt)
open import Data.Maybe.Base using (Maybe; just; nothing)
open import Function.Base
open import Level
open import Relation.Nullary.Reflects using (invert)
open import Relation.Nullary using (Dec; yes; no; _because_; ¬_)
private
variable
a b : Level
A B : Set a
------------------------------------------------------------------------
-- Re-export content from base module
open import Data.Sum.Base public
------------------------------------------------------------------------
-- Additional functions
module _ {a b} {A : Set a} {B : Set b} where
isInj₁ : A ⊎ B → Maybe A
isInj₁ (inj₁ x) = just x
isInj₁ (inj₂ y) = nothing
isInj₂ : A ⊎ B → Maybe B
isInj₂ (inj₁ x) = nothing
isInj₂ (inj₂ y) = just y
From-inj₁ : A ⊎ B → Set a
From-inj₁ (inj₁ _) = A
From-inj₁ (inj₂ _) = ⊤
from-inj₁ : (x : A ⊎ B) → From-inj₁ x
from-inj₁ (inj₁ x) = x
from-inj₁ (inj₂ _) = _
From-inj₂ : A ⊎ B → Set b
From-inj₂ (inj₁ _) = ⊤
From-inj₂ (inj₂ _) = B
from-inj₂ : (x : A ⊎ B) → From-inj₂ x
from-inj₂ (inj₁ _) = _
from-inj₂ (inj₂ x) = x
-- Conversion back and forth with Dec
fromDec : Dec A → A ⊎ ¬ A
fromDec ( true because [p]) = inj₁ (invert [p])
fromDec (false because [¬p]) = inj₂ (invert [¬p])
toDec : A ⊎ ¬ A → Dec A
toDec (inj₁ p) = yes p
toDec (inj₂ ¬p) = no ¬p