44 lines
1.4 KiB
Org Mode
44 lines
1.4 KiB
Org Mode
:PROPERTIES:
|
|
:ID: 460f4a49-8ae4-444a-bf82-4e14ca7cad3f
|
|
:END:
|
|
#+title: afp_lec_2
|
|
#+filetags: :uni:notes:
|
|
|
|
- List are dependant, thats what makes it so special.
|
|
|
|
|
|
```agda
|
|
data _≡_ {X : Type} : X → X → Type where
|
|
refl : (x : X) → x ≡ x
|
|
|
|
infix 0 _≡_
|
|
```
|
|
Here is the identity type. For every type X, im going to define two elements of X, and the only way to define this element the constructor of which is single. The type is like a proposition and the element is like the proof. By just having this rule we can do everything we wanna do, for example, proving that if x=y, y=x.
|
|
Definition equal : =
|
|
Type equality : ≡
|
|
|
|
|
|
|
|
we want to write propositions as types and proofs as programs.
|
|
|
|
A proof is a convincing argument. How do you convince someone that something you believe is true is actually true, it ivolves reasoning.
|
|
* AND
|
|
To prove A and B we have to prove A, and also prove B. Proof by arguments; you have to argue/justify that A is true and that B is true.
|
|
|
|
a : A
|
|
the little `a` is a justification of the the big `A`. little a is a way to prove that big A holds.
|
|
|
|
So for this it would be:
|
|
a : A
|
|
b : B
|
|
and we need that both holds, imagine them as pairs: (a , b)
|
|
cartesian product -> (a , b) : A x B
|
|
the cartesian product is just a set of pairs. The below is a translation of conjunction to cartesian product in Agda.
|
|
|
|
```agda
|
|
|
|
data _ x _ (A B : Type) : Type where
|
|
_ , _ : A -> B -> A x B
|
|
|
|
```
|