-
Notifications
You must be signed in to change notification settings - Fork 3
/
Sg.agda
40 lines (30 loc) · 900 Bytes
/
Sg.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
module LibAgda.Sg where
open import Agda.Primitive
open import LibAgda.Two
open import LibAgda.Comb
record Sg {k l}(S : Set k)(T : S -> Set l) : Set (k ⊔ l) where
constructor _,_
field
fst : S
snd : T fst
open Sg public
_*_ : forall {k l} -> Set k -> Set l -> Set (k ⊔ l)
S * T = Sg S \ _ -> T
infixr 5 _,_ _*_
sg : forall {k k' l l'}{S : Set k}{S' : Set k'}
{T : S -> Set l}{T' : S' -> Set l'}
(f : S -> S')(g : forall {s} -> T s -> T' (f s)) ->
Sg S T -> Sg S' T'
sg f g (s , t) = f s , g t
_+_ : forall {l} -> Set l -> Set l -> Set l
S + T = Sg Two (S <?> T)
infixr 4 _+_
_<+>_ : forall {k l}{S T : Set k}{S' T' : Set l} ->
(S -> S') -> (T -> T') -> (S + T) -> (S' + T')
(f <+> g) = sg id \ { {tt} -> f ; {ff} -> g }
record %_ {I : Set}(T : I -> Set) : Set where
constructor %[_]
field
{wit} : I
see : T wit
infixl 0 %_