11institutetext: 1 Nanjing University of Aeronautics and Astronautics, Jiangsu
Nanjing, China
2 School of Informatics, University of Leicester, Leicester LE1 7RH, U.K
11email<EMAIL_ADDRESS>
# Robust Ensembling Network for Unsupervised Domain Adaptation

Han Sun1(✉) Lei Lin1 Ningzhong Liu1 Huiyu Zhou2

# Robust Ensembling Network for Unsupervised Domain Adaptation

Han Sun1(✉) Lei Lin1 Ningzhong Liu1 Huiyu Zhou2

###### Abstract

Recently, in order to address the unsupervised domain adaptation (UDA)
problem, extensive studies have been proposed to achieve transferrable models.
Among them, the most prevalent method is adversarial domain adaptation, which
can shorten the distance between the source domain and the target domain.
Although adversarial learning is very effective, it still leads to the
instability of the network and the drawbacks of confusing category
information. In this paper, we propose a Robust Ensembling Network (REN) for
UDA, which applies a robust time ensembling teacher network to learn global
information for domain transfer. Specifically, REN mainly includes a teacher
network and a student network, which performs standard domain adaptation
training and updates weights of the teacher network. In addition, we also
propose a dual-network conditional adversarial loss to improve the ability of
the discriminator. Finally, for the purpose of improving the basic ability of
the student network, we utilize the consistency constraint to balance the
error between the student network and the teacher network. Extensive
experimental results on several UDA datasets have demonstrated the
effectiveness of our model by comparing with other state-of-the-art UDA
algorithms.

###### Keywords:

Unsupervised domain adaptation Adversarial learning Time ensembling

##  1 Introduction

In recent years, deep neural networks have played a particularly critical role
in the face of many computer vision tasks, such as image classification [12],
object detection [22], semantic segmentation [3] and so on. However, training
a perfect neural network demands a large amount of data and corresponding data
labeling, which is very time-consuming and expensive. When faceing a new task
or a new dataset, the previously trained model may exhibit poor performance
due to the domain shift. We hope to use available network and data to complete
the target task through knowledge transfer, where domain adaptation methods
are needed. The problem that domain adaptation figures out is how to adapt the
model trained in the source domain with rich labels to the target domain with
sparse labels, and minimize the negative transfer. Besides, UDA means that we
only have annotations on the source domain data, without the target domain.

Figure 1: Comparison between previous adversarial domain training method and
ours. (a): Before domain adaptation, the data distribution of the source
domain and the target domain are quite different. (b): The adversarial domain
training method aligns the source domain and the target domain by a domain
discriminator, and make them as close as possible to each other, which causes
the confusion of the category information. (c): Our model uses the time
ensembling algorithm to obtain a more stable network with the consistency
constraint, which effectively avoids the distribution of data samples near the
category decision boundary.

Due to the rapid development of deep learning, many approaches of deep domain
adaptation have sprung up [6][16][20]. Among them, many methods try to map the
source domain and target domain features into a high-dimensional space, and
then perform feature alignment in this space for the reduction of domain
shift. The feature alignment method generally uses Maximum Mean Discrepancy
(MMD) [2] or its improved versions. Subsequently, as a result of the bloom of
Generative Adversarial Networks (GAN) [10], the concept of adversarial
learning has also been widely employed to domain adaptation. In this way, the
domain bias between the source domain and the target domain can be effectively
reduced by adversarial learning.

The previous UDA methods such as feature alignment, adversarial learning, or
clustering methods to generate pseudo-labels for the target domain have been
relatively mature, whereas most methods rely on the features or the
predictions obtained during the network training process with loss constraint.
However, it is assumed that the network with the poor generalization ability
itself is unstable during the training process due to the insufficient data,
which can cause greater errors in the distribution of the source and target
domain features extracted by the network, and may eventually result in
disappointing performance and poor robustness of the network. Therefore, it is
particularly significant to train a more stable network. In addition, the main
popular methods often use adversarial learning. Although adversarial learning
can effectively shorten the distance between the source domain and the target
domain, it can also confuse the category information between the domains. As
shown in Fig. 1, the source domain and target domain samples get closer to
each other in the process of adversarial learning, but they also become closer
to the decision line, resulting in inaccurate classification. Consequently, we
propose a more robust network, and decrease misclassification through
consistency constraint.

In this paper, we explore a robust ensembling network for UDA, which captures
more information-rich global features through a more stable model to achieve
domain transfer. Specifically, a basic student network is applied for regular
domain adaptation training, and then another ensembling teacher network is
applied. The weight of the teacher network is the time series ensembling of
the basic student network weights, so that the teacher network not only
becames more stable, but also has more global information. The ensembling
teacher network is adopted to reversely guide the basic student network to
enhance the accuracy of its intra-domain classification. Besides, the instance
feature is combined with the prediction of the ensembling teacher network and
student network as a new condition for the domain discriminator, thereby
adversarially decreasing the difference between domains. The main contribution
points of this article are:

  * $\bullet$

This paper proposes a robust ensembling network for UDA, which can reduce the
prediction error caused by network fluctuations during the training process.
The features and predictions obtained by network during training will be more
stable with more global information, and more conducive to domain transfer.

  * $\bullet$

We employ the predictions of the ensembling teacher network to reversely
constrain the basic student network to raise the stability of the basic
student network. Besides, we use the new predictions to constitute dual-
network conditional adversarial loss and effectively alleviate the phenomenon
of negative transfer.

  * $\bullet$

The proposed network is better than its baseline CDAN[15], and it presents a
competitive result on the various UDA datasets.

##  2 Related Work

UDA has been widely studied in computer vision mainly for classification and
detection tasks. In the era of deep neural networks, the main idea of domain
adaptation is to learn domain invariant features between the source and target
domain. Among them, several methods exploit MMD [2] and its kernel variants to
minimize the difference in feature distribution. With the rise of neural
networks, [9] attempts to introduce MMD as a regularization method to minimize
the distribution mismatch between the source and target domain in the latent
space. In addition to considering the adaptive algorithm of multi-feature
representation, [29] also provides an improved conditional maximum mean error.

Recently, adversarial learning-based methods exert a tremendous fascination to
bridge the gap between the source domain and the target domain. GAN [10] is
motivated by the idea of two-play game in game theory. Adversarial training is
the process in which the generator and the discriminator compete against each
other. Adversarial learning is firstly applied to domain adaptation in [8].
Its core idea is to adopt the discriminator to learn domain invariant
features. A more general framework is proposed by [27] for adversarial domain
adaptation. The author of [15] is motivated by [19] and proposes to align
category labels by using the joint distribution of features and predictions.
Inspired by [1], [24] applies the Wasserstein GAN measurement to domain
adaptation, and proposes Wasserstein distance guided representation learning.

Semi-supervised learning uses both labeled data and unlabeled data during
training. The domain adaptation problem is similar to semi-supervised learning
in the strict sense, but the source domain and target domain have domain shift
due to various image capture devices, environmental changes, and different
styles. Initially, the application of a time series ensembling is proposed by
[13], which adopts the average of the current model prediction results and the
historical prediction results to calculate the mean square error. Different
from historically weighted sum of model predictions in [13] , [26] uses
weighted exponential moving average (EMA) on the weight of the student model.
Temporal Ensembling [13] is applied by [7] to the domain adaptation problem,
and data augmentation is implemented to increase the generalization ability of
the model. The prediction results of time ensembling is utilized as pseudo-
labels to cluster and align the feature spaces of the source domain and the
target domain in [5].

With the current adversarial domain adaptation methods, the network tends to
overlap the source domain and target domain’s category distributions during
adversarial training, resulting in poor classification results. However, the
consistency constraint of semi-supervised learning can just constrain sample
distribution and decrease classification errors. In addition, most of the
current semi-supervised learning methods in domain adaptation exploit pseudo-
label methods, but the wrong pseudo-label may mislead the training of the
network. Moreover, most of the previous methods only adopt prediction
ensembling methods, and there are few researches on the model ensembling of
[26]. Therefore, based on CDAN [15], we propose an UDA method of robust
ensembling model.

##  3 Methodology

This part we mainly provide the specific steps of the method proposed in this
article. First we introduce the overall structure of the method in this
article; then we dive deep into the loss function of each part; finally we
examines the total loss function of the network.

Figure 2: Overview of the proposed REN model. It principally comprises a
student network, a teacher network and a domain discriminator. Both the
student network and the teacher network consist of a feature extractor and a
classifier. The source and target domain samples are delivered to the student
network at the same time to extract features, and the weight of the teacher
network is the ensembling of the student network’s weights in time series.
Then, the predictions of the student and the teacher network are ensembled and
multiplied with the features of the student network to form a dual-network
conditional adversarial loss. Finally, the classification results of the two
models are considered together for consistency loss.

###  3.1 Overview

In the UDA problem, the labeled source domain is denoted as
$\mathbf{D}_{s}=\left\\{\left(\mathbf{x}_{i}^{s},y_{i}^{s}\right)\right\\}_{i=0}^{N_{s}}$,
where $\mathbf{N_{s}}$ represents the number of samples with labels in the
source domain, and the unlabeled target domain is denoted as
$\mathbf{D}_{t}=\left\\{\left(\mathbf{x}_{j}^{t}\right)\right\\}_{j=0}^{N_{t}}$,
where $\mathbf{N_{t}}$ represents the number of samples without labels in the
target domain [21]. The source domain and target domain samples conform to the
joint distribution $P_{s}\left(X^{s},Y^{s}\right)$ and
$Q_{t}\left(X^{t},Y^{t}\right)$ respectively, and $P\neq Q$. Our goal is to
train a deep neural network $\mathcal{F}:X^{t}\rightarrow Y^{t}$ using source
domain data with labels and target domain data, which can accurately predict
target domain samples while minimizing domain shift.

As shown in Fig. 2, our model mainly includes two networks, a student network
and a teacher network, and a domain discriminator $D$. Each network has a
feature extractor $F$ and a classifier $C$. Given a picture $x$, the
corresponding feature vector $f=F\left(x\right)\in\mathbb{R}^{d}$ is obtained
through the feature extractor $F$, where $d$ represents the feature dimension,
and the corresponding prediction result $p=C\left(f\right)\in\mathbb{R}^{c}$
is obtained through the classifier $C$, where $c$ represents the total number
of classes [8]. According to [8], the adversarial domain adaptation method can
be expressed as optimizing the following minimum and maximum problem:

$\min_{F,C}\max_{D}\mathcal{L}_{c}(F,C)-\lambda_{d}\mathcal{L}_{d}(F,D),$ (1)
$\mathcal{L}_{c}(F,C)=-\mathbb{E}_{\left(x_{s},y_{s}\right)\sim\left(X_{s},Y_{s}\right)}\sum_{n=1}^{N_{s}}\left[\mathbf{1}_{\left[n=y_{s}\right]}\log\left[C\left(F\left(x_{s}\right)\right)\right]\right],$
(2) $\mathcal{L}_{d}(F,D)=-\mathbb{E}_{x_{s}\sim
P_{s}}\log\left[D\left(f_{s}\right)\right]-\mathbb{E}_{x_{t}\sim
Q_{t}}\log\left[1-D\left(f_{t}\right)\right]\odot,$ (3)

Among them, $\mathcal{L}_{c}\left(F,C\right)$ is the standard supervised
classification task, which uses only the cross-entropy loss of labeled source
domain data. The domain discriminator $D$ is a two-classifier
$D:\mathbb{R}^{d}\rightarrow[0,1]$, which predicts whether the data comes from
the source domain or the target domain.

###  3.2 Robust Ensembling Network

The previous domain adaptation adversarial methods are limited to some extent
due to the problem that the model is unrobust caused by adversarial learning.
Although adversarial learning effectively narrows the distribution of the
source and target domains, it also confuses category information. The semi-
supervised learning method is mainly dedicated to finding the optimal
classification decision line. The key of these methods is to enhance the
training model with unlabeled data and cluster data points of different labels
with perturbations.

We believe that semi-supervised learning and domain adaptation have something
in common. Both semi-supervised learning and UDA are limited to the fact that
part of the data is not labeled, which makes their solutions intersect. The
only difference is that there is a distribution difference between the source
domain and the target domain in UDA, so semi-supervised learning methods can
be applied to enhance the robustness of the model and raise model prediction
accuracy. The main method used in this paper is the mean teacher method, which
contains a student network and a teacher network. The student network is
trained normally, and the weight update of the teacher network is integrated
by the time of the weight of the student network, and the update method is
exponential moving average (EMA) :

$\theta_{n}^{\prime}={\alpha_{\theta}\theta}_{n-1}^{\prime}+\left(1-\alpha_{\theta}\right)\theta_{n},$
(4)

Among them, $\theta_{n}$ represents the weight of the student model during the
$n$-th training, $\theta_{n}^{\prime}$ represents the weight of the teacher
model during the $n$-th training, and $\alpha_{\theta}$ is the smoothing
coefficient hyperparameter of the network parameter.

###  3.3 Dual-Network Conditional Adversarial Learning

The previous adversarial learning is generally limited to the labels without
the target domain, so CDAN [15] proposes to jointly consider the feature
representation and the prediction result of the classifier in the
discriminator part. CDAN believes that the outer product of the feature
representation and the prediction result can affect the feature
representation, so a discriminator shared by the source domain and the target
domain is used to align this conditional feature representation. The general
conditional adversarial loss are as follows:

$\begin{aligned}
\mathcal{L}_{d}^{con}\left(F,D\right)=-\mathbb{E}_{x_{s}~{}P_{s}}\log{\left[D\left(f_{s},p_{s}\right)\right]}-\mathbb{E}_{x_{t}~{}Q_{t}}\log{\left[1-D\left(f_{t},p_{t}\right)\right]}\end{aligned}.$
(5)

This conditional adversarial loss generally utilizes the feature $f_{s}$ and
prediction $p_{s}$ of the source domain, and also exploits the feature $f_{t}$
and prediction $p_{t}$ of the target domain. However, the features and
predictions that this adversarial loss mainly relies on are not stable, and
the two may have numerical deviations during the network training process,
which will eventually lead to the poor effect of adversarial learning. The
dual network proposed in this article can effectively avoid this problem. The
student network performs standard domain adaptation adversarial learning,
while the update of the teacher network is provided by the student network.
The update method is the former time ensembling, so that the teacher network
integrates the student network in time series, and the network structure is
more stable and robust. In addition to the student’s condition adversarial
loss, the prediction of the teacher network is also applied as another
condition.

$\displaystyle\mathcal{L}_{d}^{stu}\left(F_{stu},D\right)=-\mathbb{E}_{x_{s}~{}P_{s}}\log{\left[D\left(f_{s}^{stu},\widehat{p_{s}^{stu}}\right)\right]}$
(6)
$\displaystyle-\mathbb{E}_{x_{t}~{}Q_{t}}\log{\left[1-D\left(f_{t}^{stu},\widehat{p_{t}^{stu}}\right)\right]},$
$\displaystyle\mathcal{L}_{d}^{tea}\left(F_{stu},D\right)=-\mathbb{E}_{x_{s}~{}P_{s}}\log{\left[D\left(f_{s}^{stu},\widehat{p_{s}^{tea}}\right)\right]}$
(7)
$\displaystyle-\mathbb{E}_{x_{t}~{}Q_{t}}\log{\left[1-D\left(f_{t}^{stu},\widehat{p_{t}^{tea}}\right)\right]},$
$\widehat{p_{n}}=\left(1-\alpha_{p}\right)\\\
\widehat{p_{n-1}}+\alpha_{p}p_{n},$ (8)

Among them, $p_{n}$ represents the prediction of the student or teacher model
during the $n$-th training, $\widehat{p_{n}}$ represents the ensembling
prediction during the $n$-th training and $\alpha_{p}$ is the smoothing
coefficient hyperparameter. The prediction of the student network and the
teacher network performs an EMA operation to promote the stability of the
prediction. In this way, with global student predictions and global teacher
predictions, the network can learn more reliable conditional and transferable
information in the process of adversarial learning.

###  3.4 Consistency Constraint

The student network provides weights for the teacher network, just as student
asks the teacher in the classroom, so the teacher needs to answer the
student’s questions to help the student. Therefore, the teacher network needs
to assist the student network, and the method of assistance is to adopt
consistency constraint. The core idea of consistency constraint is to perturb
high-dimensional data so that it tends to be consistent in the feature space.
In other words, we hope that in the process of dimensionality reduction,
multiple high-dimensional data can be compressed into a low-dimensional point,
so that the feature distribution in the feature space is more compact, which
is conducive to the model learning more accurate classification decision
lines. We mainly utilize the L2 norm between the student model and the teacher
model as the consistency loss.

$\mathcal{L}_{con}=\left\|C_{stu}\left(F_{stu}\left(x\right)\right)-C_{tea}\left(F_{tea}\left(x\right)\right)\right\|_{2}.$
(9)

###  3.5 Total Loss Function

In this part, we introduce the total loss function:

$\mathcal{L}_{all}=\mathcal{L}_{c}+{\lambda_{d}^{stu}\mathcal{L}}_{d}^{stu}+{\lambda_{d}^{tea}\mathcal{L}}_{d}^{tea}+\gamma\mathcal{L}_{con},$
(10)

Therefore, the final total loss function is as described above, and it mainly
includes four parts: the supervised classification loss $\mathcal{L}_{c}$ of
source domain, a student network adversarial loss $\mathcal{L}_{d}^{stu}$, a
teacher network adversarial loss $\mathcal{L}_{d}^{tea}$ and finally the
consistency loss $\mathcal{L}_{con}$ between the student network and the
teacher network. Among them, $\lambda_{d}^{stu}$ and $\lambda_{d}^{stu}$ are
the hyperparameters of student adversarial loss and teacher adversarial loss,
and their role is to control the importance of the two in adversarial
training. $\gamma$ is the relative weight that controls the consistency
constraint.

##  4 Experiment

###  4.1 Experimental Setting

Datasets. Office-31 [23] contains 31 classes and 4,110 images collected from
three differenet domains: Amazon Website (A) with 2817 images, Web Camera (W)
with 498 images and Digital SLR Camera (D) with 795 images. By permuting the
three domains, we obtain six transfer tasks: A→W, D→W, W→D, A→D, D→A and W→A.
ImageCLEF-DA [17] is a dataset created by the ImageCLEF2014 domain adaptation
competition. We follow the guidelines of [14] and select 3 sub-domains of
Caltech-256 (C), ImageNet ILSVRC 2012 (I) and Pascal VOC 2012 (P), which have
12 common categories. There are six UDA tasks to be evaluated. Office-Home
[28] is another more challenging dataset for visual domain adaptation. It
mainly includes four dissimilar subdomains, namely Artistic images (Ar),
ClipArt (Ca), Product images (Pr) and Real-World images (Re). There are 15500
images in 65 different categories. They are all pictures under office and home
settings, which constitute a total of 12 domain adaptation tasks.

Comparisons. We compare the REN model with other state-of-the-art methods: (1)
ResNet-50 [11]. (2) Domain Adversarial Neural Network(DANN) [8]. (3)
Adversarial Discriminative Domain Adaptation (ADDA) [27]. (4) Deep transfer
learning with joint adaptation networks (JAN) [17] (5)Conditional Domain
Adversarial Network (CDAN) [15]. (6) Cluster Alignment with a Teacher for
Unsupervised Domain Adaptation (CAT) [5]. (7) Towards Discriminability and
Diversity: Batch Nuclear-norm Maximization under Label Insufficient Situations
(BNM) [4].

Implementation details. The method proposed in this paper is mainly
implemented on the Pytorch framework. For a fair comparison, we apply the same
network structure in each experiment. We utilize ResNet50 pre-trained on
ImageNet without the final fully connected layer as the feature extractor. We
adopt all the labeled data in the source domain and all the unlabeled data in
the target domain. We apply the SGD optimizer with a momentum of 0.9, the
batch size is 32, and the dimension of the bottleneck layer is set to 256. We
adopt the learning rate annealing strategy as [8]: the learning rate is
adjusted by $\eta_{p}=\eta_{0}(1+\alpha p)^{-\beta}$, where $p$ is the
training progress changing from 0 to 1, and $\eta_{0}=0.01$, $\alpha=10$,
$\beta=0.75$ are optimized by the importance-weighted cross-validation [25].
In the testing phase, we mainly choose the more stable teacher model for
testing.

###  4.2 Results

Table LABEL:tab1 shows the UDA results of the six transfer tasks of the
Office-31 dataset. We can observe that the performance of the REN method in
this paper is much better than all the previous methods on most tasks. It is
worth noting that our method REN is not only on simple transfer tasks, such as
D→W and W→D, with superior performance, reaching almost 100% accuracy, but
also on tasks that are difficult to transfer due to unbalanced samples, such
as D→A and W→A, which have achieved superior results. The main reason for the
success of our model is that we have introduced a more robust time ensembling
teacher model. The adversarial training of the student model and the teacher
model effectively solves the domain offset and enhances the predictive ability
of the model.

