← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to examples/outdated-and-incorrect/AIM6/Cat/lib/Logic/ChainReasoning.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
examples/outdated-and-incorrect/AIM6/Cat/lib/Logic/ChainReasoning.agda
1
 
 
2
 
module Logic.ChainReasoning where
3
 
 
4
 
module Mono where
5
 
 
6
 
  module Homogenous
7
 
    { A : Set }
8
 
    ( _==_ : A -> A -> Set )
9
 
    (refl  : (x : A) -> x == x)
10
 
    (trans : (x y z : A) -> x == y -> y == z -> x == z)
11
 
    where
12
 
 
13
 
    infix 2 chain>_
14
 
    infixl 2 _===_
15
 
    infix 3 _by_
16
 
 
17
 
    chain>_ : (x : A) -> x == x
18
 
    chain> x = refl _
19
 
 
20
 
    _===_ : {x y z : A} -> x == y -> y == z -> x == z
21
 
    xy === yz = trans _ _ _ xy yz
22
 
 
23
 
    _by_ : {x : A}(y : A) -> x == y -> x == y
24
 
    y by eq = eq
25
 
 
26
 
module Poly where
27
 
 
28
 
  module Homogenous
29
 
    ( _==_ : {A : Set} -> A -> A -> Set )
30
 
    (refl  : {A : Set}(x : A) -> x == x)
31
 
    (trans : {A : Set}(x y z : A) -> x == y -> y == z -> x == z)
32
 
    where
33
 
 
34
 
    infix 2 chain>_
35
 
    infixl 2 _===_
36
 
    infix 3 _by_
37
 
 
38
 
    chain>_ : {A : Set}(x : A) -> x == x
39
 
    chain> x = refl _
40
 
 
41
 
    _===_ : {A : Set}{x y z : A} -> x == y -> y == z -> x == z
42
 
    xy === yz = trans _ _ _ xy yz
43
 
 
44
 
    _by_ : {A : Set}{x : A}(y : A) -> x == y -> x == y
45
 
    y by eq = eq
46
 
 
47
 
  module Heterogenous
48
 
    ( _==_ : {A B : Set} -> A -> B -> Set )
49
 
    (refl  : {A : Set}(x : A) -> x == x)
50
 
    (trans : {A B C : Set}(x : A)(y : B)(z : C) -> x == y -> y == z -> x == z)
51
 
    where
52
 
 
53
 
    infix 2 chain>_
54
 
    infixl 2 _===_
55
 
    infix 3 _by_
56
 
 
57
 
    chain>_ : {A : Set}(x : A) -> x == x
58
 
    chain> x = refl _
59
 
 
60
 
    _===_ : {A B C : Set}{x : A}{y : B}{z : C} -> x == y -> y == z -> x == z
61
 
    xy === yz = trans _ _ _ xy yz
62
 
 
63
 
    _by_ : {A B : Set}{x : A}(y : B) -> x == y -> x == y
64
 
    y by eq = eq
65
 
 
66
 
  module Heterogenous1
67
 
    ( _==_ : {A B : Set1} -> A -> B -> Set1 )
68
 
    (refl  : {A : Set1}(x : A) -> x == x)
69
 
    (trans : {A B C : Set1}(x : A)(y : B)(z : C) -> x == y -> y == z -> x == z)
70
 
    where
71
 
 
72
 
    infix 2 chain>_
73
 
    infixl 2 _===_
74
 
    infix 3 _by_
75
 
 
76
 
    chain>_ : {A : Set1}(x : A) -> x == x
77
 
    chain> x = refl _
78
 
 
79
 
    _===_ : {A B C : Set1}{x : A}{y : B}{z : C} -> x == y -> y == z -> x == z
80
 
    xy === yz = trans _ _ _ xy yz
81
 
 
82
 
    _by_ : {A B : Set1}{x : A}(y : B) -> x == y -> x == y
83
 
    y by eq = eq
84