HOL_Basics_Base

Binary_Relation_Functions

Binary_Relations_Order_Base

Binary_Relations_Lattice

Functions_Base

HOL_Syntax_Bundles_Lattices

Predicates_Lattice

Function_Relators

Predicates_Order

Predicates

Functions_Monotone

Binary_Relations_Reflexive

Binary_Relations_Symmetric

Binary_Relations_Transitive

Binary_Relations_Order

Binary_Relations_Antisymmetric

Binary_Relations_Injective

Binary_Relations_Irreflexive

Binary_Relations_Left_Total

Binary_Relations_Right_Unique

Binary_Relations_Surjective

Binary_Relation_Properties

Preorders

Partial_Equivalence_Relations

Equivalence_Relations

Partial_Orders

Restricted_Equality

LBinary_Relations

Functions_Injective

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

Galois

Closure_Operators

Order_Functions

Order_Functors

Orders

HOL_Basics

HOL_Mem_Of

HOL_Syntax_Bundles_Relations

HOL_Alignment_Binary_Relations

HOL_Syntax_Bundles_Functions

HOL_Alignment_Functions

HOL_Syntax_Bundles_Orders

HOL_Alignment_Orders

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_Base

Transport_Bijections

Transport_Compositions_Agree_Base

Transport_Compositions_Agree_Monotone

Transport_Compositions_Agree_Galois_Property

Transport_Compositions_Agree_Galois_Connection

Transport_Compositions_Agree_Galois_Equivalence

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

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_Rel_If

Transport_Prototype

Transport_Syntax

Transport_Dep_Fun_Rel_Examples

Transport_Lists_Sets_Examples

Transport_Partial_Quotient_Types

Transport_Typedef_Base

Transport_Typedef

Transport_Via_Partial_Galois_Connections_Equivalences_Paper