Index - P
| pairMapCong | Type.Family.Tuple |
| parFst | Data.Type.Conjunction |
| parSnd | Data.Type.Conjunction |
| permute | Data.Type.Product |
| permute' | Data.Type.Product |
| Pos | Type.Family.Nat |
| ppMatrix | Data.Type.Vector |
| ppMatrix' | Data.Type.Vector |
| ppVec | Data.Type.Vector |
| Pred | Type.Family.Nat |
| pred' | Data.Type.Nat |
| predCong | Type.Family.Nat |
| prj | Data.Type.Sum |
| Prod | Data.Type.Product, Data.Type.Subset |
| Proven | Type.Class.Witness |
| pureC | Type.Class.Witness |