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
|
{-# language BlockArguments #-}
{-# language DefaultSignatures #-}
{-# language DerivingStrategies #-}
{-# language EmptyCase #-}
{-# language ExplicitNamespaces #-}
{-# language ImportQualifiedPost #-}
{-# language FlexibleContexts #-}
{-# language FlexibleInstances #-}
{-# language FunctionalDependencies #-}
{-# language GADTs #-}
{-# language LambdaCase #-}
{-# language LinearTypes #-}
{-# language NoStarIsType #-}
{-# language PolyKinds #-}
{-# language QuantifiedConstraints #-}
{-# language RankNTypes #-}
{-# language RoleAnnotations #-}
{-# language ScopedTypeVariables #-}
{-# language StandaloneDeriving #-}
{-# language StandaloneKindSignatures #-}
{-# language StrictData #-}
{-# language TupleSections #-}
{-# language TypeApplications #-}
{-# language TypeFamilies #-}
{-# language TypeFamilyDependencies #-}
{-# language TypeOperators #-}
{-# language UndecidableInstances #-}
{-# language UndecidableSuperClasses #-}
module T19627 where
import Data.Kind
import Prelude hiding ( Functor(..) )
--------------------
class (Prop (Not p), Not (Not p) ~ p) => Prop (p :: Type) where
type Not p :: Type
(!=) :: p -> Not p -> r
data Y (a :: Type) (b :: Type) (c :: Type) where
L :: Y a b a
R :: Y a b b
newtype a & b = With (forall c. Y a b c -> c)
with :: (forall c. Y a b c -> c) -> a & b
with = With
runWith :: a & b -> Y a b c -> c
runWith (With f) = f
withL' :: a & b -> a
withL' (With f) = f L
withR' :: a & b -> b
withR' (With f) = f R
instance (Prop a, Prop b) => Prop (a & b) where
type Not (a & b) = Not a `Either` Not b
w != Left a = withL' w != a
w != Right b = withR' w != b
instance (Prop a, Prop b) => Prop (Either a b) where
type Not (Either a b) = Not a & Not b
Left a != w = a != withL' w
Right a != w = a != withR' w
newtype Yoneda f a = Yoneda
(forall r. Prop r => (a -> r) -> f r)
data Noneda f a where
Noneda :: Prop r => !(f r <#- (a ⊸ r)) -> Noneda f a
liftYoneda :: forall f a i. (Functor f, Prop a, Iso i) => i (f a) (Yoneda f a)
liftYoneda = iso \case
L -> lowerYoneda'
R -> lol \case
L -> \(Noneda ((a2r :: a ⊸ r) :-#> nfr)) -> runLol (fmap @f @a @r a2r) L nfr
R -> \fa -> Yoneda do
lol \case
R -> \f -> fmap' f fa
L -> \nfr -> whyNot \a2r -> fmap a2r fa != nfr
type family NotApart (p :: Type -> Type -> Type) :: Type -> Type -> Type
class
( forall a b. (Prop a, Prop b) => Prop (p a b)
, NotApart (NotIso p) ~ p
) => Iso p where
type NotIso p = (q :: Type -> Type -> Type) | q -> p
iso :: (forall c. Y (b ⊸ a) (a ⊸ b) c -> c) -> p a b
data b <#- a where (:-#>) :: a -> Not b -> b <#- a
newtype a ⊸ b = Lol (forall c. Y (Not b %1 -> Not a) (a %1 -> b) c -> c)
class
( forall a. Prop a => Prop (f a)
) => Functor f where
fmap' :: (Prop a, Prop b, Lol l, Lol l') => l ((a ⊸ b)) (l' (f a) (f b))
fmap :: forall f a b l. (Functor f, Prop a, Prop b, Lol l) => (a ⊸ b) -> l (f a) (f b)
fmap f = fmap' f
class Iso p => Lol (p :: Type -> Type -> Type) where
lol :: (forall c. Y (Not b -> Not a) (a -> b) c -> c) -> p a b
apartR :: Not (p a b) -> b <#- a
|
