Index - I
| Id | Type.Function |
| idIsFun | Type.Function |
| idLemma | Type.Function |
| Image | |
| 1 (Type/Class) | Type.Function |
| 2 (Data Constructor) | Type.Function |
| imageCod | Type.Function |
| imageEmpty | Type.Function |
| imageGraphList | Type.Function |
| imageMonotonic | Type.Function |
| imageOfInclusion | Type.Function |
| imageUnion | Type.Function |
| image_Preimage | Type.Function |
| Incl | |
| 1 (Type/Class) | Type.Function |
| 2 (Data Constructor) | Type.Function |
| inclusionIsFun | Type.Function |
| inclusion_Injective | Type.Function |
| inCod | Type.Function |
| inDom | Type.Function |
| Initor | Type.Nat |
| initorFun | Type.Nat |
| InitorS | Type.Nat |
| InitorZ | Type.Nat |
| Injective | |
| 1 (Type/Class) | Type.Function |
| 2 (Data Constructor) | Type.Function |
| injective | Type.Function |
| injective_Inv | Type.Function |
| insert | Type.Set.Example |
| IntegralType | |
| 1 (Type/Class) | Type.Set |
| 2 (Data Constructor) | Type.Set |
| Inter | |
| 1 (Type/Class) | Type.Set |
| 2 (Data Constructor) | Type.Set |
| interFst | Type.Set |
| interIdempotent | Type.Set |
| interMaximal | Type.Set |
| Inters | |
| 1 (Type/Class) | Type.Set |
| 2 (Data Constructor) | Type.Set |
| interSnd | Type.Set |
| intInExampleSet | Type.Set.Example |
| introToTyCon | Type.Function |
| Inv | |
| 1 (Type/Class) | Type.Function |
| 2 (Data Constructor) | Type.Function |
| invId | Type.Function |
| invInv | Type.Function |
| invInv0 | Type.Function |
| IsFun | Type.Function |
| isFun_congruence | Type.Function |
| IsS | Type.Nat |
| IsZ | Type.Nat |