Table 1: Accuracy (%) on Office-31 for UDA (ResNet-50) Method | A→W | D→W | W→D | A→D | D→A | W→A | Avg
---|---|---|---|---|---|---|---
ResNet-50[11] | 68.4 | 96.7 | 99.3 | 68.9 | 62.5 | 60.7 | 76.1
DANN[8] | 82.0 | 96.9 | 99.1 | 79.7 | 68.2 | 67.4 | 82.2
ADDA[27] | 86.2 | 96.2 | 98.4 | 77.8 | 69.5 | 68.9 | 82.9
JAN[17] | 86.0 | 96.7 | 99.7 | 85.1 | 69.2 | 70.7 | 84.6
CDAN[15] | 93.1 | 98.2 | 100.0 | 89.8 | 70.1 | 68.0 | 86.6
CDAN+E[15] | 94.1 | 98.6 | 100.0 | 92.9 | 71.0 | 69.3 | 87.7
CAT[5] | 94.4 | 98.0 | 100.0 | 90.8 | 72.2 | 70.2 | 87.6
BNM[4] | 92.8 | 98.8 | 100.0 | 92.9 | 73.5 | 73.8 | 88.6
REN(Ours) | 95.0 | 99.2 | 100.0 | 94.6 | 74.1 | 74.8 | 89.6

The results of the six transfer tasks of the ImageCLEF-DA dataset are shown in
Table LABEL:tab2. Although the number of images in each subdomain in the
ImageCLEF-DA dataset is similar, it is still challenging for the transfer task
because of the images from various scenarios. Compared to ResNet-50, which
only utilizes source domain samples for fine-tuning, the above-mentioned
domain adaptation method achieves significant effect. Compared with other
methods, the method in this article has achieved significant improvement. The
CAT method also adopts the idea of semi-supervised learning, but it only
adopts the Pi-model [13] prediction ensembling method, and we utilize model
ensembling, which is more effective. This also proves that the student-teacher
model of REN can learn more transferable features.

Table 2: Accuracy (%) on ImageCLEF-DA for UDA (ResNet-50) Method | I→P | P→I | I→C | C→I | C→P | P→C | Avg
---|---|---|---|---|---|---|---
ResNet-50[11] | 74.8 | 83.9 | 91.5 | 78.0 | 65.5 | 91.2 | 80.7
DANN[8] | 75.0 | 86.0 | 96.2 | 87.0 | 74.3 | 91.5 | 85.0
JAN[17] | 76.8 | 88.0 | 94.7 | 89.5 | 74.2 | 91.7 | 85.8
CDAN[15] | 76.7 | 90.6 | 97.0 | 90.5 | 74.5 | 93.5 | 87.1
CDAN+E[15] | 77.7 | 90.7 | 97.7 | 91.3 | 74.2 | 94.3 | 87.7
CAT[5] | 77.2 | 91.0 | 95.5 | 91.3 | 75.3 | 93.6 | 87.3
REN(Ours) | 79.8 | 93.3 | 97.3 | 91.5 | 76.8 | 94.8 | 88.9
Table 3: Accuracy (%) on Office-Home for UDA (ResNet-50)

| Ar | Ar | Ar | Cl | Cl | Cl | Pr | Pr | Pr | Rw | Rw | Rw |
---|---|---|---|---|---|---|---|---|---|---|---|---|---
Method | ↓ | ↓ | ↓ | ↓ | ↓ | ↓ | ↓ | ↓ | ↓ | ↓ | ↓ | ↓ | Avg
| Cl | Pr | Rw | Ar | Pr | Rw | Ar | Cl | Rw | Ar | Cl | Pr |
ResNet-50[11] | 34.9 | 50.0 | 58.0 | 37.4 | 41.9 | 46.2 | 38.5 | 31.2 | 60.4 | 53.9 | 41.2 | 59.9 | 46.1
DANN[8] | 45.6 | 59.3 | 70.1 | 47.0 | 58.5 | 60.9 | 46.1 | 43.7 | 68.5 | 63.2 | 51.8 | 76.8 | 57.6
JAN[17] | 45.9 | 61.2 | 68.9 | 50.4 | 59.7 | 61.0 | 45.8 | 43.4 | 70.3 | 63.9 | 52.4 | 76.8 | 58.3
CDAN[15] | 49.0 | 69.3 | 74.5 | 54.4 | 66.0 | 68.4 | 55.6 | 48.3 | 75.9 | 68.4 | 55.4 | 80.5 | 63.8
CDAN+E[15] | 50.7 | 70.6 | 76.0 | 57.6 | 70.0 | 70.0 | 57.4 | 50.9 | 77.3 | 70.9 | 56.7 | 81.6 | 65.8
BNM[4] | 52.3 | 73.9 | 80.0 | 63.3 | 72.9 | 74.9 | 61.7 | 49.5 | 79.7 | 70.5 | 53.6 | 82.2 | 67.9
REN(Ours) | 54.4 | 73.6 | 77.4 | 61.6 | 71.1 | 71.7 | 61.0 | 52.2 | 78.8 | 73.1 | 59.4 | 83.5 | 68.2

Table LABEL:tab3 shows the results of 12 transfer tasks on the Office-Home
dataset. Different from the first two datasets, there are more categories in
the Office-Home dataset, thus leads to the methods which perform well on the
Office-31 dataset may have performance degradation on the Office-Home dataset.
Although the method in this paper only has the best effect on 5 transfer
tasks, the average accuracy is even better than BNM method. The main reason
for this is that the sample size of some categories in Office-Home is
extremely unbalanced. For example, the Ruler class in the Art subdomain has
only 15 pictures, while the Bottle class has 99 pictures. The main problem
that the BNM method solves is this kind of imbalance. Though the method in
this paper does not focus on the imbalance of the dataset, due to the
stability of the dual network and the ensembling teacher network, the final
classification result is not much different from that of BNM. In addition, our
method is more effective on difficult tasks such as Ar→Cl, Pr→Cl and Rw→Cl,
which are improved by 2.1%, 2.7% and 5.8% respectively than BNM. The above
experiments prove the effectiveness of our method.

###  4.3 Ablation Study and Visualization

Table 4: Accuracy (%) in ablation experiments for REN based on CDAN on Office-31 Method | A→W | D→W | W→D | A→D | D→A | W→A | Avg
---|---|---|---|---|---|---|---
CDAN | 93.1 | 98.2 | 100.0 | 89.8 | 70.1 | 68.0 | 86.6
CDAN+M | 93.3 | 98.9 | 100.0 | 92.7 | 71.5 | 73.0 | 88.3
CDAN+M+D | 94.8 | 99.0 | 100.0 | 93.7 | 72.2 | 74.5 | 89.0
CDAN+M+D+C(REN) | 95.0 | 99.2 | 100.0 | 94.6 | 74.1 | 74.8 | 89.6

Table LABEL:tab4 presents ablation experiments on Office-31 dataset based on
CDAN. In this table, we denote performing in mean teacher model ensembling
as“M”, dual-network conditional adversarial loss as “D” and consistency
constraint as “C”. On Office-31, CDAN+M outperforms CDAN by 1.7%. In addition,
compared with CDAN, CDAN+M+D and CDAN+M+D+C improve its accuracy by 2.4%, 3%,
indicating the effectiveness of our method.

(a) W→A (Office-31)

(b) P→I (ImageCLEF-DA)

Figure 3: Comparison of stablility of CDAN, student network and teacher
network of our model REN. Obviously, the blue line (teacher network) is much
smoother and more stable than the red line (student network).

