Le implicazioni (funzione) sono più fondamentali di quanto diciamo congiunzione (prodotto) nella teoria del tipo?

Question

Secondo la risposta a (Come definire il tipo di funzione in AGDA) Il tipo di funzione è una specie di cosa fondamentale in AGDA e necessario per il bootstrap, quindi l'utente finale non può definirlo come quello che fanno per il tipo di congiunzione (prodotto) e deve essere predefinito a livello di lingua. Ciò significa che il tipo di implicazione (funzione) è più fondamentale di tipi come il prodotto (congiunzione) poiché la funzione viene utilizzata nella definizione di tali tipi?