98 where constant @{term three} is explicitly defined as the representing set: |
98 where constant @{term three} is explicitly defined as the representing set: |
99 \begin{center} |
99 \begin{center} |
100 @{thm three_def}\hfill(@{thm[source]three_def}) |
100 @{thm three_def}\hfill(@{thm[source]three_def}) |
101 \end{center} |
101 \end{center} |
102 The situation is best summarized with the help of the following diagram, |
102 The situation is best summarized with the help of the following diagram, |
103 where squares are types and circles are sets: |
103 where squares denote types and the irregular region denotes a set: |
104 \begin{center} |
104 \begin{center} |
105 \unitlength1mm |
105 \includegraphics[scale=.8]{Types/typedef} |
106 \thicklines |
|
107 \begin{picture}(100,40) |
|
108 \put(3,13){\framebox(15,15){@{typ three}}} |
|
109 \put(55,5){\framebox(30,30){@{term three}}} |
|
110 \put(70,32){\makebox(0,0){@{typ nat}}} |
|
111 \put(70,20){\circle{40}} |
|
112 \put(10,15){\vector(1,0){60}} |
|
113 \put(25,14){\makebox(0,0)[tl]{@{term Rep_three}}} |
|
114 \put(70,25){\vector(-1,0){60}} |
|
115 \put(25,26){\makebox(0,0)[bl]{@{term Abs_three}}} |
|
116 \end{picture} |
|
117 \end{center} |
106 \end{center} |
118 Finally, \isacommand{typedef} asserts that @{term Rep_three} is |
107 Finally, \isacommand{typedef} asserts that @{term Rep_three} is |
119 surjective on the subset @{term three} and @{term Abs_three} and @{term |
108 surjective on the subset @{term three} and @{term Abs_three} and @{term |
120 Rep_three} are inverses of each other: |
109 Rep_three} are inverses of each other: |
121 \begin{center} |
110 \begin{center} |