# SLVideo: A Sign Language Video Moment Retrieval Framework

Gonçalo Vinagre Martins, Afonso Quinaz, Carla Viegas, Sofia Cavaco, João
Magalhães  NOVA School of Science and TechnologyLisboaPortugal gv.martins,
<EMAIL_ADDRESS>s.cavaco<EMAIL_ADDRESS>
(2018)

###### Abstract.

Sign Language Recognition has been studied and developed throughout the years
to help the deaf and hard-of-hearing people in their day-to-day lives. These
technologies leverage manual sign recognition algorithms, however, most of
them lack the recognition of facial expressions, which are also an essential
part of Sign Language as they allow the speaker to add expressiveness to their
dialogue or even change the meaning of certain manual signs. SLVideo is a
video moment retrieval software for Sign Language videos with a focus on both
hands and facial signs. The system extracts embedding representations for the
hand and face signs from video frames to capture the language signs in full.
This will then allow the user to search for a specific sign language video
segment with text queries, or to search by similar sign language videos. To
test this system, a collection of five hours of annotated Sign Language videos
is used as the dataset, and the initial results are promising in a zero-shot
setting. SLVideo is shown to not only address the problem of searching sign
language videos but also supports a Sign Language thesaurus with a search by
similarity technique.

Project web page: https://novasearch.github.io/SLVideo/

Sign Language Recognition, Video Moment Retrieval.

††copyright: acmlicensed††journalyear: 2018††doi: XXXXXXX.XXXXXXX††conference:
Make sure to enter the correct conference title from your rights confirmation
emai; June 03–05, 2018; Woodstock, NY††isbn: 978-1-4503-XXXX-X/18/06 Figure 1.
SLVideo is a video moment retrieval framework that is prepared to index and
search sign-language content by focusing on the hand, hand-positions and
facial signs.

##  1\. Introduction

In their everyday life, deaf and hard-of-hearing people have to face the
challenge of talking to hearing people who don’t know sign language. Writing
is not always a solution, because the ”writing language” is like a whole
different language to deaf people, so it works as a second language. The
emergence of Sign Language Recognition technologies helps to solve this
problem and can support video moment retrieval tasks over sign language
videos. Users will then be able to submit a natural language query regarding a
video and the system must return the appropriate video segment that
corresponds to the query.

Figure 2. SLVideo workflow follows six steps: (1) the initial page allows
users to choose whether the search will be embedding-based or transcripts,
whether it will search for a facial expression or a phrase, and to write and
submit the query; (2) next, SLVideo presents the videos which have one or more
segments corresponding with the query, allowing the user to choose a video and
go to the next step (3) where it is shown all the video segments, from the
chosen video. After selecting a particular video segment, (4) a modal will
open with the video segment. The user can then (5) edit the annotations of
that video segment, or (6) go to the sign-language thesaurus.

A Sign Language Recognition software has to support the recognition of non-
manual signs, which include facial expressions and head and shoulder
movements, because they are an essential aspect of sign language, due to their
grammatical and expressive functions in the dialogue. Facial expressions,
specifically, can distinguish what type of phrase is being said, add intensity
to what is being said, and even change the meaning of a manual sign (Silva and
Costa, 2017).

Despite the importance of facial expressions in communication through sign
language, most of the approaches for Sign Language Recognition focus on hand
gestures and put facial expressions as a low-priority research, as in (Cheng
et al., 2023). This is a concerning fact because the system will lose
linguistic information that is present in the facial signs. For a video moment
retrieval task with sign language videos, the lack of facial expression
recognition could lead to a wrong video segment being returned for a query
where the facial expression has an important role.

With SLVideo, we aim to support video moment retrieval systems where the user
can search for a sign through a text query and get a set of the relevant video
segments corresponding to that query. For this, we are using a five-hour
collection of annotated Portuguese Sign Language videos, focusing on the signs
that include a facial expression. SLVideo is agnostic of the video encoder and
we provide a proof-of-concept with two CLIP (Radford et al., 2021) encoders
for embedding generation and three different techniques for processing the
extracted video frames. This system also includes a sign-language thesaurus
for the user to search for signs that are similar in terms of gestures and
facial signs. Finally, we also support the edition of the video sign-language
annotations.

##  2\. Video and Annotations Formats

To demonstrate SLVideo, we used a dataset with more than five hours of video
footage featuring people talking in Portuguese Sign Language. Each video is a
time-ordered sequence of images that depict the performance of a sign. These
signs can be either manual or non-manual and convey a collection of words
which compose a phrase.

SLVideo supports videos of any format with or without Sign Language
transcriptions/annotations. We use video annotations in the EAF annotation
format but other formats are easily supported. The EAF annotation format (Max
Planck Institute for Psycholinguistics, The Language Archive, 2023) supports
complex annotations for video and audio recordings, primarily used in
linguistic research, i.e., ”an annotation can be a sentence, word or gloss, a
comment, translation or a description of any feature observed in the media”.
111https://www.mpi.nl/tools/elan/EAF_Annotation_Format.pdf

The EAF file of each video is composed of several annotations, being either
timely aligned to the video or it can refer to another annotation. The timely
aligned annotations have a start and end timestamp associated with them and
can be a literal translation of the signs executed in the video to a written
form in Portuguese or a translation to a gloss annotation in Portuguese. The
annotations referring to other ones are defined as symbolic associations,
since they give more information about the annotation it is referring to, such
as the type of phrase that is being said and the grammatical class of the
gloss annotations.

##  3\. UX Design Overview

Currently, there is a ready-to-use user interface as illustrated in figure 2.
The system allows the user to search for a facial expression, using the ground
truth or four types of embedding-based search: searching by base frames
embeddings, by the average of the frames embeddings, by the best frame
embedding, or by the annotations’ embeddings. A phrase can also be searched,
but, for now, only using the ground truth. The search results are divided by
videos, with each video showing the number of matches it has with the query,
and when selecting a video it will display the video segments, from the best
to the worst similarity, so that the user can watch the video segment
referring to one of the results by selecting it and can also cycle through the
retrieved video segments.

##  4\. System Architecture

The architecture of SLVideo comprises distinct modules, each assigned with a
specific task. These tasks consist of how the video will be indexed and
processed, how the annotations will be used, and how the queries will be
interpreted.

###  4.1. Video Processing

The annotations in the EAF file are the input of a parser that outputs a more
readable annotations file, in order to have only the relevant information and
to have all the annotations have a start and end timestamp, contrary to the
EAF file where only some annotations had those timestamps. After this parsing,
the video information is analysed more easily.

With the parsed annotations file, it is possible to know the start and end
timestamps of every sign with a facial expression. The frames within those
timestamps are classified as keyframes, so all of them are extracted. The
extraction is done using FFmpeg, an open-source software used for video and
audio manipulation. After extracting the frames, a cropping and background
removal process will be applied to them to only have the person.

Figure 3. SLVideo Moment Retrieval System.

Current Video Moment Retrieval System

###  4.2. Frame Embeddings Generation

The generation of embeddings from the video and from the dataset annotations
allows the system to support an embedding-based search. The system was tested
using two CLIP models, the clip-ViT-B-32, which is the image and text model
CLIP, and the CAPIVARA(Santos et al., 2023), which is optimized for texts
written in Portuguese. Both of these models receive a frame or annotation as
input and generate its embeddings. Receiving text as a query, its embeddings
can be generated to perform an embedding-based search, using the same CLIP
model.

###  4.3. Facial Signs Embeddings

We extend the capabilities of the existing CLIP model by incorporating a
specialized version tailored for Portuguese Sign Language (PSL). This enhanced
model leverages the CLIPER(Li et al., 2023) framework, which builds on CLIP
but is fine-tuned to handle more specific and complex tasks, such as
recognizing detailed facial expressions and full-body gestures in PSL.

The standard CLIP model, specifically clip-ViT-B-32, maps text and images to a
shared vector space, facilitating the generation of embeddings from both
modalities. However, this generic model does not adequately capture the
intricacies of PSL, which includes not just manual signs but also essential
non-manual signals like facial expressions and body movements.

To address this limitation, we propose the use of a modified CLIPER-like
approach. This involves training the model specifically on a dataset
comprising annotated PSL videos. This specialized training enables the model
to generate more accurate and expressive embeddings for PSL gestures, taking
into account the full range of non-manual signals.

In this enhanced setup, the text encoder is also adapted to better align with
the linguistic characteristics of PSL. By using datasets tailored for PSL,
such as gloss annotations and natural language descriptions of sign language
videos, the text encoder can generate more contextually relevant embeddings.
This ensures that the text queries match more precisely with the visual
content of PSL videos.

###  4.4. Indexing Embedding Vectors and Annotations

To make the extracted information from the videos searchable through a query
given by the user, OpenSearch is a good solution, being an open-source search
and analytics suite that allows the user to search, insert, analyse, and
visualize data. The information retrieved from the Portuguese Sign Language
videos and annotations can be seen as documents that are indexed in
OpenSearch, allowing the use of its full-text search capabilities to retrieve
these documents.

| Primeiro | Rir | Ter
---|---|---|---
Base | Average | Best | Base | Average | Best | Base | Average | Best
No Cropping or Background Removal | clip-ViT-B-32 | 0.14 | 0.29 | 0.14 | 0.0 | 0.0 | 0.0 | 0.33 | 0.0 | 0.33
CAPIVARA | 0.0 | 0.0 | 0.0 | 0.75 | 1.0 | 0.57 | 0.33 | 0.33 | 0.33
Cropping but no Background Removal | clip-ViT-B-32 | 0.14 | 0.14 | 0.43 | 0.25 | 0.25 | 0.25 | 0.33 | 0.33 | 0.33
CAPIVARA | 0.0 | 0.0 | 0.0 | 0.5 | 0.5 | 0.25 | 0.0 | 0.0 | 0.0
Cropping and Background Removal | clip-ViT-B-32 | 0.43 | 0.43 | 0.29 | 0.0 | 0.0 | 0.0 | 0.33 | 0.0 | 0.33
CAPIVARA | 0.0 | 0.0 | 0.0 | 0.0 | 0.25 | 0.0 | 0.0 | 0.0 | 0.0
Annotations | clip-ViT-B-32 | 1.0 | 0.5 | 0.33
CAPIVARA | 1.0 | 1.0 | 1.0
Table 1. Results for searching for the words ”Primeiro” (first), ”Rir” (laugh)
and ”Ter” (have) using the three techniques of frame embedding-based search,
the three methods of processing the extracted frames and the annotations
embeddings search. The metric used in these results is Recall, measuring the
proportion of relevant video segments that were retrieved.