In order to demonstrate the stability of the method in the training process,
we present the results of the classification accuracy of different training
processes in Fig. 3. The graph on the left shows the experimental results of
task W→A (Office-31), and the right presents the results of task P→I
(ImageCLEF-DA). We can find that the accuracy of both the student network and
the teacher network in this article is much higher than the result of CDAN. By
observing Fig. 3 carefully, we can find that the accuracy curve of the teacher
network has less fluctuations than the student network, and the accuracy has
also been improved compared with CDAN. In addition, the reason why the
accuracy of the student network is also excellent is that the consistency
constraint of the teacher network promotes the improvement of the prediction
result of the student network. Therefore, according to the curve comparison
between CDAN and Teacher Network(Ours), our method has less fluctuation and
more stability.

In addition, compared to CDAN, our method is composed of student network and
teacher network. It can be seen from Table LABEL:tab5 that the parameters of
our method is twice that of CDAN during training, and the training time is
relatively longer.

Table 5: Comparison of parameters with CDAN in the training phase on Office-31(12k epoches) Method  |  Params |  Time
---|---|---
CDAN |  24M |  1.3h
REN(Ours) |  48M |  1.8h

###  4.4 Ablation Study and Visualization

(a) Before training

(b) CDAN

(c) REN

(d) Before training

(e) CDAN

(f) REN

Figure 4: The t-SNE visualization of A→W(Office-31). (a)(b)(c)represent
category information and each color denotes a class.(d)(e)(f)Red circles are
the source samples while blue circles are the target samples.

To present the process of domain adaptation training more intuitively, we
utilize the t-distribution Stochastic Neighbour Embedding (t-SNE) [18] method
to visualize the low-dimensional changes of features before and after
adaptation in Fig. 4. We implement one task, namely A→W (Office-31) to perform
these experiments. Obviously, before training, the spatial distribution of the
source domain and target domain features is completely different. This
indicates that the distribution contains no discernible intrinsic structure.
Although after CDAN, most of data has been aggregated, there are still some
classes indistinguishable. But after our method, the feature distribution
shows a clear clustered structure. The cluster centers of the distribution are
closer than before, and the degree of dispersion is more similar. This means
that our method greatly improves the distribution in the feature space.

##  5 Conclusion

We propose a robust ensembling network for UDA based on model time ensembling
and consistency constraint. It solves the negative transfer problem of target
domain samples, which is close to the edge of the decision line due to
adversarial learning. At the same time, the dual-network conditional
adversarial loss proposed in this paper effectively decreases the instability
in the adversarial learning process, and enables the network to learn more
global transferable features. All-round experiments illustrate that our method
is superior to the current mainstream methods on various domain adaptation
datasets.

## References

  * [1] Arjovsky, M., Chintala, S., Bottou, L.: Wasserstein generative adversarial networks. In: International Conference on Machine Learning. pp. 214–223. PMLR (2017)
  * [2] Borgwardt, K.M., Gretton, A., Rasch, M.J., Kriegel, H.P., Schölkopf, B., Smola, A.J.: Integrating structured biological data by kernel maximum mean discrepancy. Bioinformatics 22(14), e49–e57 (2006)
  * [3] Chen, L.C., Papandreou, G., Kokkinos, I., Murphy, K., Yuille, A.L.: Deeplab: Semantic image segmentation with deep convolutional nets, atrous convolution, and fully connected crfs. IEEE Transactions on Pattern Analysis and Machine Intelligence 40(4), 834–848 (2017)
  * [4] Cui, S., Wang, S., Zhuo, J., Li, L., Huang, Q., Tian, Q.: Towards discriminability and diversity: Batch nuclear-norm maximization under label insufficient situations. In: Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition. pp. 3941–3950 (2020)
  * [5] Deng, Z., Luo, Y., Zhu, J.: Cluster alignment with a teacher for unsupervised domain adaptation. In: Proceedings of the IEEE/CVF International Conference on Computer Vision. pp. 9944–9953 (2019)
  * [6] Duan, L., Tsang, I.W., Xu, D.: Domain transfer multiple kernel learning. IEEE Transactions on Pattern Analysis and Machine Intelligence 34(3), 465–479 (2012)
  * [7] French, G., Mackiewicz, M., Fisher, M.: Self-ensembling for visual domain adaptation. In: International Conference on Learning Representations (2018)
  * [8] Ganin, Y., Ustinova, E., Ajakan, H., Germain, P., Larochelle, H., Laviolette, F., Marchand, M., Lempitsky, V.: Domain-adversarial training of neural networks. The Journal of Machine Learning Research 17(1), 2096–2030 (2016)
  * [9] Ghifary, M., Kleijn, W.B., Zhang, M.: Domain adaptive neural networks for object recognition. In: Pacific Rim International Conference on Artificial Intelligence. pp. 898–904. Springer (2014)
  * [10] Goodfellow, I.J., Pouget-Abadie, J., Mirza, M., Xu, B., Warde-Farley, D., Ozair, S., Courville, A., Bengio, Y.: Generative adversarial networks. arXiv preprint arXiv:1406.2661 (2014)
  * [11] He, K., Zhang, X., Ren, S., Sun, J.: Deep residual learning for image recognition. In: Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition. pp. 770–778 (2016)
  * [12] Krizhevsky, A., Sutskever, I., Hinton, G.E.: Imagenet classification with deep convolutional neural networks. Advances in Neural Information Processing Systems 25, 1097–1105 (2012)
  * [13] Laine, S., Aila, T.: Temporal ensembling for semi-supervised learning. arXiv preprint arXiv:1610.02242 (2016)
  * [14] Long, M., Cao, Y., Wang, J., Jordan, M.: Learning transferable features with deep adaptation networks. In: International Conference on Machine Learning. pp. 97–105. PMLR (2015)
  * [15] Long, M., CAO, Z., Wang, J., Jordan, M.I.: Conditional adversarial domain adaptation. Advances in Neural Information Processing Systems 31 (2018)
  * [16] Long, M., Wang, J., Ding, G., Sun, J., Yu, P.S.: Transfer joint matching for unsupervised domain adaptation. In: Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition. pp. 1410–1417 (2014)
  * [17] Long, M., Zhu, H., Wang, J., Jordan, M.I.: Deep transfer learning with joint adaptation networks. In: International Conference on Machine Learning. pp. 2208–2217. PMLR (2017)
  * [18] Van der Maaten, L., Hinton, G.: Visualizing data using t-sne. Journal of Machine Learning Research 9(11) (2008)
  * [19] Mirza, M., Osindero, S.: Conditional generative adversarial nets. arXiv preprint arXiv:1411.1784 (2014)
  * [20] Pan, S.J., Tsang, I.W., Kwok, J.T., Yang, Q.: Domain adaptation via transfer component analysis. IEEE Transactions on Neural Networks 22(2), 199–210 (2010)
  * [21] Pan, S.J., Yang, Q.: A survey on transfer learning. IEEE Transactions on Knowledge and Data Engineering 22(10), 1345–1359 (2009)
  * [22] Ren, S., He, K., Girshick, R., Sun, J.: Faster r-cnn: towards real-time object detection with region proposal networks. IEEE Transactions on Pattern Analysis and Machine Intelligence 39(6), 1137–1149 (2016)
  * [23] Saenko, K., Kulis, B., Fritz, M., Darrell, T.: Adapting visual category models to new domains. In: European Conference on Computer Vision. pp. 213–226. Springer (2010)
  * [24] Shen, J., Qu, Y., Zhang, W., Yu, Y.: Wasserstein distance guided representation learning for domain adaptation. In: Proceedings of the AAAI Conference on Artificial Intelligence. vol. 32 (2018)
  * [25] Sugiyama, M., Krauledat, M., Müller, K.R.: Covariate shift adaptation by importance weighted cross validation. Journal of Machine Learning Research 8(5) (2007)
  * [26] Tarvainen, A., Valpola, H.: Mean teachers are better role models: Weight-averaged consistency targets improve semi-supervised deep learning results. Advances in Neural Information Processing Systems 30 (2017)
  * [27] Tzeng, E., Hoffman, J., Saenko, K., Darrell, T.: Adversarial discriminative domain adaptation. In: Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition. pp. 7167–7176 (2017)
  * [28] Venkateswara, H., Eusebio, J., Chakraborty, S., Panchanathan, S.: Deep hashing network for unsupervised domain adaptation. In: Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition. pp. 5018–5027 (2017)
  * [29] Zhu, Y., Zhuang, F., Wang, J., Chen, J., Shi, Z., Wu, W., He, Q.: Multi-representation adaptation network for cross-domain image classification. Neural Networks 119, 214–221 (2019)


