Mercurial > hg > Members > kono > Proof > category

comparison src/list-nat0.agda @ 1124:f683d96fbc93 default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
safe fix done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 07 Jul 2024 22:28:50 +0900
parents ac53803b3b2a
children
comparison
equal deleted inserted replaced
1123:b6ab443f7a43 1124:f683d96fbc93
1 {-# OPTIONS --cubical-compatible --safe #-}
1 module list-nat0 where 2 module list-nat0 where
2 3
3 open import Level 4 open import Level
4 5
5 6 data i3 : Set where
6 postulate a : Set 7 a : i3
7 postulate b : Set 8 b : i3
8 postulate c : Set 9 c : i3
9 10
10 11
11 infixr 40 _::_ 12 infixr 40 _::_
12 data List {a} (A : Set a) : Set a where 13 data List {a} (A : Set a) : Set a where
13 [] : List A 14 [] : List A
57 58
58 cong1 : ∀{a} {A : Set a } {b} { B : Set b } → 59 cong1 : ∀{a} {A : Set a } {b} { B : Set b } →
59 ( f : A → B ) → {x : A } → {y : A} → x ≡ y → f x ≡ f y 60 ( f : A → B ) → {x : A } → {y : A} → x ≡ y → f x ≡ f y
60 cong1 f refl = refl 61 cong1 f refl = refl
61 62
62 lemma11 : ∀{n} → ( Set n ) IsRelatedTo ( Set n ) 63 -- lemma11 : ∀{n} → ( Set n ) IsRelatedTo ( Set n )
63 lemma11 = relTo refl 64 -- lemma11 = relTo refl
64 65
65 lemma12 : {L : Set} ( x : List L ) → x ++ x ≡ x ++ x 66 lemma12 : {L : Set} ( x : List L ) → x ++ x ≡ x ++ x
66 lemma12 x = begin x ++ x ∎ 67 lemma12 x = begin x ++ x ∎
67 68
68 69