###  4.5. Query Processing

The queries the user provides are text-only, and the querying process can be
done using the query plain text or its generated embeddings. In the case of
text embeddings-based search, the embeddings must be generated using the same
model used for generating the frames and annotations embeddings, in order to
make them comparable.

###  4.6. Supported Workflows

SLVideo supports two key workflows, Figure 3: a pre-processing and indexing
phase, which is executed when the system starts, and a querying phase, which
is executed every time a query is done. It also includes a thesaurus,
annotation rating and edition.

####  4.6.1. Pre-Processing and Indexing

The system starts by parsing the Portuguese Sign Language video annotations in
the EAF files to make them more easily analyzed, then uses those annotations’
information to extract the keyframes using FFmpeg. Currently, the keyframes
are all frames where it is being executed a sign with a facial expression, so
all of these are extracted. Every extracted keyframe will be cropped using the
DETR-ResNet-50(Carion et al., 2020) model so that it becomes a smaller image
with only the person in the frame, and then the background will be removed
using the RMBG-1.4.

With the extracted key frames, embeddings are generated for all of the
annotated facial expressions, using the chosen CLIP model, either clip-
ViT-B-32 or CAPIVARA. Four types of embeddings are generated: base frames
embeddings, where only embeddings from selected frames are generated and then
summed together, with the selection being made by calculating a step size and
selecting frames at intervals of this step size; average frames embeddings,
where all frames embeddings are generated and its average is saved as that
facial expression embedding; best frame embeddings, where only the best frame
embedding is saved for each facial expression, comparing the generated
embeddings by the norm of the embedding vectors; annotations’ embeddings,
where the embeddings for all the facial expressions annotations’ values are
generated and saved.

All of this information will be indexed in a document, to be used by
OpenSearch, composed of the video and annotation IDs and the four types of
embeddings generated for that facial expression.

####  4.6.2. Querying

The queries created by the user will be text-based, searching for a facial
expression or phrase in the Portuguese Sign Language videos. When querying
using the ground truth, the provided text is used to search for
correspondences in the annotations files, returning all the matching
annotations.

When performing an embedding-based search, the query embeddings are generated,
also using CLIP, and they are used to search in OpenSearch for the
corresponding document, returning the ten matches with the best similarity
score with the provided query and its embeddings, which is calculated using
cosine similarity.

####  4.6.3. Thesaurus and User’s Annotations

Despite the video moment retrieval task being the most focused task of this
system, SLVideo also includes a thesaurus and the ability for the users to
edit and evaluate the existing annotations.

When selecting a video segment, the user might be interested to know signs
that are performed similarly to the one it was retrieved. The thesaurus
fulfills that request, by retrieving the selected video segment’s embeddings
previously generated and searching, using OpenSearch, for similar videos using
those embeddings.

It is also useful to constantly improve the dataset to enhance the CLIP model.
This can be done by allowing the users to rate the retrieved video segments
and also edit the existing annotations. To guarantee the rating and editions
reliability, this would only be available to professional annotators and sign
language speakers.

##  5\. Experiences and Results

This system is evaluated based on the retrieved video segments regarding the
query given by the user, whether it returns the correct video segments or not,
being recall the most important metric, as it measures the proportion of
relevant video segments that are retrieved. The relevant video segments are
known by retrieving them from the ground truth, that is by using the query
plain text to search for the desired results directly from the video
annotations.

When the search is embedding-based, the retrieved video segments will have
associated with them a similarity score based on the cosine similarity between
the query embeddings and the chosen search method embeddings. Those similarity
scores were not satisfying, as for every video segment the score is in an
interval of [0.56, 0.59], which is not accurate as the correct video segments
should have a higher similarity score.

As demonstrated in table 1, to test the system we queried for the words
”Primeiro” (first), ”Rir” (laugh) and ”Ter” (have) using embedding-based
search with Base Frames Embeddings, Average Frames Embeddings and Best Frames
Embeddings. For both CLIP models, we did three different tests, one where the
extracted frames are given as it is, one where the extracted frames are
cropped to have only the person, and one where the extracted frames are
cropped and the background is removed. We also tested the usage of
Annotations’ Embeddings.

We can see that the results vary a lot depending on how the extracted frames
are processed and that both CLIP models have similar results. We believe that
this is because the used models are not trained specifically for this problem,
as they are a generic image and text model and are not focused on facial
expression or Portuguese Sign Language interpretation. It’s important to note
that when using these non-fine-tuned models, this task becomes a zero-shot
task, so, despite initial appearances, the results are quite satisfactory for
certain cases as it retrieves a good amount of relevant video segments
regarding the given query. As for searching using the Annotation’s Embeddings,
we can see that CAPIVARA retrieve better results than clip-ViT-B-32, as it is
a model focused on the Portuguese language.

