Skip to content

Instantly share code, notes, and snippets.

@ncfavier

ncfavier/seminar20201020_TT-intro-06-family_model.agda

Created December 22, 2024 16:09
Show Gist options
  • Save ncfavier/6ca209ab691f640a8d08e9f67bd041e1 to your computer and use it in GitHub Desktop.
Save ncfavier/6ca209ab691f640a8d08e9f67bd041e1 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
seminar20201020_TT-intro-06-family_model.agda
-- A = 𝟘 β†’ πŸ™
-- Pierce's law does not hold in the family model: we have (A β‡’ βŠ₯) β‰… βŠ₯,
-- hence ((A β‡’ βŠ₯) β‡’ A) β‰… ⊀, hence (((A β‡’ βŠ₯) β‡’ A) β‡’ A) β‰… A, but there is
-- no term of type A.
notPierce : Tm β‹„ (((A β‡’ βŠ₯) β‡’ A) β‡’ A) β†’ 𝟘
notPierce (aβ‚€ , a₁) = a₁ tt tt _ (Ξ» aβ‚‚ _ β†’ aβ‚‚ tt)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment