module list-nat0 where open import Level postulate a : Set postulate b : Set postulate c : Set infixr 40 _::_ data List {a} (A : Set a) : Set a where [] : List A _::_ : A → List A → List A infixl 30 _++_ -- _++_ : {a : Level } → {A : Set a} → List A → List A → List A _++_ : ∀ {a} {A : Set a} → List A → List A → List A [] ++ ys = ys (x :: xs) ++ ys = x :: (xs ++ ys) l1 = a :: [] l2 = a :: b :: a :: c :: [] l3 = l1 ++ l2 infixr 20 _==_ data _==_ {n} {A : Set n} : List A → List A → Set n where reflection : {x : List A} → x == x eq-cons : {x y : List A} { a : A } → x == y → ( a :: x ) == ( a :: y ) trans-list : {x y z : List A} { a : A } → x == y → y == z → x == z -- eq-nil : [] == [] list-id-l : { A : Set } → { x : List A} → [] ++ x == x list-id-l = reflection list-id-r : { A : Set } → ( x : List A ) → x ++ [] == x list-id-r [] = reflection list-id-r (x :: xs) = eq-cons ( list-id-r xs ) -- listAssoc : { A : Set } → { a b c : List A} → ( ( a ++ b ) ++ c ) == ( a ++ ( b ++ c ) ) -- listAssoc = eq-reflection list-assoc : {A : Set } → ( xs ys zs : List A ) → ( ( xs ++ ys ) ++ zs ) == ( xs ++ ( ys ++ zs ) ) list-assoc [] ys zs = reflection list-assoc (x :: xs) ys zs = eq-cons ( list-assoc xs ys zs ) open import Relation.Binary.PropositionalEquality open ≡-Reasoning cong1 : ∀{a} {A : Set a } {b} { B : Set b } → ( f : A → B ) → {x : A } → {y : A} → x ≡ y → f x ≡ f y cong1 f refl = refl lemma11 : ∀{n} → ( Set n ) IsRelatedTo ( Set n ) lemma11 = relTo refl lemma12 : {L : Set} ( x : List L ) → x ++ x ≡ x ++ x lemma12 x = begin x ++ x ∎ ++-assoc : {L : Set} ( xs ys zs : List L ) → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs) ++-assoc [] ys zs = -- {A : Set} → -- let open ==-Reasoning A in begin -- to prove ([] ++ ys) ++ zs ≡ [] ++ (ys ++ zs) ( [] ++ ys ) ++ zs ≡⟨ refl ⟩ ys ++ zs ≡⟨ refl ⟩ [] ++ ( ys ++ zs ) ∎ ++-assoc (x :: xs) ys zs = -- {A : Set} → -- let open ==-Reasoning A in begin -- to prove ((x :: xs) ++ ys) ++ zs ≡ (x :: xs) ++ (ys ++ zs) ((x :: xs) ++ ys) ++ zs ≡⟨ refl ⟩ (x :: (xs ++ ys)) ++ zs ≡⟨ refl ⟩ x :: ((xs ++ ys) ++ zs) ≡⟨ cong1 (_::_ x) (++-assoc xs ys zs) ⟩ x :: (xs ++ (ys ++ zs)) ≡⟨ refl ⟩ (x :: xs) ++ (ys ++ zs) ∎ --data Bool : Set where -- true : Bool -- false : Bool --postulate Obj : Set --postulate Hom : Obj → Obj → Set --postulate id : { a : Obj } → Hom a a --infixr 80 _○_ --postulate _○_ : { a b c : Obj } → Hom b c → Hom a b → Hom a c -- postulate axId1 : {a b : Obj} → ( f : Hom a b ) → f == id ○ f -- postulate axId2 : {a b : Obj} → ( f : Hom a b ) → f == f ○ id --assoc : { a b c d : Obj } → -- (f : Hom c d ) → (g : Hom b c) → (h : Hom a b) → -- (f ○ g) ○ h == f ○ ( g ○ h) --a = Set -- ListObj : {A : Set} → List A -- ListObj = List Set -- ListHom : ListObj → ListObj → Set