##  6\. Conclusion

In this paper, we proposed SLVideo, a system to search Sign Language content.
The key contributions are:

  * •

Sign-Language Video Moment Retrieval: SLVideo is one of the first video search
frameworks to support hand and facial signs with an embedding-based
architecture.

  * •

Support for modular Sign-Language Encoders: The two different encoders that we
used to extract video embeddings, demonstrate the modularity of SLVideo.

  * •

Proof of concept demonstration: Using a dataset of annotated videos, the
system allows users to search for specific signs through text queries.

Future improvements will focus on enhancing model accuracy to better support
communication for deaf and hard-of-hearing individuals.

## References

  * (1)
  * Carion et al. (2020) Nicolas Carion, Francisco Massa, Gabriel Synnaeve, Nicolas Usunier, Alexander Kirillov, and Sergey Zagoruyko. 2020.  End-to-End Object Detection with Transformers.  _CoRR_ abs/2005.12872 (2020).  arXiv:2005.12872 https://arxiv.org/abs/2005.12872
  * Cheng et al. (2023) Yiting Cheng, Fangyun Wei, Jianmin Bao, Dong Chen, and Wenqiang Zhang. 2023.  CiCo: Domain-Aware Sign Language Retrieval via Cross-Lingual Contrastive Learning. In _Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR)_. 19016–19026.
  * Li et al. (2023) Hanting Li, Hongjing Niu, Zhaoqing Zhu, and Feng Zhao. 2023.  CLIPER: A Unified Vision-Language Framework for In-the-Wild Facial Expression Recognition.  arXiv:2303.00193 [cs.CV]
  * Max Planck Institute for Psycholinguistics, The Language Archive (2023) Max Planck Institute for Psycholinguistics, The Language Archive. 2023.  _ELAN (Version 6.7)_.  https://archive.mpi.nl/tla/elan Nijmegen: Max Planck Institute for Psycholinguistics, The Language Archive.
  * Radford et al. (2021) Alec Radford, Jong Wook Kim, Chris Hallacy, Aditya Ramesh, Gabriel Goh, Sandhini Agarwal, Girish Sastry, Amanda Askell, Pamela Mishkin, Jack Clark, Gretchen Krueger, and Ilya Sutskever. 2021.  Learning Transferable Visual Models From Natural Language Supervision. In _Proceedings of the 38th International Conference on Machine Learning_ _(Proceedings of Machine Learning Research, Vol. 139)_ , Marina Meila and Tong Zhang (Eds.). PMLR, 8748–8763.  https://proceedings.mlr.press/v139/radford21a.html
  * Santos et al. (2023) Gabriel O. dos Santos, Diego A. B. Moreira, Alef I. Ferreira, Jhessica Silva, Luiz Pereira, Pedro Bueno, Thiago Sousa, Helena Maia, Nádia da Silva, Esther Colombini, Helio Pedrini, and Sandra Avila. 2023.  CAPIVARA: Cost-Efficient Approach for Improving Multilingual CLIP Performance on Low-Resource Languages. In _Workshop on Multi-lingual Representation Learning (MRL), Conference on Empirical Methods in Natural Language Processing (EMNLP)_.
  * Silva and Costa (2017) Emely Silva and Paula Costa. 2017.  Recognition of Non-Manual Expressions in Brazilian Sign Language.  _12th IEEE International Conference on Automatic Face and Gesture Recognition_.


$\Theta^{\mathtt{Tm}}_{\Delta}:\mathtt{Tm}^{f}\left(\Delta.A[\sigma],\operatorname{\mathsf{isContr}}(Y)\right)\rightarrow\mathtt{Tm}^{f}\left(\Delta,\operatorname{\mathsf{isContr}}(\Theta_{\Delta}^{\mathtt{Ty}}(Y))\right).$

In other words, if $Y$ is contractible, then so is
$\Theta^{\mathtt{Ty}}_{\Gamma}(Y)$.

######  Remark 4.18.

This does not represent a _direct_ translation of the internal definition;
rather, it can be seen as a _universe-free_ adaptation of it. In Definition
2.13, the quantification is over specific types within a particular universe.
Externally, we can express it in terms of _all types_. Consequently, the
external version holds slightly more strength.

The naturality conditions give the following: In Figure 6, all vertical arrows
are context substitutions. When the commutative sides are appropriately
composed, the top and bottom isomorphisms are equal, which can be expressed as
the cube “commuting”. In Figure 7, the vertical arrows are context
substitutions, and the square is commutative.

