|
1124
|
1 {-# OPTIONS --cubical-compatible --safe #-}
|
|
153
|
2 module list-nat0 where
|
|
|
3
|
|
|
4 open import Level
|
|
|
5
|
|
1124
|
6 data i3 : Set where
|
|
|
7 a : i3
|
|
|
8 b : i3
|
|
|
9 c : i3
|
|
153
|
10
|
|
|
11
|
|
|
12 infixr 40 _::_
|
|
300
|
13 data List {a} (A : Set a) : Set a where
|
|
153
|
14 [] : List A
|
|
300
|
15 _::_ : A → List A → List A
|
|
153
|
16
|
|
|
17
|
|
|
18 infixl 30 _++_
|
|
300
|
19 -- _++_ : {a : Level } → {A : Set a} → List A → List A → List A
|
|
|
20 _++_ : ∀ {a} {A : Set a} → List A → List A → List A
|
|
153
|
21 [] ++ ys = ys
|
|
|
22 (x :: xs) ++ ys = x :: (xs ++ ys)
|
|
|
23
|
|
|
24
|
|
|
25 l1 = a :: []
|
|
|
26 l2 = a :: b :: a :: c :: []
|
|
|
27
|
|
|
28 l3 = l1 ++ l2
|
|
|
29
|
|
|
30 infixr 20 _==_
|
|
|
31
|
|
300
|
32 data _==_ {n} {A : Set n} : List A → List A → Set n where
|
|
|
33 reflection : {x : List A} → x == x
|
|
|
34 eq-cons : {x y : List A} { a : A } → x == y → ( a :: x ) == ( a :: y )
|
|
|
35 trans-list : {x y z : List A} { a : A } → x == y → y == z → x == z
|
|
153
|
36 -- eq-nil : [] == []
|
|
|
37
|
|
300
|
38 list-id-l : { A : Set } → { x : List A} → [] ++ x == x
|
|
153
|
39 list-id-l = reflection
|
|
|
40
|
|
300
|
41 list-id-r : { A : Set } → ( x : List A ) → x ++ [] == x
|
|
153
|
42 list-id-r [] = reflection
|
|
|
43 list-id-r (x :: xs) = eq-cons ( list-id-r xs )
|
|
|
44
|
|
|
45
|
|
300
|
46 -- listAssoc : { A : Set } → { a b c : List A} → ( ( a ++ b ) ++ c ) == ( a ++ ( b ++ c ) )
|
|
153
|
47 -- listAssoc = eq-reflection
|
|
|
48
|
|
300
|
49 list-assoc : {A : Set } → ( xs ys zs : List A ) →
|
|
153
|
50 ( ( xs ++ ys ) ++ zs ) == ( xs ++ ( ys ++ zs ) )
|
|
|
51 list-assoc [] ys zs = reflection
|
|
|
52 list-assoc (x :: xs) ys zs = eq-cons ( list-assoc xs ys zs )
|
|
|
53
|
|
|
54
|
|
|
55
|
|
|
56 open import Relation.Binary.PropositionalEquality
|
|
|
57 open ≡-Reasoning
|
|
|
58
|
|
300
|
59 cong1 : ∀{a} {A : Set a } {b} { B : Set b } →
|
|
|
60 ( f : A → B ) → {x : A } → {y : A} → x ≡ y → f x ≡ f y
|
|
153
|
61 cong1 f refl = refl
|
|
|
62
|
|
1124
|
63 -- lemma11 : ∀{n} → ( Set n ) IsRelatedTo ( Set n )
|
|
|
64 -- lemma11 = relTo refl
|
|
153
|
65
|
|
300
|
66 lemma12 : {L : Set} ( x : List L ) → x ++ x ≡ x ++ x
|
|
153
|
67 lemma12 x = begin x ++ x ∎
|
|
|
68
|
|
|
69
|
|
300
|
70 ++-assoc : {L : Set} ( xs ys zs : List L ) → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
|
|
|
71 ++-assoc [] ys zs = -- {A : Set} → -- let open ==-Reasoning A in
|
|
153
|
72 begin -- to prove ([] ++ ys) ++ zs ≡ [] ++ (ys ++ zs)
|
|
|
73 ( [] ++ ys ) ++ zs
|
|
|
74 ≡⟨ refl ⟩
|
|
|
75 ys ++ zs
|
|
|
76 ≡⟨ refl ⟩
|
|
|
77 [] ++ ( ys ++ zs )
|
|
|
78 ∎
|
|
|
79
|
|
300
|
80 ++-assoc (x :: xs) ys zs = -- {A : Set} → -- let open ==-Reasoning A in
|
|
153
|
81 begin -- to prove ((x :: xs) ++ ys) ++ zs ≡ (x :: xs) ++ (ys ++ zs)
|
|
|
82 ((x :: xs) ++ ys) ++ zs
|
|
|
83 ≡⟨ refl ⟩
|
|
|
84 (x :: (xs ++ ys)) ++ zs
|
|
|
85 ≡⟨ refl ⟩
|
|
|
86 x :: ((xs ++ ys) ++ zs)
|
|
|
87 ≡⟨ cong1 (_::_ x) (++-assoc xs ys zs) ⟩
|
|
|
88 x :: (xs ++ (ys ++ zs))
|
|
|
89 ≡⟨ refl ⟩
|
|
|
90 (x :: xs) ++ (ys ++ zs)
|
|
|
91 ∎
|
|
|
92
|
|
|
93
|
|
|
94
|
|
|
95
|
|
|
96
|
|
|
97 --data Bool : Set where
|
|
|
98 -- true : Bool
|
|
|
99 -- false : Bool
|
|
|
100
|
|
|
101
|
|
|
102 --postulate Obj : Set
|
|
|
103
|
|
300
|
104 --postulate Hom : Obj → Obj → Set
|
|
153
|
105
|
|
|
106
|
|
300
|
107 --postulate id : { a : Obj } → Hom a a
|
|
153
|
108
|
|
|
109
|
|
|
110 --infixr 80 _○_
|
|
300
|
111 --postulate _○_ : { a b c : Obj } → Hom b c → Hom a b → Hom a c
|
|
153
|
112
|
|
300
|
113 -- postulate axId1 : {a b : Obj} → ( f : Hom a b ) → f == id ○ f
|
|
|
114 -- postulate axId2 : {a b : Obj} → ( f : Hom a b ) → f == f ○ id
|
|
153
|
115
|
|
300
|
116 --assoc : { a b c d : Obj } →
|
|
|
117 -- (f : Hom c d ) → (g : Hom b c) → (h : Hom a b) →
|
|
153
|
118 -- (f ○ g) ○ h == f ○ ( g ○ h)
|
|
|
119
|
|
|
120
|
|
|
121 --a = Set
|
|
|
122
|
|
300
|
123 -- ListObj : {A : Set} → List A
|
|
153
|
124 -- ListObj = List Set
|
|
|
125
|
|
300
|
126 -- ListHom : ListObj → ListObj → Set
|
|
153
|
127
|
