333 lines
12 KiB
HTML
Executable File
333 lines
12 KiB
HTML
Executable File
<?xml version="1.0" encoding="utf-8"?>
|
||
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
|
||
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
|
||
<html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en">
|
||
<head>
|
||
<!-- 2025-12-28 Sun 20:49 -->
|
||
<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
|
||
<meta name="viewport" content="width=device-width, initial-scale=1" />
|
||
<title>afp_lec_2</title>
|
||
<meta name="generator" content="Org Mode" />
|
||
<style type="text/css">
|
||
#content { max-width: 60em; margin: auto; }
|
||
.title { text-align: center;
|
||
margin-bottom: .2em; }
|
||
.subtitle { text-align: center;
|
||
font-size: medium;
|
||
font-weight: bold;
|
||
margin-top:0; }
|
||
.todo { font-family: monospace; color: red; }
|
||
.done { font-family: monospace; color: green; }
|
||
.priority { font-family: monospace; color: orange; }
|
||
.tag { background-color: #eee; font-family: monospace;
|
||
padding: 2px; font-size: 80%; font-weight: normal; }
|
||
.timestamp { color: #bebebe; }
|
||
.timestamp-kwd { color: #5f9ea0; }
|
||
.org-right { margin-left: auto; margin-right: 0px; text-align: right; }
|
||
.org-left { margin-left: 0px; margin-right: auto; text-align: left; }
|
||
.org-center { margin-left: auto; margin-right: auto; text-align: center; }
|
||
.underline { text-decoration: underline; }
|
||
#postamble p, #preamble p { font-size: 90%; margin: .2em; }
|
||
p.verse { margin-left: 3%; }
|
||
pre {
|
||
border: 1px solid #e6e6e6;
|
||
border-radius: 3px;
|
||
background-color: #f2f2f2;
|
||
padding: 8pt;
|
||
font-family: monospace;
|
||
overflow: auto;
|
||
margin: 1.2em;
|
||
}
|
||
pre.src {
|
||
position: relative;
|
||
overflow: auto;
|
||
}
|
||
pre.src:before {
|
||
display: none;
|
||
position: absolute;
|
||
top: -8px;
|
||
right: 12px;
|
||
padding: 3px;
|
||
color: #555;
|
||
background-color: #f2f2f299;
|
||
}
|
||
pre.src:hover:before { display: inline; margin-top: 14px;}
|
||
/* Languages per Org manual */
|
||
pre.src-asymptote:before { content: 'Asymptote'; }
|
||
pre.src-awk:before { content: 'Awk'; }
|
||
pre.src-authinfo::before { content: 'Authinfo'; }
|
||
pre.src-C:before { content: 'C'; }
|
||
/* pre.src-C++ doesn't work in CSS */
|
||
pre.src-clojure:before { content: 'Clojure'; }
|
||
pre.src-css:before { content: 'CSS'; }
|
||
pre.src-D:before { content: 'D'; }
|
||
pre.src-ditaa:before { content: 'ditaa'; }
|
||
pre.src-dot:before { content: 'Graphviz'; }
|
||
pre.src-calc:before { content: 'Emacs Calc'; }
|
||
pre.src-emacs-lisp:before { content: 'Emacs Lisp'; }
|
||
pre.src-fortran:before { content: 'Fortran'; }
|
||
pre.src-gnuplot:before { content: 'gnuplot'; }
|
||
pre.src-haskell:before { content: 'Haskell'; }
|
||
pre.src-hledger:before { content: 'hledger'; }
|
||
pre.src-java:before { content: 'Java'; }
|
||
pre.src-js:before { content: 'Javascript'; }
|
||
pre.src-latex:before { content: 'LaTeX'; }
|
||
pre.src-ledger:before { content: 'Ledger'; }
|
||
pre.src-lisp:before { content: 'Lisp'; }
|
||
pre.src-lilypond:before { content: 'Lilypond'; }
|
||
pre.src-lua:before { content: 'Lua'; }
|
||
pre.src-matlab:before { content: 'MATLAB'; }
|
||
pre.src-mscgen:before { content: 'Mscgen'; }
|
||
pre.src-ocaml:before { content: 'Objective Caml'; }
|
||
pre.src-octave:before { content: 'Octave'; }
|
||
pre.src-org:before { content: 'Org mode'; }
|
||
pre.src-oz:before { content: 'OZ'; }
|
||
pre.src-plantuml:before { content: 'Plantuml'; }
|
||
pre.src-processing:before { content: 'Processing.js'; }
|
||
pre.src-python:before { content: 'Python'; }
|
||
pre.src-R:before { content: 'R'; }
|
||
pre.src-ruby:before { content: 'Ruby'; }
|
||
pre.src-sass:before { content: 'Sass'; }
|
||
pre.src-scheme:before { content: 'Scheme'; }
|
||
pre.src-screen:before { content: 'Gnu Screen'; }
|
||
pre.src-sed:before { content: 'Sed'; }
|
||
pre.src-sh:before { content: 'shell'; }
|
||
pre.src-sql:before { content: 'SQL'; }
|
||
pre.src-sqlite:before { content: 'SQLite'; }
|
||
/* additional languages in org.el's org-babel-load-languages alist */
|
||
pre.src-forth:before { content: 'Forth'; }
|
||
pre.src-io:before { content: 'IO'; }
|
||
pre.src-J:before { content: 'J'; }
|
||
pre.src-makefile:before { content: 'Makefile'; }
|
||
pre.src-maxima:before { content: 'Maxima'; }
|
||
pre.src-perl:before { content: 'Perl'; }
|
||
pre.src-picolisp:before { content: 'Pico Lisp'; }
|
||
pre.src-scala:before { content: 'Scala'; }
|
||
pre.src-shell:before { content: 'Shell Script'; }
|
||
pre.src-ebnf2ps:before { content: 'ebfn2ps'; }
|
||
/* additional language identifiers per "defun org-babel-execute"
|
||
in ob-*.el */
|
||
pre.src-cpp:before { content: 'C++'; }
|
||
pre.src-abc:before { content: 'ABC'; }
|
||
pre.src-coq:before { content: 'Coq'; }
|
||
pre.src-groovy:before { content: 'Groovy'; }
|
||
/* additional language identifiers from org-babel-shell-names in
|
||
ob-shell.el: ob-shell is the only babel language using a lambda to put
|
||
the execution function name together. */
|
||
pre.src-bash:before { content: 'bash'; }
|
||
pre.src-csh:before { content: 'csh'; }
|
||
pre.src-ash:before { content: 'ash'; }
|
||
pre.src-dash:before { content: 'dash'; }
|
||
pre.src-ksh:before { content: 'ksh'; }
|
||
pre.src-mksh:before { content: 'mksh'; }
|
||
pre.src-posh:before { content: 'posh'; }
|
||
/* Additional Emacs modes also supported by the LaTeX listings package */
|
||
pre.src-ada:before { content: 'Ada'; }
|
||
pre.src-asm:before { content: 'Assembler'; }
|
||
pre.src-caml:before { content: 'Caml'; }
|
||
pre.src-delphi:before { content: 'Delphi'; }
|
||
pre.src-html:before { content: 'HTML'; }
|
||
pre.src-idl:before { content: 'IDL'; }
|
||
pre.src-mercury:before { content: 'Mercury'; }
|
||
pre.src-metapost:before { content: 'MetaPost'; }
|
||
pre.src-modula-2:before { content: 'Modula-2'; }
|
||
pre.src-pascal:before { content: 'Pascal'; }
|
||
pre.src-ps:before { content: 'PostScript'; }
|
||
pre.src-prolog:before { content: 'Prolog'; }
|
||
pre.src-simula:before { content: 'Simula'; }
|
||
pre.src-tcl:before { content: 'tcl'; }
|
||
pre.src-tex:before { content: 'TeX'; }
|
||
pre.src-plain-tex:before { content: 'Plain TeX'; }
|
||
pre.src-verilog:before { content: 'Verilog'; }
|
||
pre.src-vhdl:before { content: 'VHDL'; }
|
||
pre.src-xml:before { content: 'XML'; }
|
||
pre.src-nxml:before { content: 'XML'; }
|
||
/* add a generic configuration mode; LaTeX export needs an additional
|
||
(add-to-list 'org-latex-listings-langs '(conf " ")) in .emacs */
|
||
pre.src-conf:before { content: 'Configuration File'; }
|
||
|
||
table { border-collapse:collapse; }
|
||
caption.t-above { caption-side: top; }
|
||
caption.t-bottom { caption-side: bottom; }
|
||
td, th { vertical-align:top; }
|
||
th.org-right { text-align: center; }
|
||
th.org-left { text-align: center; }
|
||
th.org-center { text-align: center; }
|
||
td.org-right { text-align: right; }
|
||
td.org-left { text-align: left; }
|
||
td.org-center { text-align: center; }
|
||
dt { font-weight: bold; }
|
||
.footpara { display: inline; }
|
||
.footdef { margin-bottom: 1em; }
|
||
.figure { padding: 1em; }
|
||
.figure p { text-align: center; }
|
||
.equation-container {
|
||
display: table;
|
||
text-align: center;
|
||
width: 100%;
|
||
}
|
||
.equation {
|
||
vertical-align: middle;
|
||
}
|
||
.equation-label {
|
||
display: table-cell;
|
||
text-align: right;
|
||
vertical-align: middle;
|
||
}
|
||
.inlinetask {
|
||
padding: 10px;
|
||
border: 2px solid gray;
|
||
margin: 10px;
|
||
background: #ffffcc;
|
||
}
|
||
#org-div-home-and-up
|
||
{ text-align: right; font-size: 70%; white-space: nowrap; }
|
||
textarea { overflow-x: auto; }
|
||
.linenr { font-size: smaller }
|
||
.code-highlighted { background-color: #ffff00; }
|
||
.org-info-js_info-navigation { border-style: none; }
|
||
#org-info-js_console-label
|
||
{ font-size: 10px; font-weight: bold; white-space: nowrap; }
|
||
.org-info-js_search-highlight
|
||
{ background-color: #ffff00; color: #000000; font-weight: bold; }
|
||
.org-svg { }
|
||
</style>
|
||
|
||
<link rel="stylesheet" href="/assets/styles/style.css" />
|
||
<link rel="stylesheet" href="/assets/styles/bigger-picture.min.css" />
|
||
<link rel="stylesheet" href="/assets/styles/media.css" />
|
||
|
||
<script src="/assets/scripts/script.js" defer></script>
|
||
<script src="/assets/scripts/search.js" defer></script>
|
||
<script src="/assets/scripts/bigger-picture.min.js" defer></script>
|
||
<script src="/assets/scripts/svg-pan-zoom.min.js" defer></script>
|
||
<script src="/assets/scripts/gallery-init.js" defer></script>
|
||
</head>
|
||
<body>
|
||
<div id="preamble" class="status">
|
||
|
||
<div class="banner-header">
|
||
<div class="banner-left">
|
||
<a href="/20241210233721-brain_moc.html"> <img src="/assets/gr.png" alt="Site Logo" class="banner-logo" /> </a>
|
||
<div id="updated">Updated: 2025-12-28 Sun 19:48</div>
|
||
</div>
|
||
|
||
<div class="banner-search">
|
||
<input id="search-box"
|
||
type="search"
|
||
placeholder="Search notes…"
|
||
aria-label="Search notes"
|
||
autocomplete="off" />
|
||
<div id="search-results"></div>
|
||
</div>
|
||
|
||
<button id="close-all">Close All</button>
|
||
</div>
|
||
</div>
|
||
<div id="stack-root">
|
||
<div class="stack-track">
|
||
<article class="stack-pane pane-root" data-url="/20250128111008-afp_lec_2.html">
|
||
<div id="content" class="content">
|
||
<div class="title-section">
|
||
<div class="title-controls">
|
||
<button class="pane-fullscreen" aria-label="Fullscreen">F</button>
|
||
<button class="pane-edit" aria-label="Edit pane">E</button>
|
||
<button class="pane-close" aria-label="Close pane">×</button>
|
||
</div>
|
||
<h1 class="title">afp<sub>lec</sub><sub>2</sub></h1>
|
||
<div class="title-metadata">
|
||
<span class="metadata-item">
|
||
<span class="metadata-label">planted:</span>
|
||
<span class="metadata-value">2025-01-28</span>
|
||
</span>
|
||
<span class="metadata-item">
|
||
<span class="metadata-label">last tended to:</span>
|
||
<span class="metadata-value">2025-12-28</span>
|
||
</span>
|
||
</div>
|
||
</div>
|
||
<ul class="org-ul">
|
||
<li>List are dependant, thats what makes it so special.</li>
|
||
</ul>
|
||
|
||
|
||
<p>
|
||
```agda
|
||
data <span class="underline">≡</span> {X : Type} : X → X → Type where
|
||
refl : (x : X) → x ≡ x
|
||
</p>
|
||
|
||
<p>
|
||
infix 0 <span class="underline">≡</span>
|
||
```
|
||
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 : ≡
|
||
</p>
|
||
|
||
|
||
|
||
<p>
|
||
we want to write propositions as types and proofs as programs.
|
||
</p>
|
||
|
||
<p>
|
||
A proof is a convincing argument. How do you convince someone that something you believe is true is actually true, it ivolves reasoning.
|
||
</p>
|
||
<div id="outline-container-orgf1944d5" class="outline-2">
|
||
<h2 id="orgf1944d5"><a href="#orgf1944d5">AND</a></h2>
|
||
<div class="outline-text-2" id="text-orgf1944d5">
|
||
<p>
|
||
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.
|
||
</p>
|
||
|
||
<p>
|
||
a : A
|
||
the little `a` is a justification of the the big `A`. little a is a way to prove that big A holds.
|
||
</p>
|
||
|
||
<p>
|
||
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.
|
||
</p>
|
||
|
||
<p>
|
||
```agda
|
||
</p>
|
||
|
||
<p>
|
||
data _ x _ (A B : Type) : Type where
|
||
_ , _ : A -> B -> A x B
|
||
</p>
|
||
|
||
<p>
|
||
```
|
||
</p>
|
||
|
||
<p class="backlinks-section" id="backlinks">
|
||
Backlinks
|
||
</p>
|
||
<ul class="org-ul backlinks-list">
|
||
<li><a href="20250128110828-afp_week2.html#ID-4bc71106-1d2b-4c71-836d-54b738fe5ff5">afp<sub>week2</sub></a></li>
|
||
</ul>
|
||
</div>
|
||
</div>
|
||
</div>
|
||
</div></article></div></div>
|
||
<div id="postamble" class="status">
|
||
<footer>
|
||
<div class="copyright-container">
|
||
<div class="copyright">
|
||
Copyright © 2022-2025 Zaine Qayyum. All rights reserved unless otherwise noted.</div></div>
|
||
<div class="generated">
|
||
Created with <a href="https://www.gnu.org/software/emacs/">Emacs</a> 30.2 (<a href="https://orgmode.org">Org</a> mode 9.7.11) on <a href="https://www.archlinux.org/">Arch</a> <a href="https://www.gnu.org">GNU</a>/<a href="https://www.kernel.org/">Linux</a>
|
||
</div>
|
||
</footer>
|
||
</div>
|
||
</body>
|
||
</html>
|