The usual homogeneous form of equality type in Martin-Löf Type
Theory contains identifications between elements of the same
type. By contrast, the heterogeneous form of equality contains
identifications between elements of possibly different types. This
paper introduces a simple set of axioms for such types. The axioms
are equivalent to the combination of systematic elimination rules
for both forms of equality, albeit with typal (also known as
“propositional”) computation properties, together with Streicher's
Axiom K, or equivalently, the principle of uniqueness of identity

§ INTRODUCTION

Equality types in the intensional version of Martin-Löf Type
Theory <cit.> are
traditionally formulated in terms of an introduction rule
(reflexivity) together with a rule for eliminating proofs of equality
and a rule describing how elimination computes when it meets a
reflexivity proof. Some recent work
<cit.> on models of Homotopy Type
Theory <cit.> uses a formulation of equality types that differs
from this in two respects. First, the elimination operation is
replaced by the combination of a simple operation for transporting
elements along proofs of equality, together with an axiom asserting
contractibility of singleton types. Secondly, the analogue of the
computation rule for the eliminator, namely that transporting along a
reflexivity proof does nothing, is weakened from a judgemental
equality to the existence of an element of the corresponding equality
type; see <cit.> and Figure 2 in
<cit.>.  This formulation is sometimes called a
“propositional” equality type <cit.>, but here I
will follow <cit.> for the reasons given
there and refer to typal equality types.  Although these
changes to the formulation of equality types affect computation, it
seems that they do not change what is provable (see
<cit.> for example) and they make it easier to
construct models. Furthermore, they can lead to surprising
simplifications. For example, Lumsdaine [private communication] has
observed that the computation rule is superfluous (for elimination,
but the observation also holds for transport): if a proto-identity
type has a transport operation lacking its typal computation property,
then the operation can be corrected to a new one that does have the
computation property (see Lemma <ref> and the Appendix).

[0]

Axioms for typal heterogeneous equality satisfying Axiom K

[2]– the derived homogeneous equality

Axioms for $\Sigma$-types with surjective pairing

[2]– concrete syntax for ∑-types

The Axioms

The above remarks apply to the usual, homogeneous notion of equality
in which elements of the same type are compared. The purpose of this
paper is to give an analogous treatment of heterogeneous
equality <cit.> in the presence of
$\Sigma$-types and the Axiom K of
<cit.>.  Since Axiom K is not
compatible with the Univalence Principle of Homotopy Type
Theory <cit.>, the focus here is on the simpler
(but still useful!) world of zero-dimensional type theory.  We will
see that the axioms in Fig. <ref> capture homogeneous and
heterogeneous equality satisfying their usual dependent elimination
and (typal) computation properties and Axiom K, and $\Sigma$-types
with their usual dependent elimination and (typal) computation
properties.  It seems necessary to include $\Sigma$-types in order to
get Lumsdaine's result mentioned above (see Remark <ref>);
the axioms we give for such types are standard, except that the
equality property of dependent second projection (spr) is
simplified by the use of heterogeneous rather than homogeneous
equality. The axioms in the figure are pleasingly simple compared to
the usual formulation in terms of elimination and computation
properties, and may aid finding new models of heterogeneous equality

The implementation of intensional Martin-Löf Type Theory provided by
Agda 2.6 <cit.> is used to state the axioms and develop their
properties. More precisely, we just make use of Agda's implementation
of a countably infinite, non-cumulative hierarchy of universes
$\atyp{Set}\,\AgdaBound{l}$, where $\AgdaBound{l}$ ranges
over a type $\atyp{Level}$ of universe levels whose closed normal
forms are in bijection with the natural numbers. The universes are
closed under dependent function types (written in Agda as
$(\aarg{x}:\aarg{A})\fun\aarg{B}\,$) and inductive types.  The use of
a whole hierarchy of universes is necessary; for example, the function
$\afun{eqt}$ in Fig. <ref> takes a heterogeneous equality
type $\aarg{x}\heq\aarg{y}$ in universe $\afun{Set}\,\aarg{l}$ and
produces a homogeneous one $\aarg{A}\eq\aarg{B}$ in the universe one
level up, which is denoted $\afun{Set}(\afun{lsuc}\,\aarg{l})$ in
Agda. We also use Agda's notation for infix and for implicit
arguments. For example, the function $\_{\heq}\_$ in
Fig. <ref> takes five arguments, the first three of which
are implicit and the last two of which are infix. In particular,
Agda's ability to infer the values of implicit arguments (or of
unspecified explicit arguments, which are denoted by an underscore,
$\,\_\,$) is used quite aggressively in what follows, in order to be
able to see the wood from the trees.

