quantitative-poly/Isomorphisms.idr at main · g-nakov/quantitative-poly · GitHub

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
module Isomorphisms

import Linear.Types
import FunExt

-- Isomorphisms in the category of types and linear functions
record Iso a b where
  constructor MkIso
  to : a -<> b
  from : b -<> a
  0 toFrom : (0 y : b) -> to (from y) = y
  0 fromTo : (0 x : a) -> from (to x) = x

-- Identity isomorphism
idIso : Iso a a
idIso = MkIso (\ x => x) (\ x => x) (\ x => Refl) (\ x => Refl)

-- Composition of isomorphisms
transIso : Iso a b -> Iso b c -> Iso a c
transIso f g = MkIso (\ x => to g (to f x))
                     (\ x => from f (from g x))
                     (\ x => rewrite toFrom f (from g x) in toFrom g x)
                     (\ x => rewrite fromTo g (to f x) in fromTo f x)

-- "Dependent pairs are left adjoint to dependent functions" -- true
-- for arbitrary resource annotation ρ, but can only be stated for ρ =
-- 0, 1, ω^< in Idris 2. Here we state it for the most interesting
-- case ρ = ω^<.
curryuncurry : {c : Sigma1 a b -> Type} ->
               Iso ((1 xy : Sigma1 a b) -> c xy) ((1 x : a) -> (1 y : b x) -> c (x # y))
curryuncurry = MkIso (\ f => \ x => \ y => f (x # y))
                     (\ g => \ (x # y) => g x y)
                     (\ f => Refl)
                     (\ g => funext (\ (x # y) => Refl))

pairUnitL : Iso (Sigma1 I b) (b Star)
pairUnitL = MkIso (\ (Star # a) => a)
                  (\ a => Star # a)
                  (\ x => Refl)
                  (\ (Star # a) => Refl)

data Box : Type -> Type where
  Unrestricted : a -> Box x

{-
-- The rules for Top refer to arbitrary contexts, so they
-- cannot be formulated inside Idris 2 itself.

zeroInitial : Iso (Void -<> a) Top
zeroInitial = MkIso (\ f => Star)
                    (\ x => \ y => void1 y)
                    (\ x => ?Refl)
                    (\ x => funext (\ y => void1 y))
-}

trivArgument : Iso (I -<> a) a
trivArgument = MkIso (\ f => f Star)
                     (\ a => \ Star => a)
                     (\ a => Refl)
                     (\ f => funext (\ Star => Refl))

-- With our encoding of With a a, this is almost a tautology
twoArgument : Iso (Bool -<> a) (With a a)
twoArgument = MkIso (\ f => \ b => if b then f True else f False)
                    (\ aa => \ b => if b then aa True else aa False)
                    (\ f => funext (\ b => if b then Refl else Refl))
                    (\ aa => funext (\ b => if b then Refl else Refl))