Created
December 21, 2018 14:19
-
-
Save SimonForest/d8fb4e109bb437dd0a5af19f968089ae to your computer and use it in GitHub Desktop.
A bug in Agda ?
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
record MyS | |
(State : Set) | |
(Operation : (f g : State) → Set) | |
(Change : {f g : State} (O : Operation f g) → Set) | |
: | |
Set | |
where | |
data Left-state : Set where | |
Left-notdone : Left-state | |
Left-done : Left-state | |
data Right-state : Set where | |
Right-notdone : Right-state | |
Right-done : Right-state | |
data State : Set where | |
State-both : Left-state → Right-state → State | |
data Left : Left-state → Left-state → Set where | |
Left-id : (a : Left-state) → Left a a | |
Left-step : Left Left-notdone Left-done | |
data Right : Right-state → Right-state → Set where | |
Right-id : (a : Right-state) → Right a a | |
Right-step : Right Right-notdone Right-done | |
data Operation : (a b : State) → Set where | |
Operation-both : {a b : Left-state} {c d : Right-state} (A : Left a b) (C : Right c d) → Operation (State-both a c) (State-both b d) | |
data Change : {a b : State} (O : Operation a b) → Set where | |
Change-id : {a b : State} (O : Operation a b) → Change O | |
comp : {f f' f'' : State} (F : Operation f f') (G : Operation f' f'') → Operation f f'' | |
comp' : {f f' f'' : State} {F : Operation f f'} {G : Operation f' f''} (φ : Change F) (ψ : Change G) → Change (comp F G) | |
comp (Operation-both (Left-id a) (Right-id d)) (Operation-both B D) = Operation-both B D | |
comp (Operation-both (Left-id a) (Right-step)) (Operation-both B (Right-id .Right-done)) = Operation-both B (Right-step) | |
comp (Operation-both (Left-step) (Right-id a)) (Operation-both (Left-id .Left-done) D) = Operation-both (Left-step) D | |
comp (Operation-both (Left-step) (Right-step)) (Operation-both (Left-id .Left-done) (Right-id .Right-done)) = Operation-both (Left-step) (Right-step) | |
comp' (Change-id (Operation-both (Left-step) (Right-id a))) (Change-id (Operation-both (Left-id .Left-done) D)) = Change-id (Operation-both (Left-step) D) | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment