menu

Return to entry

HOL_Basics_Base
HOL_Syntax_Bundles_Lattices
Predicates_Lattice
Bounded_Quantifiers
Binary_Relation_Functions
Binary_Relations_Order_Base
Functions_Base
Function_Relators
Predicate_Functions
Predicates_Order
Functions_Monotone
Reverse_Implies
Binary_Relations_Injective
Binary_Relations_Agree
Dependent_Binary_Relations
Binary_Relations_Extend
Binary_Relations_Right_Unique
Binary_Relations_Function_Evaluation
Binary_Relations_Left_Total
Binary_Relations_Function_Base
Binary_Relations_Clean_Functions
Binary_Relations_Symmetric
Binary_Relations_Reflexive
Binary_Relations_Transitive
Preorders
Partial_Equivalence_Relations
Equivalence_Relations
Binary_Relations_Antisymmetric
Partial_Orders
Restricted_Equality
Binary_Relations_Function_Composition
Binary_Relations_Function_Extend
Binary_Relations_Function_Lambda
Binary_Relations_Functions
Binary_Relations_Order
Binary_Relations_Irreflexive
Binary_Relations_Asymmetric
Binary_Relations_Surjective
Binary_Relations_Bi_Total
Binary_Relations_Bi_Unique
Functions_Injective
Binary_Relations_Connected
Binary_Relations_Wellfounded
Binary_Relation_Properties
Bounded_Definite_Description
Binary_Relations_Least
Binary_Relations_Transitive_Closure
Functions_Restrict
Wellfounded_Transitive_Recursion
Wellfounded_Recursion
Binary_Relations_Graph
Binary_Relations_Lattice
Binary_Relations_Reflexive_Closure
LBinary_Relations
Functions_Inverse
Functions_Bijection
Functions_Surjective
Function_Properties
LFunctions
Order_Functions_Base
Order_Functors_Base
Galois_Base
Galois_Relator_Base
Order_Equivalences
Half_Galois_Property
Galois_Property
Galois_Connections
Galois_Equivalences
Galois_Relator
Transport_Base
Transport_Compositions_Agree_Base
Transport_Compositions_Agree_Monotone
Transport_Compositions_Agree_Galois_Property
Transport_Compositions_Agree_Galois_Connection
Transport_Compositions_Agree_Galois_Equivalence
Galois_Equivalent
Galois
Linear_Orders
Closure_Operators
Order_Functions
Transport_Bijections
Order_Isomorphisms
Order_Functors
Strict_Partial_Orders
Strict_Linear_Orders
Wellorders
Orders
Predicates
HOL_Basics
HOL_Mem_Of
HOL_Alignment_Binary_Relations
HOL_Syntax_Bundles_Functions
HOL_Alignment_Functions
HOL_Syntax_Bundles_Orders
HOL_Alignment_Orders
HOL_Alignment_Predicates
HOL_Alignments
HOL_Algebra_Alignment_Orders
HOL_Algebra_Alignment_Galois
HOL_Algebra_Alignments
HOL_Syntax_Bundles_Base
HOL_Syntax_Bundles_Groups
HOL_Syntax_Bundles
Transport_Compositions_Agree_Galois_Relator
Transport_Compositions_Agree_Order_Equivalence
Transport_Compositions_Agree
Transport_Compositions_Generic_Base
Transport_Compositions_Generic_Galois_Property
Transport_Compositions_Generic_Monotone
Transport_Compositions_Generic_Galois_Connection
Transport_Compositions_Generic_Galois_Equivalence
Transport_Compositions_Generic_Galois_Relator
Transport_Compositions_Generic_Order_Base
Transport_Compositions_Generic_Order_Equivalence
Transport_Compositions_Generic
Transport_Compositions
Reflexive_Relator
Monotone_Function_Relator
Transport_Functions_Base
Transport_Functions_Monotone
Transport_Functions_Galois_Property
Transport_Functions_Galois_Connection
Transport_Functions_Order_Base
Transport_Functions_Galois_Equivalence
Transport_Functions_Relation_Simplifications
Transport_Functions_Galois_Relator
Transport_Functions_Order_Equivalence
Transport_Functions
Transport_Identity
Transport_Black_Box
Transport_Equality
Transport_Universal_Quantifier
Transport_Existential_Quantifier
Transport_Galois_Relator_Properties
Transport_Implies
Transport_White_Box
Transport
Transport_Rel_If
Transport_Prototype
Galois_Relator_Syntax
Transport_Dep_Fun_Rel_Examples
Transport_Lists_Sets_Examples
Transport_Partial_Quotient_Types
Transport_Typedef_Base
Transport_Typedef
Transport_Natural_Functors_Base
Transport_Natural_Functors_Galois
Transport_Natural_Functors_Galois_Relator
Transport_Natural_Functors_Order_Base
Transport_Natural_Functors_Order_Equivalence
Transport_Natural_Functors
Transport_Via_Partial_Galois_Connections_Equivalences_Paper

Transport.Transport_Compositions_Agree_Galois_Equivalence

HTML Presentation