${{\mathtt{Ty}^{f}(\Delta.A[\sigma])}}$${\mathtt{Ty}^{f}(\Delta)}$${{\mathtt{Ty}^{e}(\Delta.A[\sigma])}}$${\mathtt{Ty}^{e}(\Delta)}$${{\mathtt{Ty}^{f}(\Upsilon.A[\sigma\circ\tau])}}$${\mathtt{Ty}^{f}(\Upsilon)}$${{\mathtt{Ty}^{e}(\Upsilon.A[\sigma\circ\tau])}}$${\mathtt{Ty}^{e}(\Upsilon)}$$\scriptstyle{\Theta^{\mathtt{Ty}}_{\Delta}}$$\scriptstyle{\mathcal{c}_{\Delta.A[\sigma]}}$$\scriptstyle{\mathcal{c}_{\Delta}}$$\scriptstyle{\prod^{e}(A[\sigma],\\_)}$$\scriptstyle{\Theta^{\mathtt{Ty}}_{\Upsilon}}$$\scriptstyle{\mathcal{c}_{\Upsilon.A[\sigma\circ\tau]}}$$\scriptstyle{\mathcal{c}_{\Upsilon}}$$\scriptstyle{\prod^{e}(A[\sigma\circ\tau],\\_)}$
Figure 6: Naturality condition for $\Theta^{\mathtt{Ty}}$, where
$\sigma:\Delta\rightarrow\Gamma$ and $\tau:\Upsilon\rightarrow\Delta$ in
$\mathcal{C}$.
${{\mathtt{Tm}^{f}\left(\Delta.A[\sigma],\operatorname{\mathsf{isContr}}(Y)\right)}}$${{\mathtt{Tm}^{f}\left(\Delta,\operatorname{\mathsf{isContr}}(\Theta_{\Delta}^{\mathtt{Ty}}(Y))\right)}}$${{\mathtt{Tm}^{f}\left(\Upsilon.A[\sigma\circ\tau],\operatorname{\mathsf{isContr}}(Y[\tau])\right)}}$${{\mathtt{Tm}^{f}\left(\Upsilon,\operatorname{\mathsf{isContr}}(\Theta_{\Upsilon}^{\mathtt{Ty}}(Y[\tau]))\right)}}$$\scriptstyle{\Theta^{\mathtt{Tm}}_{\Delta}}$$\scriptstyle{\Theta^{\mathtt{Tm}}_{\Upsilon}}$
Figure 7: Naturality condition for $\Theta^{\mathtt{Tm}}$, where
$\sigma:\Delta\rightarrow\Gamma$ and $\tau:\Upsilon\rightarrow\Delta$ in
$\mathcal{C}$.

##  5 Models with cofibrant exo-nat

In the following definition, recall that all products exist in the category of
sets.

######  Definition 5.1.

Let $(\mathcal{C},\mathtt{Ty},\mathtt{Tm})$ be a CwF with enough type formers.
We say $\mathcal{C}$ has _exo-nat products_ if there is a map
$\Omega_{\Gamma}:\prod_{\mathbf{N}}\mathtt{Ty}(\Gamma)\rightarrow\mathtt{Ty}(\Gamma)$,
where $\mathbf{N}$ is the external natural numbers, such that for any
$Y:\prod_{\mathbf{N}}\mathtt{Ty}(\Gamma)$ we have

  * 1)

the set $\mathtt{Tm}(\Gamma,\Omega_{\Gamma}(Y))$ is isomorphic to the
categorical product of the sets $\mathtt{Tm}(\Gamma,Y_{a})$ for each
$a:\mathbf{N}$, namely, we have

${{\mathtt{Tm}^{f}(\Gamma,\Omega_{\Gamma}(Y))}}$${\cong}$${{\prod_{a:\mathbf{N}}\mathtt{Tm}^{f}(\Gamma,Y_{a})}}$$\scriptstyle{\phi}$$\scriptstyle{\psi}$

  * 2)

if $d,c:\prod_{a:\mathbf{N}}\mathtt{Tm}(\Gamma,Y_{a})$ are such that there is
a term in the type $\operatorname{\mathsf{Id}}(d_{a},c_{a})$ as being terms of
$Y_{a}:\mathtt{Ty}(\Gamma)$, then there is a term in the type
$\operatorname{\mathsf{Id}}(\psi(d),\psi(c))$ as being terms of
$\Omega_{\Gamma}(Y)$,

and all these are natural in $\Gamma$.

In simpler terms, the first requirement stated in Definition 5.1 ensures that
$\prod^{e}_{a:\mathbb{N}^{e}}Y(a)$ has a fibrant match, while the second
requirement ensures that the $\operatorname{\mathsf{funext}}$ for cofibrant
exo-types holds.

######  Example 5.2.

Let $\mathcal{C}$ be a good model category [11]. Define $\mathtt{Ty}(\Gamma)$
as the set of fibrations over $\Gamma$ (with suitable coherence conditions
[12]). Define for $A:\mathtt{Ty}(\Gamma)$ the set $\mathtt{Tm}(\Gamma,P)$ as
the hom-set $\nicefrac{{\mathcal{C}}}{{\Gamma}}[\Gamma,\Gamma.A]$.

