===== A type system as a model for some concepts =====
| [[Drawing arrows and coding functions]] $\blacktriangleright$ A type system as a model for some concepts $\blacktriangleright$ [[Foundational temp1 ]] |
==== Guide ====
We introduce some basic notions of Idris, namely those that can be seen as "semantics" for logic, set theory and category theory (or rather topoi, as discussed in
[[http://arxiv.org/abs/1212.6543 | Leinster, Rethinking set theory]]). However, we always treat the (chosen subpart of the) language from a syntactical perspective as a programming language, //as is//, and don't "force it into" a known mathematical structure. In particular, many forms of "equality" often make problems. Then again, it's always good to know how to map your stuff //into// mathematical frameworks (e.g. into a well defined category), even if that mapping is neither surjective nor even injective.

(161013 The code presented below is also all included on the page [[Idris syntax]], but that's just for now.)

=== tmp Overview ===
== easy ==

  * 2 There is a set {0} with exactly one element 
  * 3 There is a set {} with no elements 
  * 6 Given sets X and Y, one can form the set of functions from X to Y
  * 5 Given sets X and Y, one can form their Cartesian product X x Y (pullback with {0} in the middle)
  * 9 The natural numbers form a set 
  * 1 Composition of functions is associative and there are identity functions

== harder (needs dependent types) ==

  * 8 The subsets of a set X correspond to the functions from X to {0,1} (subobject classifier pullback)
  * 7 Given f:X->Y and y:Y, one can form the inverse image of f (pullback with {0} on one side)

== harder (ew) ==

  * 10 Every surjection has a right inverse (muh axiom of choice, easy if surjective functions are defined as function type where surjectivity must be proven for terms)
  * 4 A function is determined by its effect on elements (muh (function) extensionality)





=== Types ===
>Want to talk about functions, need types

== Finite types ==
>Beagle, Kid
>Draw the corresponding arrows (akin to Lawyeres babby book)

>For any number {0, 1, 2, 3, ..., 17, 18, ...} we can form a type with that many terms

== Unit type ==
== Empty type ==

=== Functions ===
== Function type ==
>basic function definition (forth, back, permutation, identity)
>Draw the corresponding arrows (akin to Lawyeres babby book)

>given $f:X\to Y$, point out how $i:S\to{X}$ and $j:X\to{T}$ induces functions $(f\circ{i}):S\to Y$, $(j\circ{f}):X\to T$ with potentially restricted domain resp. codomain. It's always interesting to see how a given function $g$ may factor into other functions. Parts of "factors" may be general and important functions, defined for very general input, or e.g. components of natural transformations, etc.

== introduce dependent types ==

== Pullback ==
<code/Haskell>
data Pullback : (f : x -> z) -> (g : y -> z) -> Type
	where MkPullback : (tx : x) -> (ty : y) -> (f tx = g ty) -> (Pullback f g)
-- MkPullback maps a term tx, a term ty and a proof 
-- that f tx = g ty to a global element of Pullback f g
	
times8 : Nat -> Nat
times8 k = k*8

square : Nat -> Nat
square n = n*n

aSolution : Pullback Test.times8 Test.square
aSolution = MkPullback 2 4 Refl
-- The compiler already reduces the type '2*8 = 4*4' to '16 = 16' and Refl proves this

--willNotCompile : Pullback Test.times8 Test.square
--willNotCompile = MkPullback 3 5 Refl 
-- The compiler reduces '3*8 = 5*5' to '24 = 25' and then down to '0 = 1' 
-- but there is actually no way to prove this. In particular, Refl won't do
</code>
{{pullback_category_theory.png?X250 }}

== Product ==
>cheap product
>actual product syntax

== injections, subsets ==

== Nats ==
(infinitely large type)

=== Properties ===
using dependent types, prove the properties discussed below (if possible)

== of Functions ==
>identity exists
>associations

== of Types ==
>of empty
>of unit
>of product
>of exponential object
>of Nat

== caty ==
>all of the above in terms of universal properties

=== More on Functions ===
>Type level functions (type constructors)

>Functors
>Monads

=== Reference ===
ArXiv:
[[http://arxiv.org/abs/1212.6543|Leinster, Rethinking set theory]]

-----
=== Sequel of ===
[[Drawing arrows and coding functions]]