-- {\Large \bf Basic Type Theory}

--

-- 

Fam (A::Set) :: Type
  = A -> Set

-- {\em Syntactic sugar for the $\Pi$-construction}

Pi (A::Set)(B::Fam A) :: Set
  = (x::A) -> B x

ForAll (A::Set)(B::Fam A) :: Set
  = (x::A) -> B x

-- {\em Syntactic sugar relating to the $\Sigma$-construction}

Sigma (A::Set)(B::Fam A) :: Set
  = sig{_1 :: A;
        _2 :: B _1;}

Exists (A::Set)(B::Fam A) :: Set
  = sig{_1 :: A;
        _2 :: B _1;}

pair (A::Set)(B::Fam A)(a::A)(b::B a) :: Sigma A B
  = struct {
      _1 = a;
      _2 = b;}

pairExists (A::Set)(B::Fam A)(a::A)(b::B a) :: Exists A B
  = struct {
      _1 = a;
      _2 = b;}

split (A::Set)
      (B::Fam A)
      (C::Fam (Sigma A B))
      (c::Sigma A B)
      (d::(x::A) -> (y::B x) -> C (pair A B x y))
  :: C c
  = d c._1 c._2

splitExists (A::Set)
            (B::Fam A)
            (C::Fam (Exists A B))
            (c::Exists A B)
            (d::(x::A) -> (y::B x) -> C (pairExists A B x y))
  :: C c
  = d c._1 c._2

Cart (A::Set)(B::Set) :: Set
  = sig{_1 :: A;
        _2 :: B;}

pairCart (A::Set)(B::Set)(a::A)(b::B) :: Cart A B
  = struct {
      _1 = a;
      _2 = b;}

proj1 (A::Set)(B::Set)(c::Cart A B) :: A
  = c._1

proj2 (A::Set)(B::Set)(c::Cart A B) :: B
  = c._2

and (A::Set)(B::Set) :: Set
  = Cart A B

-- {\em Disjoint binary sums}

Sum (A::Set)(B::Set) :: Set
  = data inl (x::A) | inr (y::B)

or (A::Set)(B::Set) :: Set
  = Sum A B

when (A::Set)
     (B::Set)
     (C::Fam (Sum A B))
     (c::Sum A B)
     (d::(x::A) -> C (inl@_ x))
     (e::(y::B) -> C (inr@_ y))
  :: C c
  = case c of {
      (inl x) -> d x;
      (inr y) -> e y;}

-- {\em If and only if}

iff (A::Set)(B::Set) :: Set
  = Cart (A -> B) (B -> A)

-- {\em The empty set}

empty :: Set
  = data 

Absurd :: Set
  = empty

elempty (A::Set)(x::empty) :: A
  = case x of { }

not (A::Set) :: Set
  = A -> Absurd

-- {\em A unit set}

Unit :: Set
  = data elt

True :: Set
  = Unit

-- {\em Booleans}

Bool :: Set
  = data ff | tt

-- {\em Natural numbers}

Nat :: Set
  = data zero | succ (x::Nat)

rec (C::(z::Nat) -> Set)
    (t::Nat)
    (f::C zero@_)
    (g::(x::Nat) -> (y::C x) -> C (succ@_ x))
  :: C t
  = case t of {
      (zero) -> f;
      (succ x) -> g x (rec C x f g);}

-- {\em A basic dependent type}

L (z::Nat) :: Set
  = case z of {
      (zero) -> empty;
      (succ x) -> Nat;}

-- {\em Deriving first projection from split}

pr1 (A::Set)(B::Fam A)(c::Sigma A B) :: A
  = split A B (\(h::Sigma A B) -> A) c (\(x::A) -> \(y::B x) -> x)

pr2 (A::Set)(B::Fam A)(c::Sigma A B) :: B (pr1 A B c)
  = split
      A
      B
      (\(h::Sigma A B) -> B (pr1 A B h))
      c
      (\(x::A) -> \(y::B x) -> y)
{-# Alfa unfoldgoals off
brief on
hidetypeannots off
wide

nd
hiding on
con "zero" as "0"
con "succ" as "S"
var "Nat" as "N" with symbolfont
var "Prod" infix 7 as "´" with symbolfont
var "Sum" infix as "+"
var "Fun" infix rightassoc as "®" with symbolfont
var "apply" hide 2
var "pair" hide 2 tuple
var "pr1" hide 2
var "pr2" hide 2
var "rec" hide 1
var "when" hide 3
var "empty" as "Æ" with symbolfont
var "elempty" as "!"
var "Pi" as "P" with symbolfont
var "Sigma" as "S" with symbolfont
var "split" hide 3
var "Cart" infix as "´" with symbolfont
con "sigma" as "s" with symbolfont
con "emb" as "e" with symbolfont
var "Power" as "Rw"
var "Member" hide 2
var "Subclass" hide 3 infix as "Í" with symbolfont
var "iff" infix as "«" with symbolfont
var "Can" as "G" with symbolfont
var "ind"
var "fam"
var "R" as "R"
var "and" infix as "Ù" with symbolfont
var "MemberSE" hide 3 infix as "e" with symbolfont
var "MemberE" hide 2 infix as "e" with symbolfont
var "EqualE" hide 2 infix as "=="
var "SubsetsE" hide 2 infix as "Í" with symbolfont
var "EqualsetsSE" hide 3 infix as "=="
var "SubsetSE" hide 3 infix as "Í" with symbolfont
var "E"
var "Es"
var "Rs" infix as "<" with symbolfont
var "Ex" infix as "<<" with symbolfont
var "Exs" infix as "<<" with symbolfont
var "proj1" hide 2
var "proj2" hide 2
var "ForAll" hide 1 quantifier domain on as "\"" with symbolfont
var "Exists" hide 1 quantifier domain on as "$" with symbolfont
con "cross" infix as "´" with symbolfont
var "or" infix as "Ú" with symbolfont
var "not" as "Ø" with symbolfont
var "Absurd" as "^" with symbolfont
var "pairExists" hide 2 tuple
var "pairCart" hide 2 tuple
 #-}