Since $\mathtt{Ty}(\Gamma)$ is closed under countable products, we can take
$\Omega_{\Gamma}(Y):=\prod_{a:\mathbf{N}}Y_{a}$, and there is a clear
bijection between
$\nicefrac{{\mathcal{C}}}{{\Gamma}}[\Gamma,\Omega_{\Gamma}(Y)]$ and
$\prod_{a:\mathbf{N}}(\nicefrac{{\mathcal{C}}}{{\Gamma}}[\Gamma,Y_{a}])$, the
first requirement in Definition 5.1 holds.

Suppose $d,c:\prod_{a:\mathbf{N}}\mathtt{Tm}(\Gamma,Y_{a})$ are such that
there is a term in the type $\operatorname{\mathsf{Id}}(d_{a},c_{a})$ as being
terms of $Y_{a}:\mathtt{Ty}(\Gamma)$. In that model, it means $d_{a}$ and
$c_{a}$, as being maps $\Gamma\rightarrow Y_{a}$, are right homotopic. That
is, there are maps $p_{a}:\Gamma\rightarrow{Y_{a}}^{I}$ such that the
following diagram commutes:

${{{Y_{a}}^{I}}}$${\Gamma}$${{{Y_{a}}\times{Y_{a}}}}$$\scriptstyle{p_{a}}$

.

Since $Y_{a}$ is fibrant (as being in the slice category) and $\Gamma$ is
cofibrant (as being an object of a good model category), by a standard lemma
(Corollary 1.2.6 in [9]), we have $d_{a}$ and $c_{a}$ are also left homotopic.
Namely, the following diagram commutes:

${\Gamma+\Gamma}$${{Y_{a}}}$${\Gamma^{\prime}}$

where $\Gamma^{\prime}$ is a cylinder object for $\Gamma$ fixed for all
$a:\mathbf{N}$. This induces a left homotopy between $d$ and $c$, namely, we
have:

${\Gamma+\Gamma}$${{\prod_{a:\mathbf{N}}Y_{a}}}$${\Gamma^{\prime}}$

.

Now by the same lemma, we have $d$ and $c$ are right homotopic, that is, we
have $p:\Gamma\rightarrow{(\prod_{a:\mathbf{N}}Y_{a})^{I}}$ such that the
following diagram commutes:

${{(\prod_{a:\mathbf{N}}Y_{a})^{I}}}$${\Gamma}$${{\prod_{a:\mathbf{N}}Y_{a}\times\prod_{a:\mathbf{N}}Y_{a}}}$$\scriptstyle{p}$

.

This means that there is a term in the type $\operatorname{\mathsf{Id}}(d,c)$
as being terms of $\prod_{a:\mathbf{N}}Y_{a}$. So the second requirement in
Definition 5.1 holds. We omit the details, but the naturality conditions
follow from the coherence conditions on $\mathtt{Ty}$. ∎

In Theorem 5.3, we provide a class of two-level CwFs that satisfy the axiom
that $\mathbb{N}^{e}$ is a cofibrant exo-type. This is the main result of this
section.

######  Theorem 5.3.

If $(\mathcal{C},\mathtt{Ty},\mathtt{Tm})$ is CwF (with sufficient type
formers) has exo-nat products, the corresponding two-level CwF obtained by
Definition 4.14 satisfies the axiom that $\mathbb{N}^{e}$ is a cofibrant exo-
type.

###### Proof.

Recall that $\mathbb{N}^{e}:\widehat{\mathtt{Ty}}(1_{\widehat{\mathcal{C}}})$.
For any $P:\widehat{\mathcal{C}}$, the context morphism $\sigma:P\rightarrow
1_{\widehat{\mathcal{C}}}$ is unique, so we omit substitutions over such
morphisms and write $P.\mathbb{N}^{e}$ instead of $P.\mathbb{N}^{e}[\sigma]$.

First, we define the map
$\Theta^{\mathtt{Ty}}_{P}:\mathtt{Ty}^{f}(P.\mathbb{N}^{e})\rightarrow\mathtt{Ty}^{f}(P)$.
For any
$Y:\mathtt{Ty}^{f}(P.\mathbb{N}^{e})=\widehat{\mathcal{C}}(P.\mathbb{N}^{e},\mathtt{Ty})$,
we need
$\Theta^{\mathtt{Ty}}_{P}(Y):\mathtt{Ty}^{f}(P)=\widehat{\mathcal{C}}(P,\mathtt{Ty})$.
We denote $\Theta^{\mathtt{Ty}}_{P}(Y)$ by $\tilde{Y}$ for easier reading.
Now, for $\Gamma:\mathcal{C}$ and $x:P_{\Gamma}$, we define

$\tilde{Y}_{\Gamma}(x):=\Omega_{\Gamma}\left((Y_{\Gamma}(x,n))_{n}\right)$

where the map
$\Omega_{\Gamma}:\prod_{\mathbf{N}}\mathtt{Ty}(\Gamma)\rightarrow\mathtt{Ty}(\Gamma)$
is obtained by the assumption of having exo-nat products, Definition 5.1.
Since we have $Y_{\Gamma}(x,n):\mathtt{Ty}(\Gamma)$, the definition makes
sense. We want to show

$\mathcal{c}_{P}(\tilde{Y})\cong{\prod}^{e}(\mathbb{N}^{e},\mathcal{c}_{P.\mathbb{N}^{e}}(Y)).$

