EF.Categories

• Locally Preordered Bicategories
• Pseudofunctor
• Pseudonatural Transformations
• Biadjoint Biequivalence

EF.Triposes

• Pre-Heyting Algebras
  • Definition
  • Morphisms
• Reflection-Based Triposes
  • Definition
  • Morphisms
  • Categories Trip_int / Trip_ext
• Set-Based Triposes
  • Definition
  • Morphisms
  • Categories of Set-Bases Triposes
• Reflection-Based Tripos and Set-Based Tripos with Reflective Surjective Substitutions Equivalence
  • PseudoFunctor
  • Biadjoint biequivalence

EF.EvidencedFrames

• Evidenced Frames
  • Definition
  • Morphisms

EF.ImplicativeAlgebras

• Partial Orders
• Properties related to the lattice structure
• Tactics
• Other properties
• Definition VI.2 : Implicative Structures
  • Properties of implicative structures
• Encoding the λ-calculus
  • Application
  • Abstraction
• Definition VI.3 - Implicative Algebras
  • Properties
  • S (λxyz.xy(zy)
  • Entailment
• Definition VI.10 - Categories IA_int / IA_ext

EF.EFTriposEquivalence

• UFam : from Evidenced Frames to Triposes
  • Definition
  • Functoriality of UFam
• RAS: from Triposes to Evidenced Frames
  • Definition
  • Functoriality of RAS
• UFam <-> RAS Units/Counits
  • Natural Transformation: Id => UFam ∘ RAS
  • Natural Transformation: UFam ∘ RAS ⇒ Id
  • Natural Transformation: Id ⇒ RAS ∘ UFam
  • Natural Transformation: RAS ∘ UFam ⇒ Id
  • Biadjoint Biequivalence: EF ≊ Trip
• Theorem V.13: Equivalence of Evidenced Frames and Set-Based Triposes

EF.EFIAEquivalence

• UEF: From Implicative Algebras to Evidenced Frames
  • Definition
  • Functoriality of UEF
• FIA: from Evidenced Frames to Implicative Algebras
  • Definition
  • Functoriality of FIA
• Equivalence btw IA_ext and EF_ext
  • φ defines an IA-morphism: FIA (UEF (IA))→ IA
  • inv defines an IA-morphism: IA → FIA(UEF(IA))
  • Biadjoint Biequivalence : IA_ext ≊ EF_ext