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
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
|
module Encoded.Pair
import Control.Function.FunExt
import Encoded.Bool
import Encoded.Union
import Term.Semantics
import Term.Syntax
-- Type ------------------------------------------------------------------------
export
(*) : Ty -> Ty -> Ty
ty1 * ty2 = B ~> (ty1 <+> ty2)
-- Universal Properties --------------------------------------------------------
export
pair : {ty1, ty2 : Ty} -> Term (ty1 ~> ty2 ~> (ty1 * ty2)) ctx
pair = Abs $ Abs $ Abs $
let t = Var (There $ There Here) in
let u = Var (There Here) in
let b = Var Here in
App if' [<b, App inL [<t], App inR [<u]]
export
fst : {ty1, ty2 : Ty} -> Term ((ty1 * ty2) ~> ty1) ctx
fst = Abs $ App (prL . Var Here) [<True]
export
snd : {ty1, ty2 : Ty} -> Term ((ty1 * ty2) ~> ty2) ctx
snd = Abs $ App (prR . Var Here) [<False]
-- Utilities -------------------------------------------------------------------
export
bimap :
{ty1, ty1', ty2, ty2' : Ty} ->
Term ((ty1 ~> ty1') ~> (ty2 ~> ty2') ~> ty1 * ty2 ~> ty1' * ty2') ctx
bimap = Abs $ Abs $ Abs $ Abs $
let f = Var (There $ There $ There Here) in
let g = Var (There $ There Here) in
let x = Var (There $ Here) in
let b = Var Here in
App if'
[<b
, App (inL . f . prL . x) [<True]
, App (inR . g . prR . x) [<False]
]
export
mapSnd : {ty1, ty2, ty2' : Ty} -> Term ((ty2 ~> ty2') ~> ty1 * ty2 ~> ty1 * ty2') ctx
mapSnd = Abs $ Abs $
let f = Var (There Here) in
let x = Var Here in
App pair [<App fst [<x], App (f . snd) [<x]]
export
uncurry : {ty1, ty2, ty : Ty} -> Term ((ty1 ~> ty2 ~> ty) ~> ty1 * ty2 ~> ty) ctx
uncurry = Abs $ Abs $
let f = Var $ There Here in
let p = Var Here in
App f [<App fst [<p], App snd [<p]]
-- Semantics -------------------------------------------------------------------
-- Conversion to Idris
export
toPair : {ty1, ty2 : Ty} -> TypeOf (ty1 * ty2) -> (TypeOf ty1, TypeOf ty2)
toPair f = (prL (f True), prR (f False))
export
fromPair : {ty1, ty2 : Ty} -> (TypeOf ty1, TypeOf ty2) -> TypeOf (ty1 * ty2)
fromPair (x, y) b = if' b (inL x) (inR y)
export
toFromId :
FunExt =>
{ty1, ty2 : Ty} ->
(p : (TypeOf ty1, TypeOf ty2)) ->
toPair {ty1, ty2} (fromPair {ty1, ty2} p) = p
toFromId (x, y) = cong2 (,) (retractL {ty1, ty2} x) (retractR {ty1, ty2} y)
-- Redefinition in Idris
namespace Sem
public export
pair : {ty1, ty2 : Ty} -> TypeOf ty1 -> TypeOf ty2 -> TypeOf (ty1 * ty2)
pair x y b = if' b (inL x) (inR y)
public export
fst : {ty1, ty2 : Ty} -> TypeOf (ty1 * ty2) -> TypeOf ty1
fst f = prL (f True)
public export
snd : {ty1, ty2 : Ty} -> TypeOf (ty1 * ty2) -> TypeOf ty2
snd f = prR (f False)
-- Proofs
export
pairHomo :
FunExt =>
{ty1, ty2 : Ty} ->
(0 x : TypeOf ty1) ->
(0 y : TypeOf ty2) ->
toPair {ty1, ty2} (pair {ty1, ty2} x y) = (x, y)
pairHomo x y = irrelevantEq $ toFromId (x, y)
export
fstHomo :
FunExt =>
{ty1, ty2 : Ty} ->
(0 p : (TypeOf ty1, TypeOf ty2)) ->
fst {ty1, ty2} (fromPair {ty1, ty2} p) = fst p
fstHomo (x, y) = cong fst (pairHomo x y)
export
sndHomo :
FunExt =>
{ty1, ty2 : Ty} ->
(0 p : (TypeOf ty1, TypeOf ty2)) ->
snd {ty1, ty2} (fromPair {ty1, ty2} p) = snd p
sndHomo (x, y) = cong snd (pairHomo x y)
|