Both are elements in $\widehat{\mathtt{Ty}}(P)$, namely, presheaves over $\int
P$. Thus, it is enough to define a natural transformation
$G:\mathcal{c}_{P}(\tilde{Y})\rightarrow\prod^{e}(\mathbb{N}^{e},\mathcal{c}_{P.\mathbb{N}^{e}}(Y))$
such that for any $\Gamma:\mathcal{C}$ and $x:P_{\Gamma}$, the map

$G_{\Gamma,x}:\mathcal{c}_{P}(\tilde{Y})(\Gamma,x)\rightarrow{\prod}^{e}(\mathbb{N}^{e},\mathcal{c}_{P.\mathbb{N}^{e}}(Y))(\Gamma,x)$

is an isomorphism of sets, namely, a bijection. If we elaborate on these
further, we obtain the following. By definition,
$\mathcal{c}_{P}(\tilde{Y})(\Gamma,x)=\mathtt{Tm}(\Gamma,\tilde{Y}_{\Gamma}(x))$.
Also,
${\prod}^{e}(\mathbb{N}^{e},\mathcal{c}_{P.\mathbb{N}^{e}}(Y))(\Gamma,x)$
consists of the elements

$f:\prod_{\begin{subarray}{c}\Delta:\mathcal{C}\\\
\sigma:\Delta\rightarrow\Gamma\\\
n:\mathbb{N}^{e}(\Delta,x[\sigma])\end{subarray}}\mathcal{c}_{P.\mathbb{N}^{e}}(Y)(\Delta,x[\sigma],n)\Big{(}=\mathtt{Tm}(\Delta,Y_{\Delta}(x[\sigma],n))\Big{)}$

such that if $\Upsilon:\mathcal{C}$ and $\tau:\Upsilon\rightarrow\Delta$, then
$f(\Delta,\sigma,n)[\tau]=f(\Upsilon,\sigma\circ\tau,n[\tau])$. By the
definition of $\mathbb{N}^{e}$, we have
$\mathbb{N}^{e}(\Delta,x[\sigma])=\mathbf{N}$, external natural number set,
and having exo-nat products provides us

$\prod_{n:\mathbf{N}}\mathtt{Tm}(\Delta,Y_{\Delta}(x[\sigma],n))\cong\mathtt{Tm}(\Delta,\tilde{Y}(x[\sigma])).$

Thus, the range of $G_{\Gamma,x}$ can be written as

$f:\prod_{\begin{subarray}{c}\Delta:\mathcal{C}\\\
\sigma:\Delta\rightarrow\Gamma\end{subarray}}\mathtt{Tm}(\Delta,\tilde{Y}_{\Delta}(x[\sigma]))$

such that if $\Upsilon:\mathcal{C}$ and $\tau:\Upsilon\rightarrow\Delta$, then
$f(\Delta,\sigma)[\tau]=f(\Upsilon,\sigma\circ\tau)$. This elaboration allows
us to easily perceive that this function is a bijection because it is a
standard application of the Yoneda Lemma. The naturality condition of this
operation is also easily satisfied because the substitution is functorial.
Thus, we have confirmed the first stage of our claim. It remains to handle the
contractibility part.

Basically, we need to show that for the center of contraction
$c:\mathtt{Tm}^{f}(P.\mathbb{N}^{e},Y)$ and the identity terms in
$\operatorname{\mathsf{Id}}(c,d)$ for any other terms
$d:\mathtt{Tm}^{f}(P.\mathbb{N}^{e},Y)$, we can find (naturally) a center of
contraction $\tilde{c}:\mathtt{Tm}^{f}(P,\tilde{Y})$ and an identity term
$\operatorname{\mathsf{Id}}(\tilde{c},\tilde{d})$ for any other terms
$\tilde{d}:\mathtt{Tm}^{f}(P,\tilde{Y})$. With a similar elaboration on terms,
we have
$\mathtt{Tm}^{f}(P.\mathbb{N}^{e},Y)=\widehat{\mathtt{Tm}}(P.\mathbb{N}^{e},\mathcal{c}_{P.\mathbb{N}^{e}}(Y))$
and
$\mathtt{Tm}^{f}(P,\tilde{Y})=\widehat{\mathtt{Tm}}(P,\mathcal{c}_{P}(\tilde{Y}))$.
Therefore, we know

$c:\prod_{\begin{subarray}{c}\Gamma:\mathcal{C}\\\ x:P_{\Gamma}\\\
n:\mathbb{N}^{e}(\Gamma,x)\end{subarray}}\mathcal{c}_{P.\mathbb{N}^{e}}(Y)(\Gamma,x,n)\Big{(}=\mathtt{Tm}(\Gamma,Y_{\Gamma}(x,n))\Big{)}$

is a center of contraction, for any such term $d$, we have a term in
$\operatorname{\mathsf{Id}}(c,d)$, and we need

