Category Theory For Beginners: Internal Language of a Topos (Mitchell-Bénabou Language)
In this video we introduce the Mitchell-Benabou Language. Also known as the internal language of a topos. This language allows use to manipulate statements that look like those from set theory and logic, while actually talking about the much more general case of topos theory and topos logic (and topos logic basically looks like intuitionistic logic). In this video we introduce the formal rules behind the Mitchell-Benabou Language. We start by looking at the rules for building terms and interpreting them in the topos. We explain how terms with a type equal to the subobject classifier (formulas) have `extensions' corresponding to the subobjects they classify, and we explain how notation like that of lambda calculus can be used to discuss arrows involving exponential objects. We also discuss term interpretation. Next we apply the Mitchell-Benabou Language to topos logic. We explain how we can use the Mitchell-Benabou Language to say a formula is true, or to say that one formula implies another. We also discuss the idea of sequents (which are claims that formulas imply other formulas), and discuss how we denote chains of implication starting from a given sequent. We use this notation to describe the different term manipulation rules which are sound and complete for topos logic, and justify the rules using our understanding of topos theory. We also go through examples of proofs of statements in topos logic using the manipulation rules we have obtained within the Mitchell-Benabou Language.
Here are some videos including further proofs and discussions about particular topics:
Implications of implication 1
• Implications of implication 1
Understanding False and Not
• Understanding False and Not
Universal Quantification Proof
• Universal Quantification Proof
False in the Mitchell-Benabou Language
• False in the Mitchell-Benabou Language
Not in the Mitchell-Benabou Language
• Not in the Mitchell-Benabou Language
The proof of Theorem 13.6 (about implication) can be found in this video:
Mclarty Topos Basics 1
• Mclarty Topos Basics 1
More information about how "there exists" works can be found here
Existential quantifier interpretation
• Existential quantifier interpretation
The following videos give important practice in using the Mitchell-Benabou Language to formulate important notions:
Completing Equalizers with MBL
• Completing Equalizers with MBL
Finding all subobjects containing something
• Finding all subobjects containing som...
Proof that the MBL OR rule works
• Proof that the MBL OR rule works
Proof that the MBL EXISTS rule works
• Proof that the MBL EXISTS rule works
A proof of Theorem 13.9 can be found here
"Universal Quantification Proof"
• Universal Quantification Proof
Substitution Lemma argument
• Substitution Lemma argument
Substitution rule proof
• Substitution rule proof
Substitution and equality
• Substitution and equality
Substitution and equality 2
• Substitution and equality 2
Equality, biconditionality, reasoning
• Equality, biconditionality, reasoning
(a or b) and (not a) implies b
• (a or b) and (not a) implies b
Singleton and comprehension axioms
• Singleton and comprehension axioms
Axiom of extensionality proof
• Axiom of extensionality proof
Product axioms
• Product axioms
Correction at 6:06:39
The purple expression at the far bottom left should be the extension of (exists y.Y) phi [rather than just being the extension of phi].
Lots of good applications of MBL are in the following series on "From the MBL to the topos"
• From the MBL to the topos 1
• From the MBL to the topos 2
• From the MBL to the topos 3
• From the MBL to the topos 4
• From the MBL to the topos 5
• From the MBL to the topos 6
• From the MBL to the topos 7
• From the MBL to the topos 8
• From the MBL to the topos 9
• From the MBL to the topos 10
• From the MBL to the topos 11 replacem...
• From the MBL to the topos 12
• From the MBL to the topos 13
• From the MBL to the topos 14
• From the MBL to the topos 15
• From the MBL to the topos 16
• From the MBL to the topos 17
• From the MBL to the topos 18
• From the MBL to the topos 19
• From the MBL to the topos 20
coequalizer documents and videos
https://drive.google.com/open?id=17OO...
• Coequalizers for structured sets
• Coequalizers for structured sets 2
• Coequalizers for structured sets 3
• Coequalizers for structured sets 4
Power objects and equivalence relations
• Power objects and equivalence relations
Watch video Category Theory For Beginners: Internal Language of a Topos (Mitchell-Bénabou Language) online without registration, duration hours minute second in high quality. This video was added by user Richard Southwell 30 May 2021, don't forget to share it with your friends and acquaintances, it has been viewed on our site 4,805 once and liked it 107 people.