Skip to content
This repository

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse code

IDesc model: paranoid alpha-renaming.

  • Loading branch information...
commit 78bcef35a43173b501f51932b84fa2cdfc150ca9 1 parent 7359720
authored August 24, 2010

Showing 1 changed file with 6 additions and 6 deletions. Show diff stats Hide diff stats

  1. 12  models/IDesc.agda
12  models/IDesc.agda
@@ -127,12 +127,12 @@ data IMu {l : Level}{I : Set (suc l)}(R : I -> IDesc {l = l} I)(i : I) : Set l w
127 127
 -- Predicate: Box
128 128
 --********************************************
129 129
 
130  
-box : {l : Level}{I : Set (suc l)}(D : IDesc I)(P : I -> Set l) -> desc D P -> IDesc (Sigma I P)
131  
-box (var i)     P x        = var (i , x)
132  
-box (const X)   P x        = const Unit
133  
-box (prod D D') P (d , d') = prod (box D P d) (box D' P d')
134  
-box (sigma S T) P (a , b)  = box (T a) P b
135  
-box (pi S T)    P f        = pi S (\s -> box (T s) P (f s))
  130
+box : {l : Level}{I : Set (suc l)}(D : IDesc I)(X : I -> Set l) -> desc D X -> IDesc (Sigma I X)
  131
+box (var i)     X x        = var (i , x)
  132
+box (const _)   X x        = const Unit
  133
+box (prod D D') X (d , d') = prod (box D X d) (box D' X d')
  134
+box (sigma S T) X (a , b)  = box (T a) X b
  135
+box (pi S T)    X f        = pi S (\s -> box (T s) X (f s))
136 136
 
137 137
 --********************************************
138 138
 -- Elimination principle: induction

0 notes on commit 78bcef3

Please sign in to comment.
Something went wrong with that request. Please try again.