$\tilde{c}:\prod_{\begin{subarray}{c}\Gamma:\mathcal{C}\\\
x:P_{\Gamma}\end{subarray}}\mathcal{c}_{P}(\tilde{Y})(\Gamma,x)\left(=\mathtt{Tm}(\Gamma,\tilde{Y}_{\Gamma}(x))\right)$

as a center of contraction, and related contracting terms. However, this is
exactly the second criterion in Definition 5.1, and we have already assumed
it.

Therefore, $\mathbb{N}^{e}$ is a cofibrant exo-type in the presheaf two-level
CwF. ∎

######  Remark 5.4.

Example 5.2 also enables us to construct a two-level CwF out of the class in
the theorem that satisfies the axiom. Indeed, we can take
$\mathtt{Ty}^{e}(\Gamma)$ as the set of all morphisms over $\Gamma$, and
$\mathtt{Tm}^{e}$ as the same as $\mathtt{Tm}$, and obtain a two-level CwF
$(\mathcal{C},\mathtt{Ty}^{e},\mathtt{Tm}^{e},\mathtt{Ty},\mathtt{Tm})$ with
the conversion $\mathcal{c}:\mathtt{Ty}\rightarrow\mathtt{Ty}^{e}$ as being
inclusion. It is then enough to take the map $\Theta_{\Gamma}(Y)$ in
Definition 4.17 as equal to $\prod_{a:\mathbf{N}}Y_{a}$.

##  6 Future directions

As previously mentioned, this formalisation project aims to move a study about
2LTT [1] to Agda. In addition to definitions and results here, we also
formalised _exo-categories_ and _diagram signatures_ in that study. More will
be added in the future.

We also plan to generalize the results about cofibrancy and sharpness. Natural
numbers, lists, and binary-trees are all inductive types. The general class of
such inductive types is called _W-types_. Similar to the cofibrant exo-nat
axiom, we have been studying on possible conditions (or axioms) related to
W-types to obtain criteria for cofibrant and sharp W-types. Currently, a study
on W-types in 2LTT has not been conducted yet; thus, we plan to work on this
open problem.

We have been studying to improve the Agda library. The experimental feature of
Agda we used reveals also some bugs; hence, we plan to solve these issues to
obtain precise consistency. Furthermore, it is not unreasonable to think that
this study will offer new ideas about the concepts specific to 2LTT.

## References

  * [1] Benedikt Ahrens, Paige Randall North, Michael Shulman, and Dimitris Tsementzis, _The Univalence Principle_ , Available on arXiv: 2102.06275v3, 2022.
  * [2] Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pak, _The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar_ , J Autom Reason, 61(1):9-32, https://doi.org/10.1007/s10817-017-9440-6, 2018.
  * [3] Henk Barendregt and Herman Geuvers, _Proof-assistants using dependent type systems_ , Handbook of automated reasoning, Elsevier Science Publishers B. V., NLD, 1149–1238, 2001.
  * [4] Danil Annenkov, Paolo Capriotti, Nicolai Kraus, and Christian Sattler, _Two-Level Type Theory and Applications_ , Mathematical Structures in Computer Science, 1-56. https://doi.org/10.1017/S0960129523000130, 2023.
  * [5] Paolo Capriotti, _Models of Type Theory with Strict Equality_ , Phd thesis, School of Computer Science, University of Nottingham, 2016.
  * [6] Shimon Even, _Graph Algorithms_ , 2nd ed., Ed. Guy Even, Cambridge University Press, https://doi.org/10.1017/CBO9781139015165, 2011.
  * [7] Herman Geuvers, _Proof assistants: History, ideas and future_ , Sadhana 34, 3–25, https://doi.org/10.1007/s12046-009-0001-5, 2009.
  * [8] Martin Hofmann, _Syntax and semantics of dependent types_ in: Semantics and Logics of Computation, Cambridge University Press, 79–130, 1997.
  * [9] Mark Hovey, _Model Categories_ , Mathematical Surveys and Monographs, 63 AMS, ISBN:978-0-8218-4361-1, https://doi.org/10.1090/surv/063, 1999.
  * [10] Krzysztof Kapulkin and Peter LeFanu Lumsdaine, _The simplicial model of Univalent Foundations (after Voevodsky)_ , J. Eur. Math. Soc. 23, no. 6, pp. 2071–2126, 2021.
  * [11] Peter LeFanu Lumsdaine and Michael Shulman, _Semantics of higher inductive types_ , Mathematical Proceedings of the Cambridge Philosophical Society, 169(1), 159-208, https://doi.org/10.1017/S030500411900015X, 2020.
  * [12] Peter Lefanu Lumsdaine and Michael A. Warren, _The Local Universes Model: An Overlooked Coherence Construction for Dependent Type Theories_ , ACM Trans. Comput. Logic 16, 3, Article 23, https://doi.org/10.1145/2754931, 2015.
  * [13] The Univalent Foundations Program, _Homotopy type theory: Univalent foundations of mathematics_ , https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  * [14] Elif Uskuplu, _Formalization of 2LTT in Agda_ , https://github.com/ElifUskuplu/2LTT-Agda, 2023.
  * [15] Vladimir Voevodsky, _A simple type system with two identity types_ , Unpublished note, 2013.