post-lecture typo/thinko fixes

IR.lagda

@@ -217,8 +217,8 @@ right end. That means \emph{left}-nested record types (also known as
 mutual
 
   data RecL : Set1 where
-    Em : RecL
-    _::_ : {n : Nat}(R : RecL)(A : <! R !>RL -> Set)  -> RecL
+    Em    : RecL
+    _::_  : (R : RecL)(A : <! R !>RL -> Set)  -> RecL
 
   <!_!>RL : RecL -> Set
   <! Em !>RL      = One

IRDS.lagda

@@ -210,7 +210,7 @@ following exercise.
 \begin{exe}[composition for |DS|]
 This is an open problem. Construct
 \begin{spec}
-coDS : forall {I J K} -> DS J K -> DS I K -> DS I K
+coDS : forall {I J K} -> DS J K -> DS I J -> DS I K
 coDS E D = ?
 \end{spec}
 such that

Lec5.agda

@@ -25,9 +25,15 @@ sum   (suc n)  f  = f zero +Nat sum n (f o suc)
 prod  zero     _  = 1
 prod  (suc n)  f  = f zero *Nat sum n (f o suc)
 
-data FTy : Set where
-  fin    : Nat -> FTy
-  sg pi  : (S : FTy)(T : Fin {!!} -> FTy) -> FTy
+mutual
+  data FTy : Set where
+    fin    : Nat -> FTy
+    sg pi  : (S : FTy)(T : # S -> FTy) -> FTy
+
+  # : FTy -> Set
+  # (fin n) = Fin n
+  # (sg S T) = Sg (# S) (\ s -> # (T s))
+  # (pi S T) = (s : # S) -> # (T s)
 
   -- do it with Nat, #, then  tweak it to Set
 
@@ -51,12 +57,14 @@ mutual
 
   data RecL : Set1 where
     Em : RecL
-    _::_ : {n : Nat}(R : RecL)(A : <! R !>RL -> Set)  -> RecL
+    _::_ : (R : RecL)(A : <! R !>RL -> Set)  -> RecL
 
   <!_!>RL : RecL -> Set
   <! Em !>RL      = One
   <! R :: A !>RL  = Sg <! R !>RL A
 
+
+
 -- mention manifest fields
 
 -- but now, a serious universe
@@ -78,11 +86,19 @@ mutual
 
 data DS (I J : Set1) : Set1 where
   io  : J -> DS I J                                   -- no more fields
+  sg  : (A : Set)(T : A -> DS I J) -> DS I J          -- non-rec field
+  de  : (H : Set)(T : (H -> I) -> DS I J) -> DS I J
 
 <!_!>DS : forall {I J} -> DS I J -> Fam I -> Fam J
 <! io j    !>DS  Xxi
   =  One
   ,  \ { <>        -> j }
+<! sg A T  !>DS  Xxi
+  = (Sg A \ a -> fst (<! T a !>DS Xxi))
+  , (\ { (a , t) -> snd (<! T a !>DS Xxi) t })
+<! de H T !>DS (X , xi)
+  = (Sg (H -> X) \ hx -> fst (<! T (xi o hx) !>DS (X , xi)))
+  , (\ { (hx , t) -> snd (<! T (xi o hx) !>DS (X , xi)) t })
 
 mutual  -- fails positivity check and termination check
 
@@ -94,10 +110,8 @@ mutual  -- fails positivity check and termination check
 
 -- mention bind
 
-{-
-coDS : forall {I J K} -> DS J K -> DS I K -> DS I K
+coDS : forall {I J K} -> DS J K -> DS I J -> DS I K
 coDS E D = {!!}
--}
 
 {-
 PiF :  (S : Set){J : S -> Set1}(T : (s : S) -> Fam (J s)) ->

Lec6.agda

@@ -2,17 +2,20 @@ module Lec6 where
 
 open import IR public
 
-data Favourite : (Nat -> Nat) -> Set where
-  favourite : Favourite (\ x -> zero +Nat x)
+data Favourite (f : Nat -> Nat) : Set where
+  favourite : (\ x -> zero +Nat x) == f -> Favourite f
 
-plusZero : forall x -> zero +Nat x == x +Nat zero
-plusZero x = {!!}
+plusZero : forall x -> x == x +Nat zero
+plusZero zero = refl
+plusZero (suc x)  = cong suc (plusZero x)
 
 closedFact : (\ x -> zero +Nat x) == (\ x -> x +Nat zero)
 closedFact = extensionality _ _ plusZero
 
-myTerm = subst closedFact Favourite favourite
+myTerm = subst closedFact Favourite (favourite refl)
 
+help : Favourite (λ x → x +Nat 0)
+help = favourite closedFact
 
 -- remark on intensional predicates
 -- remark on the need for a more type-based computation mechanism
@@ -27,13 +30,59 @@ mutual
   Eq : (X : TU)(x : <! X !>TU) -> (Y : TU)(y : <! Y !>TU) -> TU
   Eq X x Y y = snd (EQ X Y) x y
 
-  EQ X Y = {!!}
+  EQ Zero' Zero' = One' , \ _ _ -> One'
+
+  EQ One' One' = One' , \ _ _ -> One'
+  EQ Two' Two' = One' , (\
+    { tt tt -> One'
+    ; ff ff -> One'
+    ; _ _ -> Zero'
+    })
+  EQ (Sg' X T) (Sg' Y T₁) = {!!}
+  EQ (Pi' S T) (Pi' S' T') = {!!}
+  EQ (Tree' X F i) (Tree' Y F₁ i₁) = {!!}
+  EQ _ _ = Zero' , \ _ _ -> One'
 
 coe : (X Y : TU) -> <! X <-> Y !>TU -> <! X !>TU -> <! Y !>TU
 
 postulate
   coh :  (X Y : TU)(Q : <! X <-> Y !>TU)(x : <! X !>TU) ->
          <! Eq X x Y (coe X Y Q x) !>TU
 
-coe X Y Q x = {!!}
+coe Zero' Zero' Q x = {!!}
+coe Zero' One' Q x = {!!}
+coe Zero' Two' Q x = {!!}
+coe Zero' (Sg' Y T) Q x = {!!}
+coe Zero' (Pi' Y T) Q x = {!!}
+coe Zero' (Tree' Y F i) Q x = {!!}
+coe One' Zero' Q x = {!!}
+coe One' One' Q x = {!!}
+coe One' Two' Q x = {!!}
+coe One' (Sg' Y T) Q x = {!!}
+coe One' (Pi' Y T) Q x = {!!}
+coe One' (Tree' Y F i) Q x = {!!}
+coe Two' Zero' Q x = {!!}
+coe Two' One' Q x = {!!}
+coe Two' Two' Q x = {!!}
+coe Two' (Sg' Y T) Q x = {!!}
+coe Two' (Pi' Y T) Q x = {!!}
+coe Two' (Tree' Y F i) Q x = {!!}
+coe (Sg' X T) Zero' () x
+coe (Sg' X T) One' Q x = {!!}
+coe (Sg' X T) Two' Q x = {!!}
+coe (Sg' S T) (Sg' S' T') Q (s , t) = {!!}
+coe (Sg' X T) (Pi' Y T₁) Q x = {!!}
+coe (Sg' X T) (Tree' Y F i) Q x = {!!}
+coe (Pi' X T) Zero' Q x = {!!}
+coe (Pi' X T) One' Q x = {!!}
+coe (Pi' X T) Two' Q x = {!!}
+coe (Pi' X T) (Sg' Y T₁) Q x = {!!}
+coe (Pi' X T) (Pi' Y T₁) Q x = {!!}
+coe (Pi' X T) (Tree' Y F i) Q x = {!!}
+coe (Tree' X F i) Zero' Q x = {!!}
+coe (Tree' X F i) One' Q x = {!!}
+coe (Tree' X F i) Two' Q x = {!!}
+coe (Tree' X F i) (Sg' Y T) Q x = {!!}
+coe (Tree' X F i) (Pi' Y T) Q x = {!!}
+coe (Tree' X F i) (Tree' Y F₁ i₁) Q x = {!!}
 

NormT.lagda

@@ -131,7 +131,7 @@ observe the corresponding naturality. We thus need a notion of
 %format -:> = "\F{\dot{\to}}"
 %format _-:>_ = "\us{" -:> "}"
 %format AppHom = "\D{AppHom}"
-%format respPure = "\F{resp}" pure
+%format respPure = "\F{respPure}"
 %format respApp = "\F{resp}" <*>
 \begin{code}
 _-:>_ : forall (F G : Set -> Set) -> Set1