Transport

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_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_White_Box

Transport

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_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