Although the code in this paper has been checked by Agda, some parts
of it that are not essential for understanding the development have
been hidden; the complete (non-literate) Agda code can be found
at [<https://doi.org/10.17863/CAM.47902>].

§ THE AXIOMS AND THEIR PROPERTIES

Figure <ref> postulates a family of types $\_{\heq}\_$ in
all universes, together with some operations on them that together
capture a typal version of heterogeneous
equality. Heterogeneous equality types were introduced by
<cit.> under the name of “John Major
equality”. Unlike ordinary, homogeneous equality types, such a type
$\aarg{x}\heq\aarg{y}$ relates elements $\aarg{x}$ and $\aarg{y}$ of
possibly different types, $\aarg{A}$ and $\aarg{B}$ say. The intention
is that elements of type $\aarg{x}\heq\aarg{y}$ denote proofs that not
only are $\aarg{x}$ and $\aarg{y}$ equal, but so also are their types
$\aarg{A}$ and $\aarg{B}$. The figure defines homogeneous equality
$\_{\eq}\_$ as the special case of $\_{\heq}\_$ when the types of the
two arguments are already known to be the same.  Axiom $\afun{rfl}$
says that $\eq$ is reflexive. Axiom $\afun{ctr}$ is a heterogeneous
version of the contractibility property of singleton types
(cf. $\mathsf{center}$ in Figure 2 of
<cit.>). Axiom $\afun{eqt}$ says that heterogeneously
equal things have (homogeneously) equal types. Axiom $\afun{tpt}$ is a
form of the transport property of equality (cf. $\mathsf{T}$ in
Figure 2 of <cit.>) involving both homogeneous and
heterogeneous equalities. Finally, $\afun{∑}$, $\_\afun{,}\_$,
$\afun{fst}$, $\afun{snd}$, $\afun{fpr}$, $\afun{spr}$ and
$\afun{eta}$ axiomatize dependent product types satisfying surjective

Equational reasoning for heterogeneous equality

We begin with some simple lemmas establishing the basics of equational
logic for $\heq$, namely chain-reasoning using reflexivity (already an
axiom), symmetry, transitivity and congruence properties. These are
given in Fig. <ref>.

The axioms in Fig. <ref> are notably lacking a
“regularity” property for $\afun{tpt}$, that is, a proof of type
\eq \aarg{z}$. But such a thing is needed if we are to derive the
expected elimination and (typal) computation rules for $\_{\heq}\_$
and $\_{\eq}\_$. To get those, one can define a “corrected” form of
transport that has this regularity property, using a simplified
version of a trick due to Peter Lumsdaine [unpublished]. In fact, it
is enough to produce a function coercing proofs of equality of types
$\aarg{e}:\aarg{A}\eq\aarg{B}$ into functions
$\afun{coe}\,\aarg{e} : \aarg{A}\fun\aarg{B}$ and which satisfies the
heterogeneous regularity property that
$\afun{coe}\,\aarg{e}\,\aarg{x} \heq \aarg{x}$ (so that, given how we
define $\eq$ in terms of $\heq$, the usual form of regularity,
$\afun{coe}\,(\afun{rfl}\,\aarg{A})\,\aarg{x} \eq \aarg{x}$, is just
the special case of this when $\aarg{e}$ is $\afun{rfl}\,\aarg{A}$).

The axioms in Fig. <ref> imply the existence of a coercion

satisfying a heterogeneous regularity property:

First we define the type of
functions that are injective with respect to $\eq$ and note that the
identity function is one such:

[0]

Next we use $\afun{tpt}$ to define a function coercing equalities into
injective functions:

The injectiveness of $\afun{icoe}\,\aarg{e}$ is used as follows. Applying the operation
$\afun{tpt}$ to the type family

we can transport the element
$(\aarg{e}\,,\,\afun{rfl}\, (\afun{fst}\,
(\afun{icoe}\,(\afun{rfl}\,\aarg{A}))\, \aarg{x})$ of type
$\afun{fsticoe}\,\aarg{x}\,\aarg{A}\,(\afun{rfl}\,\aarg{A})$ along
$\aarg{e}:\aarg{A}\eq\aarg{B}$ and
$\afun{ctr}\,\aarg{e}:\afun{rfl}\,\aarg{A}\heq \aarg{e}$ to give an
element of type $\afun{fsticoe}\,\aarg{x}\,\aarg{B}\,\aarg{e}$.  The
first projection of this element gives the value of the desired
coercion along $\aarg{e}$ at $\aarg{x}\,$:

and its second projection can
be used along with the injectiveness property of $\afun{icoe}$ to get
the regularity property of this coercion:

An immediate corollary is that the axioms imply the uniqueness
of identity proofs (UIP) and hence Streicher's
Axiom K <cit.>. (We will see in Sect. <ref>
that in fact it is only the $\afun{tpt}$ function that contains an
implicit use of Axiom K.)

The axioms in Fig. <ref> imply that $\eq$ satisfies

[0]

Using the functions from Fig <ref> and Lemma <ref> we have:

The elimination and computation properties of $\eq$ and $\heq$ then

The axioms in Fig. <ref> imply that $\eq$ has the usual
elimination and (typal) computation properties of homogeneous
equality (in the form suggested by <cit.>)

The axioms also imply that $\heq$ has the elimination and (typal)
computation properties of heterogeneous equality described by

[0]

Using the functions from Fig <ref> and Lemma <ref> we have:

Note that a corollary of the above two theorems is that $\_\heq\_$ is
uniquely determined up to logical equivalence by the axioms in
Fig. <ref>. In other words, for any other such family of
types $\_\heq'\_\,$, there are functions in either direction between
$\aarg{x}\heq\aarg{y}$ and $\aarg{x}\heq'\aarg{y}\,$; and because of UIP
these are necessarily mutually inverse up to $\heq$ (or $\heq'$).

$\afun{≡≡Elim}$ is the elimination form systematically
derived <cit.> from $\_\heq\_$ and $\afun{rfl}$,
regarding them as the formation and introduction rules for an
inductive type. As <cit.> points out,
$\afun{≡≡Elim}$ is not very useful, because of the way it's motive
$\aarg{P}$ involves abstraction over an arbitrary type
$\aarg{B}$. McBride goes on to give another, more useful form of
elimination for $\heq$, but in our setting where $\eq$ is a special
case of $\heq$, that coincides with the eliminator $\afun{≡Elim}$.

One of the strengths of machine-checked mathematics is that it aids
the detection of logical dependency. Although we included the
equations $\afun{fpr}$, $\afun{spr}$ and $\afun{eta}$ for
$\Sigma$-types in Fig. <ref>, they have not been used
for the results so far, as may be verified by commenting them out
from this literate Agda file and re-checking it up to this point.

So only the weak form of dependent product given by $\afun{∑}$,
$\_\afun{,}\_$, $\afun{fst}$ and $\afun{snd}$ in the figure is used
to define the regular version of coercion in Lemma <ref>
and then prove Theorems <ref> and <ref>. It
would be nice if there was some way to define $\afun{∑}$,
$\_\afun{,}\_$, $\afun{fst}$ and $\afun{snd}$ just using dependent
function types and universes.

However, the extra equations $\afun{fpr}$, $\afun{spr}$ and
$\afun{eta}$ for $\afun{∑}$ are of course very natural. Let us
record the fact that they enable one to define the usual elimination
rule for dependent products, with a typal computation rule:
∑Elim ∑Comp

[0]

§ CONSISTENCY OF THE AXIOMS

We have seen that the axioms in Fig. <ref> suffice to
define dependent products and both heterogeneous and homogeneous
equality types with uniqueness of identity proofs, all satisfying the
usual elimination properties, albeit with typal computation
rules. Conversely it is not hard to see that the elimination
and computation rules in Theorem <ref> and
Remark <ref>, together with Axiom K, imply the axioms in
Fig. <ref>. Instead of doing that, in this section we just
check that the axioms are provable from inductive definitions of
equality and dependent product types.  One can make these inductive
definitions in Agda as follows:

[0]

[2]– – without this ≡≡ would have to land in Set (lsuc l)

[2]– {-# NOUNIVERSECHECK #-}

[2]– the derived homogeneous equality

Then Agda's implementation of dependent pattern matching enables
straightforward definitions of the functions from
Fig. <ref>, as follows:

[0]

[0]

[0]

[0]

[0]

Since we know from the previous section that these functions entail
Axiom K, the above definitions have to use Agda's default
option to switch the existing implementation of
dependent pattern matching <cit.> back to the original
version due to <cit.>, which is known to imply
Axiom K <cit.>. More precisely, it is only the matches
on the two occurrences of the pattern
$\AgdaInductiveConstructor{rfl}\,\_$ in the definition of $\afun{tpt}$
that involve an implicit use of Axiom K (to discharge the unification
constraints $\aarg{A}\mathrel{≐}\aarg{A}$ and
$\aarg{B\,x}\mathrel{≐}\aarg{B\,x}$); all the other functions can be
defined without Axiom K.

§ CONCLUSION

This paper has investigated heterogeneous equality and produced a
simple collection of axioms for its typal form, in the spirit
of <cit.>. The point of view is foundational. From a
practical perspective, the use of heterogeneous equality has much to
recommend it for formalizing mathematics in dependent type theory when
assuming uniqueness of identity proofs[Such is the approach
of Lean <cit.> since version 3, for example.]; but that is
another story.

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

[Agda WikiAgda Wiki[n.d.]]
authorpersonAgda Wiki.

[Altenkirch, McBride, and SwierstraAltenkirch
et al2007]
authorpersonT. Altenkirch, personC.
McBride, and personW. Swierstra.
Observational equality, now!. In
booktitlePLPV '07: Proceedings of the 2007 Workshop on
Programming Languages Meets Program Verification. publisherACM,
addressNew York, NY, USA, pages57–68.

[Backhouse, Chisholm, Malcolm, and
SaamanBackhouse et al1989]
authorpersonR. Backhouse, personP.
Chisholm, personG. Malcolm, and personE. Saaman.
Do-it-Yourself Type Theory.
journalFormal Aspects of Computing
volume1 (year1989), pages19–84.

[Bezem, Coquand, and HuberBezem
et al2014]
authorpersonM. Bezem, personT. Coquand,
and personS. Huber. year2014.
A Model of Type Theory in Cubical Sets. In
booktitle19th International Conference on Types for Proofs
and Programs (TYPES 2013) (seriesLeibniz International
Proceedings in Informatics (LIPIcs)),
editorpersonR. Matthes and
personA. Schubert (Eds.), Vol. volume26.
publisherSchloss Dagstuhl–Leibniz-Zentrum fuer Informatik,
addressDagstuhl, Germany, pages107–128.

[Boulier and WinterhalterBoulier and
authorpersonS. Boulier and personT.
Winterhalter. year2019.
titleWeak Type Theory is Rather Strong.
(dateJune year2019).
Abstract for the 25th International Conference on Types for Proofs
and Programs (TYPES 2019), Oslo, Norway.

[Cockx and AbelCockx and Abel2018]
authorpersonJ. Cockx and personA. Abel.
Elaborating Dependent (Co)Pattern Matching.
journalProc. ACM Program. Lang.
volume2, numberICFP, Article articleno75
(dateJuly year2018), numpages30 pages.

[Cohen, Coquand, Huber, and MörtbergCohen
et al2018]
authorpersonC. Cohen, personT. Coquand,
personS. Huber, and personA. Mörtberg.
Cubical Type Theory: A Constructive Interpretation
of the Univalence Axiom. In booktitle21st International
Conference on Types for Proofs and Programs (TYPES 2015)
(seriesLeibniz International Proceedings in Informatics
(LIPIcs)), editorpersonT. Uustalu (Ed.),
Vol. volume69. publisherSchloss
Dagstuhl–Leibniz-Zentrum fuer Informatik, addressDagstuhl,
Germany, pages5:1–5:34.

authorpersonT. Coquand.
Pattern Matching with Dependent Types. In
booktitleProceedings of the 1992 Workshop on Types for
Proofs and Programs, Båstad, Sweden,
editorpersonB. Nordström,
personK. Petersson, and personG. D. Plotkin
(Eds.). pages66–79.

authorpersonT. Coquand.
titleEquality and Dependent Type Theory.
(dateFeb. year2011).
A talk given for the 24th AILA meeting, Bologna
(<http://www.cse.chalmers.se/ coquand/bologna.pdf>).

[Goguen, McBride, and McKinnaGoguen
et al2006]
authorpersonH. Goguen, personC. McBride,
and personJ. McKinna. year2006.
Eliminating Dependent Pattern Matching.
In booktitleAlgebra, Meaning, and Computation:
Essays dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday,
editorpersonK. Futatsugi, personJ.-P.
Jouannaud, and personJ. Meseguer (Eds.).
publisherSpringer Berlin Heidelberg, addressBerlin,
Heidelberg, pages521–540.

authorpersonC. McBride.
titleDependently Typed Functional Programs and their
thesistypePh.D. Dissertation. schoolUniversity
of Edinburgh.

[Nordström, Petersson, and
SmithNordström et al1990]
authorpersonB. Nordström, personK.
Petersson, and personJ. M. Smith.
booktitleProgramming in Martin-Löf's Type
publisherOxford University Press.

authorpersonChr. Paulin-Mohring.
Inductive definitions in the system Coq; rules
and properties. In booktitleTyped Lambda Calculus and
Applications (seriesLecture Notes in Computer Science),
editorpersonM. Bezem and personJ. F.
Groote (Eds.), Vol. volume664.
publisherSpringer-Verlag, Berlin, pages328–345.

authorpersonM. Shulman.
Brouwer's Fixed-Point Theorem in Real-Cohesive
Homotopy Type Theory.
journalMathematical Structures in Computer Science
volume28 (year2018), pages856–941.

authorpersonT. Streicher.
titleInvestigations into Intensional Type Theory.
Habilitation Thesis. schoolLudwig Maximilian University,

[The Lean Theorem ProverThe Lean Theorem
authorpersonThe Lean Theorem Prover.

[Univalent Foundations ProgramUnivalent
Foundations Program2013]
authorpersonThe Univalent Foundations Program.
booktitleHomotopy Type Theory: Univalent Foundations
for Mathematics.
addressInstitute for Advanced Study.

[van den Bergvan den Berg2018]
authorpersonB. van den Berg.
Path Categories and Propositional Identity Types.
journalACM Trans. Comput. Logic
volume19, number2 (dateJune
year2018), pages15:1–15:32.

§ APPENDIX: TYPAL HOMOGENEOUS EQUALITY WITHOUT K

In this appendix, for completeness sake we consider axioms in
dependent type theory without Axiom K for
homogeneous equality types

following <cit.>. (Since without Axiom K heterogeneous
equality is not very useful, we do not bother to consider axiomatizing
$\heq$ in that setting.)  One of the axioms makes use of dependent product
types. Although one could axiomatize those types as we did in the main
part of the paper, it is simpler to use an inductive defintion and
corresponding pair patterns:

[2]– concrete syntax for ∑-types

[2]– dependent product projections

The axioms for homogeneous equality are

Coquand also considers a regularity axiom for $\afun{sbst}$
($\mathsf{ax}_3$ in loc.cit.), but one can do without that by
using Peter Lumsdaine's trick to correct $\afun{sbst}$ to a version
$\afun{subst}$ for which there is a proof
$\afun{substIsRegular} : \forall\aarg{b} \fun
\afun{subst}\,(\afun{refl}\,\aarg{x})\,\aarg{b} \eq \aarg{b}$, as
follows. The proof begins as for Lemma <ref> by
considering functions that are injective modulo $\eq$:

[0]

[0]

But then to construct $\afun{subst}$ and $\afun{substIsRegular}$, one
has to work a bit harder than in the proof of the lemma, because of
the lack of uniqueness of identity proofs:

[0]

[0]