WEBVTT
Kind: captions
Language: en

00:00:04.950 --> 00:00:07.519 align:start position:0%
 
hello<00:00:05.549><c> everyone</c><00:00:06.029><c> I'm</c><00:00:06.779><c> from</c><00:00:07.049><c> Brazil</c><00:00:07.200><c> from</c>

00:00:07.519 --> 00:00:07.529 align:start position:0%
hello everyone I'm from Brazil from
 

00:00:07.529 --> 00:00:10.160 align:start position:0%
hello everyone I'm from Brazil from
state<00:00:07.799><c> box</c><00:00:08.100><c> and</c><00:00:08.490><c> I'm</c><00:00:08.700><c> going</c><00:00:09.180><c> to</c><00:00:09.209><c> talk</c><00:00:09.870><c> about</c>

00:00:10.160 --> 00:00:10.170 align:start position:0%
state box and I'm going to talk about
 

00:00:10.170 --> 00:00:14.029 align:start position:0%
state box and I'm going to talk about
how<00:00:10.830><c> to</c><00:00:10.860><c> map</c><00:00:11.250><c> finite</c><00:00:11.580><c> state</c><00:00:11.760><c> machines</c><00:00:12.180><c> to</c><00:00:13.039><c> ZK</c>

00:00:14.029 --> 00:00:14.039 align:start position:0%
how to map finite state machines to ZK
 

00:00:14.039 --> 00:00:17.720 align:start position:0%
how to map finite state machines to ZK
snarks<00:00:14.580><c> using</c><00:00:15.240><c> category</c><00:00:15.869><c> theory</c><00:00:16.550><c> this</c><00:00:17.550><c> is</c>

00:00:17.720 --> 00:00:17.730 align:start position:0%
snarks using category theory this is
 

00:00:17.730 --> 00:00:20.240 align:start position:0%
snarks using category theory this is
joint<00:00:17.970><c> work</c><00:00:18.029><c> with</c><00:00:18.320><c> unready</c><00:00:19.320><c> SPO</c><00:00:19.560><c> and</c><00:00:19.859><c> Josh</c>

00:00:20.240 --> 00:00:20.250 align:start position:0%
joint work with unready SPO and Josh
 

00:00:20.250 --> 00:00:22.040 align:start position:0%
joint work with unready SPO and Josh
aphids<00:00:20.580><c> are</c><00:00:20.760><c> all</c><00:00:20.880><c> four</c><00:00:21.150><c> from</c><00:00:21.599><c> our</c><00:00:21.720><c> team</c><00:00:21.929><c> as</c>

00:00:22.040 --> 00:00:22.050 align:start position:0%
aphids are all four from our team as
 

00:00:22.050 --> 00:00:24.499 align:start position:0%
aphids are all four from our team as
well<00:00:22.230><c> we</c><00:00:22.890><c> have</c><00:00:23.220><c> a</c><00:00:23.249><c> paper</c><00:00:23.580><c> about</c><00:00:23.820><c> what</c><00:00:24.179><c> we</c><00:00:24.359><c> did</c>

00:00:24.499 --> 00:00:24.509 align:start position:0%
well we have a paper about what we did
 

00:00:24.509 --> 00:00:28.220 align:start position:0%
well we have a paper about what we did
which<00:00:24.960><c> is</c><00:00:24.990><c> this</c><00:00:25.619><c> archive</c><00:00:26.310><c> link</c><00:00:26.490><c> there</c><00:00:27.169><c> okay</c><00:00:28.169><c> so</c>

00:00:28.220 --> 00:00:28.230 align:start position:0%
which is this archive link there okay so
 

00:00:28.230 --> 00:00:31.909 align:start position:0%
which is this archive link there okay so
let's<00:00:29.220><c> start</c><00:00:29.749><c> what</c><00:00:30.749><c> is</c><00:00:30.869><c> a</c><00:00:30.900><c> zero</c><00:00:31.289><c> knowledge</c>

00:00:31.909 --> 00:00:31.919 align:start position:0%
let's start what is a zero knowledge
 

00:00:31.919 --> 00:00:36.470 align:start position:0%
let's start what is a zero knowledge
snark<00:00:33.530><c> they</c><00:00:34.530><c> are</c><00:00:34.590><c> just</c><00:00:34.860><c> a</c><00:00:34.980><c> way</c><00:00:35.220><c> to</c><00:00:35.280><c> prove</c><00:00:36.180><c> that</c>

00:00:36.470 --> 00:00:36.480 align:start position:0%
snark they are just a way to prove that
 

00:00:36.480 --> 00:00:38.799 align:start position:0%
snark they are just a way to prove that
some<00:00:36.750><c> computation</c><00:00:37.379><c> follows</c><00:00:38.129><c> some</c><00:00:38.550><c> rules</c>

00:00:38.799 --> 00:00:38.809 align:start position:0%
some computation follows some rules
 

00:00:38.809 --> 00:00:41.540 align:start position:0%
some computation follows some rules
without<00:00:39.809><c> revealing</c><00:00:40.050><c> anything</c><00:00:40.800><c> about</c><00:00:41.399><c> the</c>

00:00:41.540 --> 00:00:41.550 align:start position:0%
without revealing anything about the
 

00:00:41.550 --> 00:00:44.060 align:start position:0%
without revealing anything about the
computation<00:00:42.090><c> itself</c><00:00:42.710><c> they</c><00:00:43.710><c> are</c><00:00:43.739><c> good</c><00:00:43.920><c> for</c>

00:00:44.060 --> 00:00:44.070 align:start position:0%
computation itself they are good for
 

00:00:44.070 --> 00:00:47.150 align:start position:0%
computation itself they are good for
privacy<00:00:44.809><c> they</c><00:00:45.809><c> compress</c><00:00:46.260><c> a</c><00:00:46.680><c> lot</c><00:00:47.010><c> of</c>

00:00:47.150 --> 00:00:47.160 align:start position:0%
privacy they compress a lot of
 

00:00:47.160 --> 00:00:49.910 align:start position:0%
privacy they compress a lot of
information<00:00:47.820><c> and</c><00:00:48.140><c> blockchain</c><00:00:49.140><c> people</c><00:00:49.679><c> seem</c>

00:00:49.910 --> 00:00:49.920 align:start position:0%
information and blockchain people seem
 

00:00:49.920 --> 00:00:52.520 align:start position:0%
information and blockchain people seem
to<00:00:49.949><c> love</c><00:00:50.219><c> them</c><00:00:50.489><c> so</c><00:00:50.879><c> why</c><00:00:51.690><c> not</c><00:00:51.719><c> doing</c><00:00:52.199><c> some</c>

00:00:52.520 --> 00:00:52.530 align:start position:0%
to love them so why not doing some
 

00:00:52.530 --> 00:00:55.729 align:start position:0%
to love them so why not doing some
research<00:00:52.890><c> about</c><00:00:53.070><c> them</c><00:00:54.350><c> the</c><00:00:55.350><c> nice</c><00:00:55.500><c> thing</c><00:00:55.710><c> is</c>

00:00:55.729 --> 00:00:55.739 align:start position:0%
research about them the nice thing is
 

00:00:55.739 --> 00:00:57.619 align:start position:0%
research about them the nice thing is
that<00:00:55.859><c> for</c><00:00:56.280><c> this</c><00:00:56.399><c> talk</c><00:00:56.699><c> you</c><00:00:56.940><c> don't</c><00:00:57.269><c> really</c><00:00:57.449><c> have</c>

00:00:57.619 --> 00:00:57.629 align:start position:0%
that for this talk you don't really have
 

00:00:57.629 --> 00:00:59.740 align:start position:0%
that for this talk you don't really have
to<00:00:57.809><c> know</c><00:00:57.989><c> what</c><00:00:58.289><c> does</c><00:00:58.530><c> that</c><00:00:58.769><c> case</c><00:00:58.980><c> not</c><00:00:59.280><c> is</c>

00:00:59.740 --> 00:00:59.750 align:start position:0%
to know what does that case not is
 

00:00:59.750 --> 00:01:02.569 align:start position:0%
to know what does that case not is
everything<00:01:00.750><c> you</c><00:01:00.839><c> have</c><00:01:00.960><c> to</c><00:01:01.140><c> know</c><00:01:01.170><c> is</c><00:01:01.679><c> that</c><00:01:02.160><c> if</c>

00:01:02.569 --> 00:01:02.579 align:start position:0%
everything you have to know is that if
 

00:01:02.579 --> 00:01:05.000 align:start position:0%
everything you have to know is that if
you<00:01:02.730><c> have</c><00:01:02.820><c> a</c><00:01:02.850><c> boolean</c><00:01:03.300><c> circuit</c><00:01:03.650><c> then</c><00:01:04.650><c> you</c><00:01:04.800><c> can</c>

00:01:05.000 --> 00:01:05.010 align:start position:0%
you have a boolean circuit then you can
 

00:01:05.010 --> 00:01:07.940 align:start position:0%
you have a boolean circuit then you can
turn<00:01:05.220><c> it</c><00:01:05.460><c> into</c><00:01:05.670><c> a</c><00:01:05.820><c> set</c><00:01:06.030><c> case</c><00:01:06.270><c> not</c><00:01:06.770><c> so</c><00:01:07.770><c> now</c><00:01:07.890><c> the</c>

00:01:07.940 --> 00:01:07.950 align:start position:0%
turn it into a set case not so now the
 

00:01:07.950 --> 00:01:10.460 align:start position:0%
turn it into a set case not so now the
question<00:01:08.280><c> becomes</c><00:01:08.400><c> cool</c><00:01:09.060><c> but</c><00:01:09.600><c> what</c><00:01:10.350><c> is</c><00:01:10.439><c> a</c>

00:01:10.460 --> 00:01:10.470 align:start position:0%
question becomes cool but what is a
 

00:01:10.470 --> 00:01:14.359 align:start position:0%
question becomes cool but what is a
boolean<00:01:10.829><c> circuit</c><00:01:11.900><c> well</c><00:01:12.900><c> it's</c><00:01:13.470><c> just</c><00:01:13.619><c> literally</c>

00:01:14.359 --> 00:01:14.369 align:start position:0%
boolean circuit well it's just literally
 

00:01:14.369 --> 00:01:16.310 align:start position:0%
boolean circuit well it's just literally
a<00:01:14.520><c> bunch</c><00:01:14.939><c> of</c><00:01:15.119><c> logical</c><00:01:15.659><c> gates</c><00:01:15.900><c> who</c><00:01:16.170><c> are</c>

00:01:16.310 --> 00:01:16.320 align:start position:0%
a bunch of logical gates who are
 

00:01:16.320 --> 00:01:18.710 align:start position:0%
a bunch of logical gates who are
together<00:01:16.590><c> so</c><00:01:17.220><c> in</c><00:01:17.670><c> here</c><00:01:17.939><c> you</c><00:01:18.090><c> see</c><00:01:18.299><c> for</c><00:01:18.659><c> instance</c>

00:01:18.710 --> 00:01:18.720 align:start position:0%
together so in here you see for instance
 

00:01:18.720 --> 00:01:21.859 align:start position:0%
together so in here you see for instance
four<00:01:19.229><c> gates</c><00:01:19.500><c> an</c><00:01:19.829><c> and</c><00:01:20.159><c> gate</c><00:01:20.460><c> and</c><00:01:20.759><c> or</c><00:01:21.509><c> gate</c><00:01:21.540><c> a</c>

00:01:21.859 --> 00:01:21.869 align:start position:0%
four gates an and gate and or gate a
 

00:01:21.869 --> 00:01:24.859 align:start position:0%
four gates an and gate and or gate a
copy<00:01:22.320><c> gate</c><00:01:22.619><c> and</c><00:01:22.979><c> a</c><00:01:23.040><c> constant</c><00:01:23.490><c> gate</c><00:01:23.670><c> and</c><00:01:24.659><c> you</c>

00:01:24.859 --> 00:01:24.869 align:start position:0%
copy gate and a constant gate and you
 

00:01:24.869 --> 00:01:26.270 align:start position:0%
copy gate and a constant gate and you
know<00:01:24.990><c> this</c><00:01:25.170><c> is</c><00:01:25.259><c> a</c><00:01:25.320><c> boolean</c><00:01:25.560><c> circuit</c><00:01:25.799><c> you</c><00:01:26.070><c> just</c>

00:01:26.270 --> 00:01:26.280 align:start position:0%
know this is a boolean circuit you just
 

00:01:26.280 --> 00:01:28.789 align:start position:0%
know this is a boolean circuit you just
like<00:01:26.399><c> work</c><00:01:26.729><c> them</c><00:01:27.090><c> together</c><00:01:27.329><c> and</c><00:01:27.899><c> you</c><00:01:28.229><c> put</c><00:01:28.439><c> bits</c>

00:01:28.789 --> 00:01:28.799 align:start position:0%
like work them together and you put bits
 

00:01:28.799 --> 00:01:31.039 align:start position:0%
like work them together and you put bits
in<00:01:29.159><c> the</c><00:01:29.369><c> vertical</c><00:01:29.759><c> wires</c><00:01:30.000><c> and</c><00:01:30.540><c> you</c><00:01:30.720><c> get</c><00:01:30.869><c> an</c>

00:01:31.039 --> 00:01:31.049 align:start position:0%
in the vertical wires and you get an
 

00:01:31.049 --> 00:01:35.270 align:start position:0%
in the vertical wires and you get an
output<00:01:31.140><c> bit</c><00:01:31.860><c> on</c><00:01:32.460><c> the</c><00:01:32.700><c> right</c><00:01:33.890><c> okay</c><00:01:34.890><c> so</c><00:01:34.950><c> what</c><00:01:35.189><c> is</c>

00:01:35.270 --> 00:01:35.280 align:start position:0%
output bit on the right okay so what is
 

00:01:35.280 --> 00:01:37.730 align:start position:0%
output bit on the right okay so what is
a<00:01:35.310><c> finite</c><00:01:35.670><c> state</c><00:01:35.909><c> machine</c><00:01:36.450><c> a</c><00:01:37.049><c> fine</c><00:01:37.560><c> state</c>

00:01:37.730 --> 00:01:37.740 align:start position:0%
a finite state machine a fine state
 

00:01:37.740 --> 00:01:40.249 align:start position:0%
a finite state machine a fine state
machine<00:01:38.070><c> in</c><00:01:38.189><c> some</c><00:01:38.460><c> very</c><00:01:39.149><c> old</c><00:01:39.299><c> gadget</c><00:01:39.990><c> in</c>

00:01:40.249 --> 00:01:40.259 align:start position:0%
machine in some very old gadget in
 

00:01:40.259 --> 00:01:42.530 align:start position:0%
machine in some very old gadget in
theoretical<00:01:40.619><c> computer</c><00:01:40.890><c> science</c><00:01:41.579><c> all</c><00:01:42.479><c> the</c>

00:01:42.530 --> 00:01:42.540 align:start position:0%
theoretical computer science all the
 

00:01:42.540 --> 00:01:45.289 align:start position:0%
theoretical computer science all the
means<00:01:42.960><c> good</c><00:01:43.500><c> because</c><00:01:44.189><c> it</c><00:01:44.490><c> means</c><00:01:44.729><c> that</c><00:01:44.969><c> a</c><00:01:45.000><c> lot</c>

00:01:45.289 --> 00:01:45.299 align:start position:0%
means good because it means that a lot
 

00:01:45.299 --> 00:01:47.630 align:start position:0%
means good because it means that a lot
of<00:01:45.329><c> period</c><00:01:45.899><c> has</c><00:01:46.110><c> been</c><00:01:46.500><c> redeveloped</c><00:01:47.040><c> about</c>

00:01:47.630 --> 00:01:47.640 align:start position:0%
of period has been redeveloped about
 

00:01:47.640 --> 00:01:50.300 align:start position:0%
of period has been redeveloped about
fine<00:01:48.390><c> state</c><00:01:48.659><c> machines</c><00:01:49.049><c> we</c><00:01:49.439><c> know</c><00:01:49.619><c> perfectly</c>

00:01:50.300 --> 00:01:50.310 align:start position:0%
fine state machines we know perfectly
 

00:01:50.310 --> 00:01:53.300 align:start position:0%
fine state machines we know perfectly
well<00:01:50.520><c> how</c><00:01:50.850><c> they</c><00:01:51.270><c> work</c><00:01:51.719><c> and</c><00:01:52.710><c> how</c><00:01:52.770><c> to</c><00:01:52.920><c> prove</c>

00:01:53.300 --> 00:01:53.310 align:start position:0%
well how they work and how to prove
 

00:01:53.310 --> 00:01:56.120 align:start position:0%
well how they work and how to prove
formal<00:01:53.759><c> properties</c><00:01:54.270><c> about</c><00:01:54.600><c> them</c><00:01:54.869><c> so</c><00:01:55.829><c> in</c><00:01:56.039><c> here</c>

00:01:56.120 --> 00:01:56.130 align:start position:0%
formal properties about them so in here
 

00:01:56.130 --> 00:01:57.620 align:start position:0%
formal properties about them so in here
you<00:01:56.310><c> can</c><00:01:56.460><c> see</c><00:01:56.490><c> this</c><00:01:56.759><c> is</c><00:01:56.909><c> just</c><00:01:56.939><c> a</c><00:01:57.270><c> vending</c>

00:01:57.620 --> 00:01:57.630 align:start position:0%
you can see this is just a vending
 

00:01:57.630 --> 00:02:01.580 align:start position:0%
you can see this is just a vending
machine<00:01:57.860><c> a</c><00:01:58.860><c> model</c><00:01:59.549><c> of</c><00:01:59.670><c> a</c><00:01:59.789><c> very</c><00:02:00.030><c> simple</c><00:02:00.590><c> vending</c>

00:02:01.580 --> 00:02:01.590 align:start position:0%
machine a model of a very simple vending
 

00:02:01.590 --> 00:02:05.090 align:start position:0%
machine a model of a very simple vending
machine<00:02:02.719><c> you</c><00:02:03.719><c> can</c><00:02:03.899><c> think</c><00:02:04.320><c> about</c><00:02:04.439><c> it</c><00:02:04.710><c> just</c><00:02:04.950><c> as</c><00:02:05.070><c> a</c>

00:02:05.090 --> 00:02:05.100 align:start position:0%
machine you can think about it just as a
 

00:02:05.100 --> 00:02:07.550 align:start position:0%
machine you can think about it just as a
graph<00:02:05.399><c> the</c><00:02:05.880><c> vertex</c><00:02:06.180><c> is</c><00:02:06.390><c> represent</c><00:02:06.990><c> all</c><00:02:07.350><c> the</c>

00:02:07.550 --> 00:02:07.560 align:start position:0%
graph the vertex is represent all the
 

00:02:07.560 --> 00:02:10.639 align:start position:0%
graph the vertex is represent all the
possible<00:02:07.680><c> states</c><00:02:08.310><c> of</c><00:02:08.520><c> the</c><00:02:08.880><c> system</c><00:02:09.060><c> and</c><00:02:09.649><c> the</c>

00:02:10.639 --> 00:02:10.649 align:start position:0%
possible states of the system and the
 

00:02:10.649 --> 00:02:14.630 align:start position:0%
possible states of the system and the
edges<00:02:11.070><c> so</c><00:02:11.940><c> the</c><00:02:12.090><c> arcs</c><00:02:12.420><c> represent</c><00:02:13.640><c> operations</c>

00:02:14.630 --> 00:02:14.640 align:start position:0%
edges so the arcs represent operations
 

00:02:14.640 --> 00:02:16.820 align:start position:0%
edges so the arcs represent operations
that<00:02:14.819><c> mutate</c><00:02:15.269><c> state</c><00:02:15.629><c> so</c><00:02:16.200><c> you</c><00:02:16.230><c> see</c><00:02:16.500><c> that</c><00:02:16.650><c> in</c>

00:02:16.820 --> 00:02:16.830 align:start position:0%
that mutate state so you see that in
 

00:02:16.830 --> 00:02:17.910 align:start position:0%
that mutate state so you see that in
here<00:02:16.950><c> you</c><00:02:17.129><c> can</c><00:02:17.340><c> insert</c>

00:02:17.910 --> 00:02:17.920 align:start position:0%
here you can insert
 

00:02:17.920 --> 00:02:19.949 align:start position:0%
here you can insert
the<00:02:18.010><c> coin</c><00:02:18.220><c> and</c><00:02:18.490><c> go</c><00:02:18.610><c> from</c><00:02:18.790><c> ready</c><00:02:19.060><c> to</c><00:02:19.270><c> select</c><00:02:19.540><c> and</c>

00:02:19.949 --> 00:02:19.959 align:start position:0%
the coin and go from ready to select and
 

00:02:19.959 --> 00:02:23.130 align:start position:0%
the coin and go from ready to select and
then<00:02:20.590><c> you</c><00:02:20.709><c> can</c><00:02:20.980><c> order</c><00:02:21.490><c> stuff</c><00:02:21.520><c> and</c><00:02:22.120><c> get</c><00:02:22.540><c> changed</c>

00:02:23.130 --> 00:02:23.140 align:start position:0%
then you can order stuff and get changed
 

00:02:23.140 --> 00:02:26.100 align:start position:0%
then you can order stuff and get changed
and<00:02:23.790><c> a</c><00:02:24.790><c> competition</c><00:02:25.150><c> that</c><00:02:25.420><c> follows</c><00:02:25.780><c> the</c><00:02:25.900><c> rules</c>

00:02:26.100 --> 00:02:26.110 align:start position:0%
and a competition that follows the rules
 

00:02:26.110 --> 00:02:28.589 align:start position:0%
and a competition that follows the rules
of<00:02:26.650><c> the</c><00:02:26.920><c> thrusting</c><00:02:27.459><c> machine</c><00:02:27.819><c> is</c><00:02:27.970><c> just</c><00:02:28.239><c> a</c><00:02:28.330><c> path</c>

00:02:28.589 --> 00:02:28.599 align:start position:0%
of the thrusting machine is just a path
 

00:02:28.599 --> 00:02:30.990 align:start position:0%
of the thrusting machine is just a path
in<00:02:28.959><c> this</c><00:02:29.170><c> graph</c><00:02:29.230><c> so</c><00:02:30.010><c> you</c><00:02:30.040><c> see</c><00:02:30.310><c> that</c><00:02:30.459><c> you</c><00:02:30.640><c> can't</c>

00:02:30.990 --> 00:02:31.000 align:start position:0%
in this graph so you see that you can't
 

00:02:31.000 --> 00:02:34.199 align:start position:0%
in this graph so you see that you can't
buy<00:02:31.690><c> coke</c><00:02:32.170><c> if</c><00:02:32.500><c> you</c><00:02:33.190><c> are</c><00:02:33.310><c> not</c><00:02:33.580><c> in</c><00:02:33.760><c> the</c><00:02:33.880><c> Select</c>

00:02:34.199 --> 00:02:34.209 align:start position:0%
buy coke if you are not in the Select
 

00:02:34.209 --> 00:02:36.630 align:start position:0%
buy coke if you are not in the Select
State<00:02:34.569><c> you</c><00:02:35.380><c> need</c><00:02:35.620><c> to</c><00:02:35.830><c> and</c><00:02:36.069><c> if</c><00:02:36.160><c> you're</c><00:02:36.310><c> in</c><00:02:36.520><c> your</c>

00:02:36.630 --> 00:02:36.640 align:start position:0%
State you need to and if you're in your
 

00:02:36.640 --> 00:02:38.550 align:start position:0%
State you need to and if you're in your
ready<00:02:37.030><c> state</c><00:02:37.420><c> then</c><00:02:37.780><c> you</c><00:02:37.930><c> have</c><00:02:38.050><c> to</c><00:02:38.170><c> insert</c><00:02:38.530><c> a</c>

00:02:38.550 --> 00:02:38.560 align:start position:0%
ready state then you have to insert a
 

00:02:38.560 --> 00:02:42.630 align:start position:0%
ready state then you have to insert a
coin<00:02:38.860><c> first</c><00:02:40.709><c> so</c><00:02:41.709><c> the</c><00:02:41.890><c> idea</c><00:02:42.069><c> is</c><00:02:42.130><c> that</c><00:02:42.220><c> if</c><00:02:42.340><c> we</c><00:02:42.489><c> can</c>

00:02:42.630 --> 00:02:42.640 align:start position:0%
coin first so the idea is that if we can
 

00:02:42.640 --> 00:02:45.780 align:start position:0%
coin first so the idea is that if we can
map<00:02:42.910><c> these</c><00:02:43.360><c> paths</c><00:02:43.750><c> of</c><00:02:44.080><c> this</c><00:02:44.230><c> graph</c><00:02:44.560><c> to</c><00:02:45.370><c> boolean</c>

00:02:45.780 --> 00:02:45.790 align:start position:0%
map these paths of this graph to boolean
 

00:02:45.790 --> 00:02:49.080 align:start position:0%
map these paths of this graph to boolean
circuits<00:02:46.360><c> then</c><00:02:47.200><c> we</c><00:02:47.560><c> can</c><00:02:47.920><c> basically</c><00:02:48.400><c> turn</c><00:02:48.880><c> this</c>

00:02:49.080 --> 00:02:49.090 align:start position:0%
circuits then we can basically turn this
 

00:02:49.090 --> 00:02:51.870 align:start position:0%
circuits then we can basically turn this
circuit<00:02:49.630><c> into</c><00:02:49.989><c> a</c><00:02:50.019><c> snark</c><00:02:50.530><c> that</c><00:02:50.830><c> verifies</c><00:02:51.430><c> that</c>

00:02:51.870 --> 00:02:51.880 align:start position:0%
circuit into a snark that verifies that
 

00:02:51.880 --> 00:02:54.840 align:start position:0%
circuit into a snark that verifies that
a<00:02:52.800><c> computation</c><00:02:53.800><c> followed</c><00:02:54.370><c> the</c><00:02:54.640><c> rules</c>

00:02:54.840 --> 00:02:54.850 align:start position:0%
a computation followed the rules
 

00:02:54.850 --> 00:02:57.229 align:start position:0%
a computation followed the rules
determined<00:02:55.450><c> by</c><00:02:55.600><c> the</c><00:02:55.660><c> final</c><00:02:56.080><c> state</c><00:02:56.260><c> machine</c>

00:02:57.229 --> 00:02:57.239 align:start position:0%
determined by the final state machine
 

00:02:57.239 --> 00:03:00.330 align:start position:0%
determined by the final state machine
okay<00:02:58.239><c> so</c><00:02:58.299><c> but</c><00:02:58.480><c> what</c><00:02:58.750><c> is</c><00:02:58.870><c> category</c><00:02:59.440><c> theory</c><00:02:59.830><c> like</c>

00:03:00.330 --> 00:03:00.340 align:start position:0%
okay so but what is category theory like
 

00:03:00.340 --> 00:03:02.940 align:start position:0%
okay so but what is category theory like
where<00:03:00.730><c> do</c><00:03:00.940><c> you</c><00:03:01.090><c> use</c><00:03:01.360><c> category</c><00:03:02.049><c> theory</c><00:03:02.380><c> so</c>

00:03:02.940 --> 00:03:02.950 align:start position:0%
where do you use category theory so
 

00:03:02.950 --> 00:03:04.380 align:start position:0%
where do you use category theory so
category<00:03:03.340><c> theory</c><00:03:03.519><c> is</c><00:03:03.610><c> a</c><00:03:03.640><c> super</c><00:03:04.030><c> complicated</c>

00:03:04.380 --> 00:03:04.390 align:start position:0%
category theory is a super complicated
 

00:03:04.390 --> 00:03:06.780 align:start position:0%
category theory is a super complicated
thing<00:03:04.900><c> that</c><00:03:05.350><c> is</c><00:03:05.470><c> used</c><00:03:05.680><c> to</c><00:03:05.799><c> do</c><00:03:05.980><c> simple</c><00:03:06.549><c> things</c>

00:03:06.780 --> 00:03:06.790 align:start position:0%
thing that is used to do simple things
 

00:03:06.790 --> 00:03:10.110 align:start position:0%
thing that is used to do simple things
that<00:03:06.940><c> seems</c><00:03:07.480><c> like</c><00:03:08.080><c> not</c><00:03:08.530><c> great</c><00:03:08.980><c> but</c><00:03:09.760><c> actually</c>

00:03:10.110 --> 00:03:10.120 align:start position:0%
that seems like not great but actually
 

00:03:10.120 --> 00:03:13.410 align:start position:0%
that seems like not great but actually
it<00:03:10.330><c> is</c><00:03:10.739><c> because</c><00:03:11.739><c> it</c><00:03:12.100><c> scales</c><00:03:12.459><c> better</c><00:03:12.819><c> so</c><00:03:13.269><c> the</c>

00:03:13.410 --> 00:03:13.420 align:start position:0%
it is because it scales better so the
 

00:03:13.420 --> 00:03:16.740 align:start position:0%
it is because it scales better so the
idea<00:03:13.690><c> is</c><00:03:13.780><c> that</c><00:03:14.019><c> in</c><00:03:15.569><c> category</c><00:03:16.569><c> theory</c>

00:03:16.740 --> 00:03:16.750 align:start position:0%
idea is that in category theory
 

00:03:16.750 --> 00:03:20.100 align:start position:0%
idea is that in category theory
everything<00:03:17.739><c> is</c><00:03:17.860><c> compositional</c><00:03:18.810><c> it's</c><00:03:19.810><c> super</c>

00:03:20.100 --> 00:03:20.110 align:start position:0%
everything is compositional it's super
 

00:03:20.110 --> 00:03:22.280 align:start position:0%
everything is compositional it's super
related<00:03:20.470><c> to</c><00:03:20.590><c> type</c><00:03:20.920><c> theory</c><00:03:21.340><c> so</c><00:03:21.640><c> if</c><00:03:21.910><c> you</c><00:03:22.060><c> like</c>

00:03:22.280 --> 00:03:22.290 align:start position:0%
related to type theory so if you like
 

00:03:22.290 --> 00:03:24.750 align:start position:0%
related to type theory so if you like
functional<00:03:23.290><c> programming</c><00:03:23.350><c> you</c><00:03:24.250><c> should</c><00:03:24.519><c> really</c>

00:03:24.750 --> 00:03:24.760 align:start position:0%
functional programming you should really
 

00:03:24.760 --> 00:03:26.699 align:start position:0%
functional programming you should really
like<00:03:24.910><c> category</c><00:03:25.480><c> theory</c><00:03:25.690><c> even</c><00:03:26.140><c> if</c><00:03:26.260><c> functional</c>

00:03:26.699 --> 00:03:26.709 align:start position:0%
like category theory even if functional
 

00:03:26.709 --> 00:03:30.319 align:start position:0%
like category theory even if functional
programmers<00:03:27.220><c> won't</c><00:03:27.519><c> agree</c><00:03:27.760><c> with</c><00:03:27.910><c> me</c><00:03:28.060><c> on</c><00:03:28.090><c> this</c>

00:03:30.319 --> 00:03:30.329 align:start position:0%
programmers won't agree with me on this
 

00:03:30.329 --> 00:03:32.759 align:start position:0%
programmers won't agree with me on this
so<00:03:31.329><c> the</c><00:03:31.660><c> idea</c><00:03:31.840><c> is</c><00:03:31.930><c> that</c><00:03:32.049><c> in</c><00:03:32.170><c> category</c><00:03:32.560><c> theory</c>

00:03:32.759 --> 00:03:32.769 align:start position:0%
so the idea is that in category theory
 

00:03:32.769 --> 00:03:34.949 align:start position:0%
so the idea is that in category theory
you<00:03:33.070><c> can</c><00:03:33.340><c> relate</c><00:03:34.209><c> different</c><00:03:34.810><c> mathematical</c>

00:03:34.949 --> 00:03:34.959 align:start position:0%
you can relate different mathematical
 

00:03:34.959 --> 00:03:37.229 align:start position:0%
you can relate different mathematical
structures<00:03:35.829><c> everything</c><00:03:36.310><c> is</c><00:03:36.459><c> formally</c>

00:03:37.229 --> 00:03:37.239 align:start position:0%
structures everything is formally
 

00:03:37.239 --> 00:03:39.390 align:start position:0%
structures everything is formally
interconnected<00:03:38.230><c> in</c><00:03:38.440><c> a</c><00:03:38.560><c> way</c><00:03:38.709><c> that</c><00:03:38.890><c> respects</c>

00:03:39.390 --> 00:03:39.400 align:start position:0%
interconnected in a way that respects
 

00:03:39.400 --> 00:03:41.039 align:start position:0%
interconnected in a way that respects
the<00:03:39.549><c> structures</c><00:03:40.090><c> of</c><00:03:40.120><c> the</c><00:03:40.450><c> things</c><00:03:40.660><c> you</c><00:03:41.019><c> are</c>

00:03:41.039 --> 00:03:41.049 align:start position:0%
the structures of the things you are
 

00:03:41.049 --> 00:03:45.000 align:start position:0%
the structures of the things you are
connecting<00:03:42.239><c> this</c><00:03:43.239><c> means</c><00:03:43.510><c> that</c><00:03:43.780><c> if</c><00:03:44.170><c> we</c><00:03:44.410><c> build</c><00:03:44.829><c> a</c>

00:03:45.000 --> 00:03:45.010 align:start position:0%
connecting this means that if we build a
 

00:03:45.010 --> 00:03:46.500 align:start position:0%
connecting this means that if we build a
categorical<00:03:45.430><c> correspondence</c><00:03:46.329><c> between</c>

00:03:46.500 --> 00:03:46.510 align:start position:0%
categorical correspondence between
 

00:03:46.510 --> 00:03:49.259 align:start position:0%
categorical correspondence between
graphs<00:03:47.109><c> and</c><00:03:47.410><c> boolean</c><00:03:47.680><c> circuits</c><00:03:48.250><c> then</c><00:03:48.970><c> we</c><00:03:49.090><c> can</c>

00:03:49.259 --> 00:03:49.269 align:start position:0%
graphs and boolean circuits then we can
 

00:03:49.269 --> 00:03:52.080 align:start position:0%
graphs and boolean circuits then we can
be<00:03:49.390><c> sure</c><00:03:49.660><c> that</c><00:03:50.049><c> if</c><00:03:50.290><c> we</c><00:03:50.590><c> morph</c><00:03:50.920><c> the</c><00:03:51.220><c> graph</c><00:03:51.459><c> the</c>

00:03:52.080 --> 00:03:52.090 align:start position:0%
be sure that if we morph the graph the
 

00:03:52.090 --> 00:03:55.069 align:start position:0%
be sure that if we morph the graph the
circuit<00:03:52.480><c> will</c><00:03:52.690><c> morph</c><00:03:52.959><c> accordingly</c><00:03:53.530><c> and</c>

00:03:55.069 --> 00:03:55.079 align:start position:0%
circuit will morph accordingly and
 

00:03:55.079 --> 00:03:58.949 align:start position:0%
circuit will morph accordingly and
moreover<00:03:56.160><c> once</c><00:03:57.160><c> you</c><00:03:57.640><c> category</c><00:03:58.150><c> FIA</c><00:03:58.359><c> concept</c>

00:03:58.949 --> 00:03:58.959 align:start position:0%
moreover once you category FIA concept
 

00:03:58.959 --> 00:04:00.690 align:start position:0%
moreover once you category FIA concept
you<00:03:59.079><c> automatically</c><00:03:59.739><c> connect</c><00:04:00.190><c> it</c><00:04:00.400><c> to</c><00:04:00.579><c> the</c>

00:04:00.690 --> 00:04:00.700 align:start position:0%
you automatically connect it to the
 

00:04:00.700 --> 00:04:04.319 align:start position:0%
you automatically connect it to the
whole<00:04:00.880><c> of</c><00:04:00.910><c> mathematics</c><00:04:02.370><c> and</c><00:04:03.370><c> this</c><00:04:03.940><c> basically</c>

00:04:04.319 --> 00:04:04.329 align:start position:0%
whole of mathematics and this basically
 

00:04:04.329 --> 00:04:07.110 align:start position:0%
whole of mathematics and this basically
means<00:04:04.600><c> that</c><00:04:04.810><c> now</c><00:04:05.500><c> if</c><00:04:06.190><c> you</c><00:04:06.459><c> have</c><00:04:06.579><c> a</c><00:04:06.609><c> categorical</c>

00:04:07.110 --> 00:04:07.120 align:start position:0%
means that now if you have a categorical
 

00:04:07.120 --> 00:04:09.120 align:start position:0%
means that now if you have a categorical
correspondence<00:04:07.989><c> between</c><00:04:08.140><c> whatever</c><00:04:08.739><c> you</c><00:04:08.950><c> like</c>

00:04:09.120 --> 00:04:09.130 align:start position:0%
correspondence between whatever you like
 

00:04:09.130 --> 00:04:12.270 align:start position:0%
correspondence between whatever you like
to<00:04:09.640><c> graphs</c><00:04:09.959><c> then</c><00:04:10.959><c> you</c><00:04:11.109><c> will</c><00:04:11.260><c> be</c><00:04:11.380><c> able</c><00:04:11.709><c> to</c><00:04:11.890><c> pipe</c>

00:04:12.270 --> 00:04:12.280 align:start position:0%
to graphs then you will be able to pipe
 

00:04:12.280 --> 00:04:14.759 align:start position:0%
to graphs then you will be able to pipe
this<00:04:12.579><c> correspondence</c><00:04:13.450><c> inside</c><00:04:14.019><c> the</c><00:04:14.410><c> thing</c><00:04:14.620><c> we</c>

00:04:14.759 --> 00:04:14.769 align:start position:0%
this correspondence inside the thing we
 

00:04:14.769 --> 00:04:16.949 align:start position:0%
this correspondence inside the thing we
are<00:04:14.829><c> doing</c><00:04:15.220><c> and</c><00:04:15.459><c> get</c><00:04:15.670><c> automatically</c><00:04:16.329><c> that</c>

00:04:16.949 --> 00:04:16.959 align:start position:0%
are doing and get automatically that
 

00:04:16.959 --> 00:04:19.529 align:start position:0%
are doing and get automatically that
case<00:04:17.169><c> narks</c><00:04:17.560><c> out</c><00:04:17.739><c> of</c><00:04:17.859><c> it</c><00:04:18.120><c> so</c><00:04:19.120><c> this</c><00:04:19.269><c> is</c><00:04:19.419><c> an</c>

00:04:19.529 --> 00:04:19.539 align:start position:0%
case narks out of it so this is an
 

00:04:19.539 --> 00:04:23.909 align:start position:0%
case narks out of it so this is an
example<00:04:21.270><c> with</c><00:04:22.270><c> each</c><00:04:22.389><c> graph</c><00:04:22.750><c> G</c><00:04:23.110><c> you</c><00:04:23.350><c> can</c><00:04:23.590><c> build</c>

00:04:23.909 --> 00:04:23.919 align:start position:0%
example with each graph G you can build
 

00:04:23.919 --> 00:04:25.580 align:start position:0%
example with each graph G you can build
a<00:04:24.160><c> free</c><00:04:24.370><c> category</c>

00:04:25.580 --> 00:04:25.590 align:start position:0%
a free category
 

00:04:25.590 --> 00:04:29.040 align:start position:0%
a free category
free<00:04:26.590><c> of</c><00:04:26.740><c> G</c><00:04:27.390><c> this</c><00:04:28.390><c> free</c><00:04:28.659><c> khattak</c><00:04:28.960><c> will</c>

00:04:29.040 --> 00:04:29.050 align:start position:0%
free of G this free khattak will
 

00:04:29.050 --> 00:04:30.719 align:start position:0%
free of G this free khattak will
represent<00:04:29.380><c> all</c><00:04:29.710><c> the</c><00:04:29.800><c> possible</c><00:04:29.919><c> paths</c><00:04:30.460><c> in</c><00:04:30.640><c> the</c>

00:04:30.719 --> 00:04:30.729 align:start position:0%
represent all the possible paths in the
 

00:04:30.729 --> 00:04:31.730 align:start position:0%
represent all the possible paths in the
graph<00:04:30.760><c> so</c><00:04:31.180><c> the</c><00:04:31.390><c> posse</c>

00:04:31.730 --> 00:04:31.740 align:start position:0%
graph so the posse
 

00:04:31.740 --> 00:04:33.470 align:start position:0%
graph so the posse
lawful<00:04:32.040><c> computations</c><00:04:32.880><c> were</c><00:04:33.060><c> interested</c>

00:04:33.470 --> 00:04:33.480 align:start position:0%
lawful computations were interested
 

00:04:33.480 --> 00:04:35.450 align:start position:0%
lawful computations were interested
about<00:04:33.690><c> and</c><00:04:34.260><c> you</c><00:04:34.380><c> know</c><00:04:34.500><c> this</c><00:04:34.740><c> is</c><00:04:34.920><c> a</c><00:04:34.950><c> community</c>

00:04:35.450 --> 00:04:35.460 align:start position:0%
about and you know this is a community
 

00:04:35.460 --> 00:04:37.130 align:start position:0%
about and you know this is a community
square<00:04:35.850><c> which</c><00:04:36.180><c> is</c><00:04:36.390><c> the</c><00:04:36.540><c> very</c><00:04:36.690><c> heart</c><00:04:37.020><c> of</c>

00:04:37.130 --> 00:04:37.140 align:start position:0%
square which is the very heart of
 

00:04:37.140 --> 00:04:39.620 align:start position:0%
square which is the very heart of
category<00:04:37.650><c> theory</c><00:04:38.010><c> and</c><00:04:38.220><c> what</c><00:04:39.000><c> it</c><00:04:39.120><c> means</c><00:04:39.300><c> is</c>

00:04:39.620 --> 00:04:39.630 align:start position:0%
category theory and what it means is
 

00:04:39.630 --> 00:04:42.200 align:start position:0%
category theory and what it means is
that<00:04:39.660><c> if</c><00:04:40.020><c> you</c><00:04:40.110><c> have</c><00:04:40.200><c> an</c><00:04:40.320><c> F</c><00:04:40.620><c> that</c><00:04:41.280><c> morphs</c><00:04:41.880><c> your</c>

00:04:42.200 --> 00:04:42.210 align:start position:0%
that if you have an F that morphs your
 

00:04:42.210 --> 00:04:44.990 align:start position:0%
that if you have an F that morphs your
graph<00:04:42.480><c> G</c><00:04:42.810><c> to</c><00:04:43.410><c> a</c><00:04:43.440><c> graph</c><00:04:43.710><c> G</c><00:04:43.980><c> prime</c><00:04:44.280><c> then</c><00:04:44.970><c> you</c>

00:04:44.990 --> 00:04:45.000 align:start position:0%
graph G to a graph G prime then you
 

00:04:45.000 --> 00:04:47.330 align:start position:0%
graph G to a graph G prime then you
obtain<00:04:45.300><c> automatically</c><00:04:46.170><c> a</c><00:04:46.200><c> way</c><00:04:46.440><c> to</c><00:04:46.500><c> morph</c><00:04:47.220><c> the</c>

00:04:47.330 --> 00:04:47.340 align:start position:0%
obtain automatically a way to morph the
 

00:04:47.340 --> 00:04:50.210 align:start position:0%
obtain automatically a way to morph the
corresponding<00:04:48.120><c> categories</c><00:04:48.660><c> and</c><00:04:49.020><c> if</c><00:04:49.830><c> you</c><00:04:49.980><c> map</c>

00:04:50.210 --> 00:04:50.220 align:start position:0%
corresponding categories and if you map
 

00:04:50.220 --> 00:04:52.820 align:start position:0%
corresponding categories and if you map
the<00:04:50.610><c> graph</c><00:04:50.850><c> G</c><00:04:51.240><c> to</c><00:04:51.570><c> the</c><00:04:51.690><c> free</c><00:04:51.960><c> category</c><00:04:52.440><c> and</c>

00:04:52.820 --> 00:04:52.830 align:start position:0%
the graph G to the free category and
 

00:04:52.830 --> 00:04:54.940 align:start position:0%
the graph G to the free category and
then<00:04:53.010><c> you</c><00:04:53.190><c> morph</c><00:04:53.460><c> does</c><00:04:53.940><c> the</c><00:04:54.120><c> same</c><00:04:54.420><c> of</c>

00:04:54.940 --> 00:04:54.950 align:start position:0%
then you morph does the same of
 

00:04:54.950 --> 00:04:57.860 align:start position:0%
then you morph does the same of
morphine's<00:04:55.950><c> morphing</c><00:04:56.880><c> the</c><00:04:57.000><c> graph</c><00:04:57.210><c> first</c><00:04:57.510><c> and</c>

00:04:57.860 --> 00:04:57.870 align:start position:0%
morphine's morphing the graph first and
 

00:04:57.870 --> 00:05:00.770 align:start position:0%
morphine's morphing the graph first and
then<00:04:58.590><c> doing</c><00:04:59.310><c> the</c><00:04:59.520><c> free</c><00:04:59.700><c> category</c><00:05:00.180><c> so</c><00:05:00.480><c> these</c>

00:05:00.770 --> 00:05:00.780 align:start position:0%
then doing the free category so these
 

00:05:00.780 --> 00:05:03.350 align:start position:0%
then doing the free category so these
square<00:05:01.140><c> commutes</c><00:05:01.440><c> it</c><00:05:01.890><c> doesn't</c><00:05:02.220><c> matter</c><00:05:02.430><c> which</c>

00:05:03.350 --> 00:05:03.360 align:start position:0%
square commutes it doesn't matter which
 

00:05:03.360 --> 00:05:05.810 align:start position:0%
square commutes it doesn't matter which
path<00:05:03.660><c> you</c><00:05:03.720><c> take</c><00:05:03.930><c> you</c><00:05:04.440><c> can</c><00:05:04.620><c> go</c><00:05:04.800><c> from</c><00:05:05.040><c> G</c><00:05:05.310><c> to</c><00:05:05.340><c> free</c>

00:05:05.810 --> 00:05:05.820 align:start position:0%
path you take you can go from G to free
 

00:05:05.820 --> 00:05:09.740 align:start position:0%
path you take you can go from G to free
of<00:05:05.940><c> G</c><00:05:06.120><c> prime</c><00:05:06.300><c> using</c><00:05:07.260><c> both</c><00:05:07.470><c> paths</c><00:05:08.390><c> so</c><00:05:09.390><c> what</c><00:05:09.570><c> we</c>

00:05:09.740 --> 00:05:09.750 align:start position:0%
of G prime using both paths so what we
 

00:05:09.750 --> 00:05:12.200 align:start position:0%
of G prime using both paths so what we
do<00:05:09.900><c> is</c><00:05:10.080><c> this</c><00:05:10.290><c> we</c><00:05:11.220><c> can</c><00:05:11.430><c> basically</c><00:05:11.610><c> use</c><00:05:11.970><c> the</c>

00:05:12.200 --> 00:05:12.210 align:start position:0%
do is this we can basically use the
 

00:05:12.210 --> 00:05:14.570 align:start position:0%
do is this we can basically use the
adjacency<00:05:12.840><c> matrix</c><00:05:13.230><c> of</c><00:05:13.470><c> the</c><00:05:14.340><c> graph</c>

00:05:14.570 --> 00:05:14.580 align:start position:0%
adjacency matrix of the graph
 

00:05:14.580 --> 00:05:17.570 align:start position:0%
adjacency matrix of the graph
corresponding<00:05:14.790><c> to</c><00:05:15.450><c> the</c><00:05:15.690><c> EFSM</c><00:05:16.070><c> to</c><00:05:17.070><c> build</c><00:05:17.400><c> a</c>

00:05:17.570 --> 00:05:17.580 align:start position:0%
corresponding to the EFSM to build a
 

00:05:17.580 --> 00:05:20.000 align:start position:0%
corresponding to the EFSM to build a
circuit<00:05:18.090><c> in</c><00:05:18.690><c> this</c><00:05:18.900><c> circuit</c><00:05:19.260><c> you</c><00:05:19.290><c> see</c><00:05:19.650><c> you</c>

00:05:20.000 --> 00:05:20.010 align:start position:0%
circuit in this circuit you see you
 

00:05:20.010 --> 00:05:22.280 align:start position:0%
circuit in this circuit you see you
basically<00:05:20.460><c> plug</c><00:05:20.880><c> in</c><00:05:21.210><c> an</c><00:05:21.450><c> enumeration</c><00:05:21.990><c> of</c><00:05:22.230><c> a</c>

00:05:22.280 --> 00:05:22.290 align:start position:0%
basically plug in an enumeration of a
 

00:05:22.290 --> 00:05:26.060 align:start position:0%
basically plug in an enumeration of a
vertex<00:05:22.680><c> on</c><00:05:23.040><c> the</c><00:05:23.370><c> left</c><00:05:23.670><c> and</c><00:05:24.000><c> an</c><00:05:24.300><c> edge</c><00:05:24.510><c> and</c><00:05:25.070><c> this</c>

00:05:26.060 --> 00:05:26.070 align:start position:0%
vertex on the left and an edge and this
 

00:05:26.070 --> 00:05:29.480 align:start position:0%
vertex on the left and an edge and this
circuit<00:05:26.490><c> will</c><00:05:26.700><c> give</c><00:05:26.940><c> you</c><00:05:27.590><c> 0</c><00:05:28.590><c> or</c><00:05:28.890><c> 1</c><00:05:29.190><c> depending</c>

00:05:29.480 --> 00:05:29.490 align:start position:0%
circuit will give you 0 or 1 depending
 

00:05:29.490 --> 00:05:33.560 align:start position:0%
circuit will give you 0 or 1 depending
if<00:05:30.210><c> the</c><00:05:31.080><c> vertex</c><00:05:31.440><c> you</c><00:05:31.590><c> plugged</c><00:05:31.860><c> in</c><00:05:32.130><c> is</c><00:05:32.570><c> the</c>

00:05:33.560 --> 00:05:33.570 align:start position:0%
if the vertex you plugged in is the
 

00:05:33.570 --> 00:05:35.810 align:start position:0%
if the vertex you plugged in is the
starting<00:05:34.140><c> vertex</c><00:05:34.320><c> of</c><00:05:34.710><c> the</c><00:05:34.890><c> edge</c><00:05:35.010><c> and</c><00:05:35.400><c> it</c><00:05:35.610><c> will</c>

00:05:35.810 --> 00:05:35.820 align:start position:0%
starting vertex of the edge and it will
 

00:05:35.820 --> 00:05:39.200 align:start position:0%
starting vertex of the edge and it will
give<00:05:35.970><c> you</c><00:05:36.060><c> the</c><00:05:36.210><c> next</c><00:05:36.890><c> vertex</c><00:05:37.890><c> so</c><00:05:38.340><c> if</c><00:05:38.490><c> X</c><00:05:38.790><c> to</c><00:05:39.060><c> the</c>

00:05:39.200 --> 00:05:39.210 align:start position:0%
give you the next vertex so if X to the
 

00:05:39.210 --> 00:05:42.830 align:start position:0%
give you the next vertex so if X to the
e<00:05:39.410><c> is</c><00:05:40.410><c> a</c><00:05:40.470><c> thing</c><00:05:41.340><c> that</c><00:05:41.370><c> goes</c><00:05:41.730><c> from</c><00:05:41.970><c> A</c><00:05:42.150><c> to</c><00:05:42.180><c> B</c><00:05:42.390><c> and</c>

00:05:42.830 --> 00:05:42.840 align:start position:0%
e is a thing that goes from A to B and
 

00:05:42.840 --> 00:05:46.070 align:start position:0%
e is a thing that goes from A to B and
you<00:05:42.990><c> plug</c><00:05:43.470><c> a</c><00:05:43.710><c> on</c><00:05:44.250><c> the</c><00:05:44.700><c> left</c><00:05:44.880><c> on</c><00:05:45.060><c> XV</c><00:05:45.480><c> then</c><00:05:45.930><c> you</c>

00:05:46.070 --> 00:05:46.080 align:start position:0%
you plug a on the left on XV then you
 

00:05:46.080 --> 00:05:49.940 align:start position:0%
you plug a on the left on XV then you
get<00:05:46.290><c> one</c><00:05:46.980><c> and</c><00:05:47.250><c> B</c><00:05:48.090><c> on</c><00:05:48.330><c> the</c><00:05:48.390><c> other</c><00:05:48.690><c> side</c><00:05:49.080><c> now</c><00:05:49.890><c> we</c>

00:05:49.940 --> 00:05:49.950 align:start position:0%
get one and B on the other side now we
 

00:05:49.950 --> 00:05:54.370 align:start position:0%
get one and B on the other side now we
can<00:05:50.310><c> connect</c><00:05:50.850><c> these</c><00:05:50.970><c> things</c><00:05:51.180><c> together</c><00:05:53.060><c> and</c>

00:05:54.370 --> 00:05:54.380 align:start position:0%
can connect these things together and
 

00:05:54.380 --> 00:05:58.130 align:start position:0%
can connect these things together and
this<00:05:55.380><c> is</c><00:05:55.440><c> exactly</c><00:05:55.800><c> what</c><00:05:56.580><c> this</c><00:05:57.270><c> tree</c><00:05:57.600><c> category</c>

00:05:58.130 --> 00:05:58.140 align:start position:0%
this is exactly what this tree category
 

00:05:58.140 --> 00:06:01.160 align:start position:0%
this is exactly what this tree category
will<00:05:59.010><c> do</c><00:05:59.250><c> so</c><00:05:59.460><c> we</c><00:05:59.610><c> can</c><00:05:59.790><c> map</c><00:06:00.000><c> now</c><00:06:00.270><c> everything</c><00:06:01.050><c> in</c>

00:06:01.160 --> 00:06:01.170 align:start position:0%
will do so we can map now everything in
 

00:06:01.170 --> 00:06:04.060 align:start position:0%
will do so we can map now everything in
this<00:06:01.260><c> tree</c><00:06:01.500><c> category</c><00:06:02.010><c> to</c><00:06:02.250><c> a</c><00:06:02.490><c> piping</c><00:06:03.390><c> of</c><00:06:03.630><c> this</c>

00:06:04.060 --> 00:06:04.070 align:start position:0%
this tree category to a piping of this
 

00:06:04.070 --> 00:06:07.100 align:start position:0%
this tree category to a piping of this
modular<00:06:05.070><c> circuits</c><00:06:05.610><c> basically</c><00:06:06.150><c> but</c><00:06:06.690><c> we</c><00:06:06.810><c> can</c><00:06:06.960><c> do</c>

00:06:07.100 --> 00:06:07.110 align:start position:0%
modular circuits basically but we can do
 

00:06:07.110 --> 00:06:09.230 align:start position:0%
modular circuits basically but we can do
more<00:06:07.140><c> we</c><00:06:07.470><c> can</c><00:06:07.620><c> obstruct</c><00:06:08.160><c> the</c><00:06:08.520><c> adjacency</c>

00:06:09.230 --> 00:06:09.240 align:start position:0%
more we can obstruct the adjacency
 

00:06:09.240 --> 00:06:11.450 align:start position:0%
more we can obstruct the adjacency
matrix<00:06:09.390><c> which</c><00:06:10.050><c> at</c><00:06:10.290><c> the</c><00:06:10.410><c> moment</c><00:06:10.440><c> is</c><00:06:10.740><c> encoded</c><00:06:11.280><c> in</c>

00:06:11.450 --> 00:06:11.460 align:start position:0%
matrix which at the moment is encoded in
 

00:06:11.460 --> 00:06:14.900 align:start position:0%
matrix which at the moment is encoded in
these<00:06:11.670><c> s</c><00:06:11.910><c> of</c><00:06:12.150><c> G</c><00:06:12.360><c> and</c><00:06:12.540><c> T</c><00:06:12.780><c> of</c><00:06:12.900><c> G</c><00:06:13.280><c> like</c><00:06:14.280><c> this</c><00:06:14.550><c> and</c>

00:06:14.900 --> 00:06:14.910 align:start position:0%
these s of G and T of G like this and
 

00:06:14.910 --> 00:06:16.700 align:start position:0%
these s of G and T of G like this and
now<00:06:15.060><c> the</c><00:06:15.120><c> idea</c><00:06:15.480><c> is</c><00:06:15.540><c> that</c><00:06:15.570><c> in</c><00:06:15.960><c> this</c><00:06:16.170><c> densely</c>

00:06:16.700 --> 00:06:16.710 align:start position:0%
now the idea is that in this densely
 

00:06:16.710 --> 00:06:19.160 align:start position:0%
now the idea is that in this densely
dotted<00:06:17.220><c> wire</c><00:06:17.430><c> you</c><00:06:18.000><c> can</c><00:06:18.150><c> also</c><00:06:18.330><c> specify</c><00:06:18.810><c> the</c>

00:06:19.160 --> 00:06:19.170 align:start position:0%
dotted wire you can also specify the
 

00:06:19.170 --> 00:06:21.350 align:start position:0%
dotted wire you can also specify the
adjacency<00:06:19.890><c> matrix</c><00:06:20.010><c> of</c><00:06:20.430><c> the</c><00:06:20.610><c> graph</c><00:06:20.640><c> you</c><00:06:20.880><c> want</c>

00:06:21.350 --> 00:06:21.360 align:start position:0%
adjacency matrix of the graph you want
 

00:06:21.360 --> 00:06:25.030 align:start position:0%
adjacency matrix of the graph you want
to<00:06:21.540><c> use</c><00:06:22.200><c> so</c><00:06:22.860><c> now</c><00:06:23.010><c> you</c><00:06:23.070><c> are</c><00:06:23.220><c> plugging</c><00:06:23.670><c> in</c><00:06:23.850><c> the</c>

00:06:25.030 --> 00:06:25.040 align:start position:0%
to use so now you are plugging in the
 

00:06:25.040 --> 00:06:28.250 align:start position:0%
to use so now you are plugging in the
vertex<00:06:26.040><c> and</c><00:06:26.280><c> edge</c><00:06:26.400><c> and</c><00:06:26.760><c> also</c><00:06:26.910><c> the</c><00:06:27.210><c> graph</c><00:06:27.540><c> the</c>

00:06:28.250 --> 00:06:28.260 align:start position:0%
vertex and edge and also the graph the
 

00:06:28.260 --> 00:06:33.530 align:start position:0%
vertex and edge and also the graph the
vertex<00:06:28.530><c> and</c><00:06:28.770><c> the</c><00:06:28.860><c> edge</c><00:06:28.950><c> belong</c><00:06:29.370><c> to</c><00:06:32.090><c> so</c><00:06:33.090><c> again</c>

00:06:33.530 --> 00:06:33.540 align:start position:0%
vertex and the edge belong to so again
 

00:06:33.540 --> 00:06:35.780 align:start position:0%
vertex and the edge belong to so again
all<00:06:33.750><c> these</c><00:06:33.960><c> things</c><00:06:34.020><c> are</c><00:06:34.350><c> composable</c><00:06:34.950><c> and</c><00:06:35.310><c> you</c>

00:06:35.780 --> 00:06:35.790 align:start position:0%
all these things are composable and you
 

00:06:35.790 --> 00:06:38.510 align:start position:0%
all these things are composable and you
can<00:06:36.000><c> basically</c><00:06:36.180><c> obtain</c><00:06:36.960><c> a</c><00:06:37.290><c> functor</c><00:06:37.830><c> that</c><00:06:38.310><c> goes</c>

00:06:38.510 --> 00:06:38.520 align:start position:0%
can basically obtain a functor that goes
 

00:06:38.520 --> 00:06:40.910 align:start position:0%
can basically obtain a functor that goes
from<00:06:38.880><c> your</c><00:06:39.630><c> free</c><00:06:39.930><c> categories</c><00:06:40.500><c> to</c><00:06:40.770><c> these</c>

00:06:40.910 --> 00:06:40.920 align:start position:0%
from your free categories to these
 

00:06:40.920 --> 00:06:43.940 align:start position:0%
from your free categories to these
circuits<00:06:41.910><c> this</c><00:06:42.630><c> means</c><00:06:42.960><c> that</c><00:06:43.200><c> you</c><00:06:43.800><c> are</c>

00:06:43.940 --> 00:06:43.950 align:start position:0%
circuits this means that you are
 

00:06:43.950 --> 00:06:44.910 align:start position:0%
circuits this means that you are
basically<00:06:44.460><c> a</c><00:06:44.550><c> cat</c>

00:06:44.910 --> 00:06:44.920 align:start position:0%
basically a cat
 

00:06:44.920 --> 00:06:47.730 align:start position:0%
basically a cat
Oracle<00:06:45.340><c> way</c><00:06:45.550><c> to</c><00:06:45.610><c> map</c><00:06:46.240><c> a</c><00:06:46.540><c> fun</c><00:06:46.750><c> estate</c><00:06:47.050><c> machine</c>

00:06:47.730 --> 00:06:47.740 align:start position:0%
Oracle way to map a fun estate machine
 

00:06:47.740 --> 00:06:50.700 align:start position:0%
Oracle way to map a fun estate machine
to<00:06:48.300><c> discard</c><00:06:49.300><c> with</c><00:06:49.630><c> boolean</c><00:06:49.900><c> circuits</c><00:06:50.410><c> and</c>

00:06:50.700 --> 00:06:50.710 align:start position:0%
to discard with boolean circuits and
 

00:06:50.710 --> 00:06:53.160 align:start position:0%
to discard with boolean circuits and
everything<00:06:51.610><c> we</c><00:06:51.730><c> built</c><00:06:51.970><c> is</c><00:06:52.150><c> compositional</c><00:06:52.930><c> so</c>

00:06:53.160 --> 00:06:53.170 align:start position:0%
everything we built is compositional so
 

00:06:53.170 --> 00:06:56.550 align:start position:0%
everything we built is compositional so
basically<00:06:54.030><c> you</c><00:06:55.030><c> see</c><00:06:55.240><c> in</c><00:06:55.480><c> this</c><00:06:55.660><c> huge</c><00:06:55.930><c> diagram</c>

00:06:56.550 --> 00:06:56.560 align:start position:0%
basically you see in this huge diagram
 

00:06:56.560 --> 00:07:00.930 align:start position:0%
basically you see in this huge diagram
you<00:06:57.070><c> start</c><00:06:57.370><c> with</c><00:06:57.550><c> graphs</c><00:06:58.140><c> on</c><00:06:59.140><c> the</c><00:06:59.350><c> left</c><00:06:59.940><c> then</c>

00:07:00.930 --> 00:07:00.940 align:start position:0%
you start with graphs on the left then
 

00:07:00.940 --> 00:07:02.940 align:start position:0%
you start with graphs on the left then
you<00:07:01.060><c> calculate</c><00:07:01.270><c> these</c><00:07:01.810><c> three</c><00:07:02.140><c> category</c><00:07:02.710><c> thing</c>

00:07:02.940 --> 00:07:02.950 align:start position:0%
you calculate these three category thing
 

00:07:02.950 --> 00:07:05.820 align:start position:0%
you calculate these three category thing
and<00:07:03.130><c> then</c><00:07:04.000><c> you</c><00:07:04.180><c> can</c><00:07:04.450><c> there</c><00:07:05.230><c> are</c><00:07:05.350><c> different</c>

00:07:05.820 --> 00:07:05.830 align:start position:0%
and then you can there are different
 

00:07:05.830 --> 00:07:07.670 align:start position:0%
and then you can there are different
kind<00:07:06.100><c> of</c><00:07:06.250><c> things</c><00:07:06.490><c> that</c><00:07:06.670><c> are</c><00:07:06.760><c> related</c><00:07:07.180><c> to</c>

00:07:07.670 --> 00:07:07.680 align:start position:0%
kind of things that are related to
 

00:07:07.680 --> 00:07:10.050 align:start position:0%
kind of things that are related to
knowledge<00:07:08.680><c> proofs</c><00:07:09.160><c> or</c><00:07:09.430><c> zero</c><00:07:09.760><c> knowledge</c><00:07:09.910><c> proof</c>

00:07:10.050 --> 00:07:10.060 align:start position:0%
knowledge proofs or zero knowledge proof
 

00:07:10.060 --> 00:07:14.190 align:start position:0%
knowledge proofs or zero knowledge proof
and<00:07:10.570><c> the</c><00:07:11.290><c> idea</c><00:07:11.590><c> is</c><00:07:11.740><c> that</c><00:07:12.600><c> you</c><00:07:13.600><c> know</c><00:07:13.750><c> if</c><00:07:13.960><c> you</c>

00:07:14.190 --> 00:07:14.200 align:start position:0%
and the idea is that you know if you
 

00:07:14.200 --> 00:07:16.650 align:start position:0%
and the idea is that you know if you
morph<00:07:14.500><c> the</c><00:07:14.740><c> graph</c><00:07:14.950><c> down</c><00:07:15.250><c> there</c><00:07:15.610><c> you</c><00:07:16.480><c> can</c>

00:07:16.650 --> 00:07:16.660 align:start position:0%
morph the graph down there you can
 

00:07:16.660 --> 00:07:19.470 align:start position:0%
morph the graph down there you can
basically<00:07:16.840><c> prover</c><00:07:17.530><c> s--</c><00:07:17.700><c> this</c><00:07:18.700><c> diagram</c><00:07:19.210><c> in</c><00:07:19.330><c> any</c>

00:07:19.470 --> 00:07:19.480 align:start position:0%
basically prover s-- this diagram in any
 

00:07:19.480 --> 00:07:21.450 align:start position:0%
basically prover s-- this diagram in any
way<00:07:19.720><c> you</c><00:07:19.780><c> want</c><00:07:20.140><c> it</c><00:07:20.410><c> doesn't</c><00:07:20.830><c> matter</c><00:07:21.040><c> which</c>

00:07:21.450 --> 00:07:21.460 align:start position:0%
way you want it doesn't matter which
 

00:07:21.460 --> 00:07:23.430 align:start position:0%
way you want it doesn't matter which
path<00:07:21.760><c> you</c><00:07:21.820><c> take</c><00:07:22.270><c> the</c><00:07:22.960><c> only</c><00:07:23.050><c> thing</c><00:07:23.170><c> that</c>

00:07:23.430 --> 00:07:23.440 align:start position:0%
path you take the only thing that
 

00:07:23.440 --> 00:07:25.920 align:start position:0%
path you take the only thing that
matters<00:07:23.860><c> is</c><00:07:24.160><c> what</c><00:07:24.880><c> is</c><00:07:25.000><c> your</c><00:07:25.270><c> starting</c><00:07:25.690><c> point</c>

00:07:25.920 --> 00:07:25.930 align:start position:0%
matters is what is your starting point
 

00:07:25.930 --> 00:07:29.010 align:start position:0%
matters is what is your starting point
and<00:07:26.200><c> your</c><00:07:26.860><c> end</c><00:07:27.160><c> point</c><00:07:27.460><c> and</c><00:07:27.730><c> is</c><00:07:28.390><c> exactly</c><00:07:28.630><c> what</c>

00:07:29.010 --> 00:07:29.020 align:start position:0%
and your end point and is exactly what
 

00:07:29.020 --> 00:07:32.310 align:start position:0%
and your end point and is exactly what
category<00:07:29.530><c> theory</c><00:07:29.830><c> is</c><00:07:29.950><c> about</c><00:07:31.230><c> so</c><00:07:32.230><c> the</c>

00:07:32.310 --> 00:07:32.320 align:start position:0%
category theory is about so the
 

00:07:32.320 --> 00:07:34.500 align:start position:0%
category theory is about so the
take-home<00:07:32.560><c> message</c><00:07:33.310><c> of</c><00:07:33.490><c> this</c><00:07:33.610><c> dope</c><00:07:33.910><c> is</c><00:07:34.180><c> this</c>

00:07:34.500 --> 00:07:34.510 align:start position:0%
take-home message of this dope is this
 

00:07:34.510 --> 00:07:37.530 align:start position:0%
take-home message of this dope is this
if<00:07:35.200><c> you</c><00:07:35.860><c> build</c><00:07:36.280><c> things</c><00:07:36.550><c> categorically</c>

00:07:37.530 --> 00:07:37.540 align:start position:0%
if you build things categorically
 

00:07:37.540 --> 00:07:40.110 align:start position:0%
if you build things categorically
there's<00:07:38.140><c> a</c><00:07:38.230><c> good</c><00:07:38.410><c> chance</c><00:07:38.710><c> that</c><00:07:39.130><c> they</c><00:07:39.820><c> will</c><00:07:39.970><c> be</c>

00:07:40.110 --> 00:07:40.120 align:start position:0%
there's a good chance that they will be
 

00:07:40.120 --> 00:07:42.900 align:start position:0%
there's a good chance that they will be
formally<00:07:40.600><c> correct</c><00:07:40.990><c> because</c><00:07:41.980><c> category</c><00:07:42.580><c> theory</c>

00:07:42.900 --> 00:07:42.910 align:start position:0%
formally correct because category theory
 

00:07:42.910 --> 00:07:45.540 align:start position:0%
formally correct because category theory
is<00:07:43.120><c> all</c><00:07:43.390><c> about</c><00:07:43.660><c> structure</c><00:07:44.050><c> and</c><00:07:44.320><c> when</c><00:07:45.250><c> you</c><00:07:45.460><c> are</c>

00:07:45.540 --> 00:07:45.550 align:start position:0%
is all about structure and when you are
 

00:07:45.550 --> 00:07:48.090 align:start position:0%
is all about structure and when you are
able<00:07:45.850><c> to</c><00:07:46.000><c> express</c><00:07:46.560><c> some</c><00:07:47.560><c> concept</c>

00:07:48.090 --> 00:07:48.100 align:start position:0%
able to express some concept
 

00:07:48.100 --> 00:07:51.540 align:start position:0%
able to express some concept
categorically<00:07:48.990><c> then</c><00:07:49.990><c> the</c><00:07:50.440><c> concept</c><00:07:50.800><c> will</c><00:07:51.040><c> be</c>

00:07:51.540 --> 00:07:51.550 align:start position:0%
categorically then the concept will be
 

00:07:51.550 --> 00:07:54.900 align:start position:0%
categorically then the concept will be
correct<00:07:52.000><c> and</c><00:07:52.210><c> type</c><00:07:52.450><c> check</c><00:07:52.780><c> by</c><00:07:53.050><c> definition</c><00:07:53.910><c> you</c>

00:07:54.900 --> 00:07:54.910 align:start position:0%
correct and type check by definition you
 

00:07:54.910 --> 00:07:56.190 align:start position:0%
correct and type check by definition you
can<00:07:55.060><c> think</c><00:07:55.240><c> about</c><00:07:55.360><c> category</c><00:07:55.840><c> theory</c><00:07:56.080><c> is</c>

00:07:56.190 --> 00:07:56.200 align:start position:0%
can think about category theory is
 

00:07:56.200 --> 00:07:58.230 align:start position:0%
can think about category theory is
really<00:07:56.470><c> like</c><00:07:56.590><c> a</c><00:07:56.770><c> semantics</c><00:07:57.340><c> for</c><00:07:57.460><c> type</c><00:07:57.820><c> theory</c>

00:07:58.230 --> 00:07:58.240 align:start position:0%
really like a semantics for type theory
 

00:07:58.240 --> 00:08:03.750 align:start position:0%
really like a semantics for type theory
if<00:07:58.300><c> you</c><00:07:58.450><c> want</c><00:08:00.690><c> then</c><00:08:01.690><c> you</c><00:08:02.350><c> will</c><00:08:02.560><c> be</c><00:08:02.740><c> able</c><00:08:03.040><c> to</c>

00:08:03.750 --> 00:08:03.760 align:start position:0%
if you want then you will be able to
 

00:08:03.760 --> 00:08:05.880 align:start position:0%
if you want then you will be able to
verify<00:08:03.940><c> that</c><00:08:04.330><c> your</c><00:08:04.480><c> constructions</c><00:08:05.230><c> satisfy</c>

00:08:05.880 --> 00:08:05.890 align:start position:0%
verify that your constructions satisfy
 

00:08:05.890 --> 00:08:07.800 align:start position:0%
verify that your constructions satisfy
some<00:08:06.220><c> nice</c><00:08:06.430><c> properties</c><00:08:07.030><c> and</c><00:08:07.270><c> this</c><00:08:07.360><c> is</c><00:08:07.510><c> because</c>

00:08:07.800 --> 00:08:07.810 align:start position:0%
some nice properties and this is because
 

00:08:07.810 --> 00:08:10.170 align:start position:0%
some nice properties and this is because
categories<00:08:08.320><c> are</c><00:08:08.440><c> very</c><00:08:08.650><c> structured</c><00:08:09.010><c> so</c><00:08:09.880><c> once</c>

00:08:10.170 --> 00:08:10.180 align:start position:0%
categories are very structured so once
 

00:08:10.180 --> 00:08:12.300 align:start position:0%
categories are very structured so once
you<00:08:10.330><c> turn</c><00:08:10.510><c> something</c><00:08:10.810><c> into</c><00:08:11.440><c> categories</c><00:08:12.070><c> you</c>

00:08:12.300 --> 00:08:12.310 align:start position:0%
you turn something into categories you
 

00:08:12.310 --> 00:08:15.060 align:start position:0%
you turn something into categories you
have<00:08:12.430><c> a</c><00:08:12.460><c> plethora</c><00:08:12.850><c> of</c><00:08:13.180><c> formal</c><00:08:13.780><c> tools</c><00:08:14.050><c> that</c><00:08:14.950><c> you</c>

00:08:15.060 --> 00:08:15.070 align:start position:0%
have a plethora of formal tools that you
 

00:08:15.070 --> 00:08:18.360 align:start position:0%
have a plethora of formal tools that you
can<00:08:15.280><c> use</c><00:08:15.490><c> to</c><00:08:15.850><c> verify</c><00:08:16.530><c> the</c><00:08:17.530><c> your</c><00:08:17.740><c> constructions</c>

00:08:18.360 --> 00:08:18.370 align:start position:0%
can use to verify the your constructions
 

00:08:18.370 --> 00:08:24.240 align:start position:0%
can use to verify the your constructions
of<00:08:18.550><c> some</c><00:08:18.730><c> properties</c><00:08:20.760><c> and</c><00:08:22.020><c> they</c><00:08:23.020><c> will</c><00:08:23.230><c> be</c><00:08:23.410><c> more</c>

00:08:24.240 --> 00:08:24.250 align:start position:0%
of some properties and they will be more
 

00:08:24.250 --> 00:08:25.680 align:start position:0%
of some properties and they will be more
easily<00:08:24.400><c> implementable</c><00:08:25.060><c> in</c><00:08:25.240><c> a</c><00:08:25.330><c> formally</c>

00:08:25.680 --> 00:08:25.690 align:start position:0%
easily implementable in a formally
 

00:08:25.690 --> 00:08:28.860 align:start position:0%
easily implementable in a formally
verified<00:08:25.720><c> setting</c><00:08:26.620><c> because</c><00:08:27.220><c> basically</c><00:08:28.030><c> many</c>

00:08:28.860 --> 00:08:28.870 align:start position:0%
verified setting because basically many
 

00:08:28.870 --> 00:08:30.780 align:start position:0%
verified setting because basically many
formally<00:08:29.260><c> verified</c><00:08:29.290><c> settings</c><00:08:30.010><c> are</c><00:08:30.250><c> fully</c>

00:08:30.780 --> 00:08:30.790 align:start position:0%
formally verified settings are fully
 

00:08:30.790 --> 00:08:33.000 align:start position:0%
formally verified settings are fully
functional<00:08:31.360><c> for</c><00:08:32.200><c> instance</c><00:08:32.470><c> we</c><00:08:32.650><c> are</c><00:08:32.740><c> merely</c>

00:08:33.000 --> 00:08:33.010 align:start position:0%
functional for instance we are merely
 

00:08:33.010 --> 00:08:34.950 align:start position:0%
functional for instance we are merely
using<00:08:33.460><c> idris</c><00:08:33.760><c> to</c><00:08:33.910><c> implement</c><00:08:34.330><c> this</c><00:08:34.450><c> stuff</c><00:08:34.690><c> and</c>

00:08:34.950 --> 00:08:34.960 align:start position:0%
using idris to implement this stuff and
 

00:08:34.960 --> 00:08:37.680 align:start position:0%
using idris to implement this stuff and
we<00:08:35.590><c> just</c><00:08:35.920><c> built</c><00:08:36.190><c> a</c><00:08:36.370><c> category</c><00:08:36.880><c> theory</c><00:08:37.180><c> library</c>

00:08:37.680 --> 00:08:37.690 align:start position:0%
we just built a category theory library
 

00:08:37.690 --> 00:08:39.990 align:start position:0%
we just built a category theory library
in<00:08:37.960><c> idris</c><00:08:38.290><c> we</c><00:08:38.590><c> literally</c><00:08:38.830><c> took</c><00:08:39.190><c> a</c><00:08:39.430><c> category</c>

00:08:39.990 --> 00:08:40.000 align:start position:0%
in idris we literally took a category
 

00:08:40.000 --> 00:08:42.300 align:start position:0%
in idris we literally took a category
theory<00:08:40.240><c> book</c><00:08:40.510><c> and</c><00:08:40.920><c> implemented</c><00:08:41.920><c> all</c><00:08:42.130><c> the</c>

00:08:42.300 --> 00:08:42.310 align:start position:0%
theory book and implemented all the
 

00:08:42.310 --> 00:08:45.690 align:start position:0%
theory book and implemented all the
definitions<00:08:42.940><c> with</c><00:08:43.360><c> proofs</c><00:08:43.690><c> in</c><00:08:44.040><c> in</c><00:08:45.040><c> idris</c><00:08:45.400><c> and</c>

00:08:45.690 --> 00:08:45.700 align:start position:0%
definitions with proofs in in idris and
 

00:08:45.700 --> 00:08:48.150 align:start position:0%
definitions with proofs in in idris and
then<00:08:46.240><c> you</c><00:08:46.360><c> see</c><00:08:46.810><c> that</c><00:08:46.990><c> if</c><00:08:47.170><c> you</c><00:08:47.320><c> are</c><00:08:47.410><c> able</c><00:08:47.590><c> to</c><00:08:47.920><c> you</c>

00:08:48.150 --> 00:08:48.160 align:start position:0%
then you see that if you are able to you
 

00:08:48.160 --> 00:08:50.160 align:start position:0%
then you see that if you are able to you
just<00:08:48.400><c> have</c><00:08:48.550><c> to</c><00:08:48.700><c> translate</c><00:08:49.060><c> the</c><00:08:49.570><c> theory</c><00:08:49.930><c> we</c>

00:08:50.160 --> 00:08:50.170 align:start position:0%
just have to translate the theory we
 

00:08:50.170 --> 00:08:53.550 align:start position:0%
just have to translate the theory we
developed<00:08:50.790><c> to</c><00:08:51.790><c> the</c><00:08:51.940><c> idris</c><00:08:52.180><c> library</c><00:08:52.630><c> just</c><00:08:53.260><c> is</c>

00:08:53.550 --> 00:08:53.560 align:start position:0%
developed to the idris library just is
 

00:08:53.560 --> 00:08:55.260 align:start position:0%
developed to the idris library just is
between<00:08:54.010><c> quotes</c><00:08:54.310><c> obviously</c><00:08:54.850><c> because</c><00:08:55.120><c> it's</c>

00:08:55.260 --> 00:08:55.270 align:start position:0%
between quotes obviously because it's
 

00:08:55.270 --> 00:08:56.680 align:start position:0%
between quotes obviously because it's
not<00:08:55.390><c> easy</c><00:08:55.690><c> but</c>

00:08:56.680 --> 00:08:56.690 align:start position:0%
not easy but
 

00:08:56.690 --> 00:09:00.040 align:start position:0%
not easy but
it's<00:08:57.470><c> a</c><00:08:57.740><c> very</c><00:08:58.070><c> conceptual</c><00:08:58.640><c> straight</c><00:08:59.120><c> path</c><00:08:59.450><c> to</c>

00:09:00.040 --> 00:09:00.050 align:start position:0%
it's a very conceptual straight path to
 

00:09:00.050 --> 00:09:03.790 align:start position:0%
it's a very conceptual straight path to
to<00:09:00.590><c> get</c><00:09:00.740><c> to</c><00:09:00.890><c> formal</c><00:09:01.250><c> verification</c><00:09:01.420><c> and</c><00:09:02.800><c> yeah</c>

00:09:03.790 --> 00:09:03.800 align:start position:0%
to get to formal verification and yeah
 

00:09:03.800 --> 00:09:05.470 align:start position:0%
to get to formal verification and yeah
in<00:09:04.040><c> the</c><00:09:04.190><c> end</c><00:09:04.310><c> you</c><00:09:04.460><c> will</c><00:09:04.610><c> be</c><00:09:04.730><c> able</c><00:09:04.820><c> to</c><00:09:05.000><c> link</c>

00:09:05.470 --> 00:09:05.480 align:start position:0%
in the end you will be able to link
 

00:09:05.480 --> 00:09:07.630 align:start position:0%
in the end you will be able to link
things<00:09:05.660><c> together</c><00:09:05.900><c> without</c><00:09:06.380><c> making</c><00:09:06.830><c> an</c><00:09:07.160><c> a</c><00:09:07.370><c> mess</c>

00:09:07.630 --> 00:09:07.640 align:start position:0%
things together without making an a mess
 

00:09:07.640 --> 00:09:10.000 align:start position:0%
things together without making an a mess
so<00:09:08.120><c> that's</c><00:09:09.050><c> basically</c><00:09:09.560><c> it</c>

00:09:10.000 --> 00:09:10.010 align:start position:0%
so that's basically it
 

00:09:10.010 --> 00:09:13.330 align:start position:0%
so that's basically it
so<00:09:11.000><c> yeah</c><00:09:11.360><c> category</c><00:09:11.840><c> theory</c><00:09:12.140><c> is</c><00:09:12.320><c> difficult</c><00:09:13.250><c> in</c>

00:09:13.330 --> 00:09:13.340 align:start position:0%
so yeah category theory is difficult in
 

00:09:13.340 --> 00:09:14.800 align:start position:0%
so yeah category theory is difficult in
the<00:09:13.430><c> beginning</c><00:09:13.520><c> especially</c><00:09:14.270><c> if</c><00:09:14.330><c> you</c><00:09:14.480><c> don't</c>

00:09:14.800 --> 00:09:14.810 align:start position:0%
the beginning especially if you don't
 

00:09:14.810 --> 00:09:18.540 align:start position:0%
the beginning especially if you don't
know<00:09:15.050><c> it</c><00:09:15.260><c> but</c><00:09:15.590><c> it</c><00:09:15.710><c> pays</c><00:09:15.980><c> off</c><00:09:16.280><c> big</c><00:09:16.610><c> time</c><00:09:17.000><c> as</c><00:09:17.440><c> your</c>

00:09:18.540 --> 00:09:18.550 align:start position:0%
know it but it pays off big time as your
 

00:09:18.550 --> 00:09:21.340 align:start position:0%
know it but it pays off big time as your
system<00:09:19.550><c> becomes</c><00:09:19.880><c> more</c><00:09:20.120><c> complicated</c><00:09:20.510><c> so</c><00:09:21.320><c> for</c>

00:09:21.340 --> 00:09:21.350 align:start position:0%
system becomes more complicated so for
 

00:09:21.350 --> 00:09:23.230 align:start position:0%
system becomes more complicated so for
instance<00:09:21.710><c> in</c><00:09:21.860><c> this</c><00:09:21.980><c> case</c><00:09:22.040><c> we</c><00:09:22.640><c> have</c><00:09:22.790><c> basically</c>

00:09:23.230 --> 00:09:23.240 align:start position:0%
instance in this case we have basically
 

00:09:23.240 --> 00:09:25.660 align:start position:0%
instance in this case we have basically
built<00:09:23.600><c> a</c><00:09:23.750><c> categorical</c><00:09:24.280><c> module</c><00:09:25.280><c> for</c><00:09:25.550><c> our</c>

00:09:25.660 --> 00:09:25.670 align:start position:0%
built a categorical module for our
 

00:09:25.670 --> 00:09:27.880 align:start position:0%
built a categorical module for our
infrastructure<00:09:26.240><c> a</c><00:09:26.390><c> categorical</c><00:09:26.810><c> gadget</c><00:09:27.470><c> that</c>

00:09:27.880 --> 00:09:27.890 align:start position:0%
infrastructure a categorical gadget that
 

00:09:27.890 --> 00:09:30.060 align:start position:0%
infrastructure a categorical gadget that
trans<00:09:28.160><c> graphs</c><00:09:28.550><c> into</c><00:09:29.480><c> zero</c><00:09:29.690><c> knowledge</c><00:09:29.810><c> proof</c>

00:09:30.060 --> 00:09:30.070 align:start position:0%
trans graphs into zero knowledge proof
 

00:09:30.070 --> 00:09:34.180 align:start position:0%
trans graphs into zero knowledge proof
now<00:09:31.090><c> whatever</c><00:09:32.090><c> you</c><00:09:32.300><c> are</c><00:09:32.420><c> doing</c><00:09:32.840><c> if</c><00:09:33.050><c> you</c><00:09:33.190><c> are</c>

00:09:34.180 --> 00:09:34.190 align:start position:0%
now whatever you are doing if you are
 

00:09:34.190 --> 00:09:36.340 align:start position:0%
now whatever you are doing if you are
able<00:09:34.490><c> to</c><00:09:34.700><c> translate</c><00:09:35.420><c> the</c><00:09:35.810><c> stuff</c><00:09:36.050><c> you</c><00:09:36.170><c> care</c>

00:09:36.340 --> 00:09:36.350 align:start position:0%
able to translate the stuff you care
 

00:09:36.350 --> 00:09:38.650 align:start position:0%
able to translate the stuff you care
about<00:09:36.590><c> into</c><00:09:37.010><c> graphs</c><00:09:37.280><c> then</c><00:09:38.060><c> you</c><00:09:38.150><c> can</c><00:09:38.330><c> just</c><00:09:38.510><c> use</c>

00:09:38.650 --> 00:09:38.660 align:start position:0%
about into graphs then you can just use
 

00:09:38.660 --> 00:09:40.270 align:start position:0%
about into graphs then you can just use
this<00:09:38.870><c> module</c><00:09:39.170><c> to</c><00:09:39.560><c> get</c><00:09:39.710><c> a</c><00:09:39.740><c> zero</c><00:09:40.130><c> knowledge</c>

00:09:40.270 --> 00:09:40.280 align:start position:0%
this module to get a zero knowledge
 

00:09:40.280 --> 00:09:43.630 align:start position:0%
this module to get a zero knowledge
proof<00:09:40.960><c> from</c><00:09:41.960><c> that</c><00:09:42.230><c> graph</c><00:09:42.500><c> that</c><00:09:42.610><c> verifies</c><00:09:43.610><c> that</c>

00:09:43.630 --> 00:09:43.640 align:start position:0%
proof from that graph that verifies that
 

00:09:43.640 --> 00:09:46.090 align:start position:0%
proof from that graph that verifies that
the<00:09:44.120><c> rules</c><00:09:44.360><c> specified</c><00:09:44.960><c> by</c><00:09:45.230><c> the</c><00:09:45.290><c> finite</c><00:09:45.950><c> state</c>

00:09:46.090 --> 00:09:46.100 align:start position:0%
the rules specified by the finite state
 

00:09:46.100 --> 00:09:47.740 align:start position:0%
the rules specified by the finite state
machine<00:09:46.550><c> corresponding</c><00:09:47.090><c> to</c><00:09:47.210><c> a</c><00:09:47.270><c> graph</c><00:09:47.480><c> are</c>

00:09:47.740 --> 00:09:47.750 align:start position:0%
machine corresponding to a graph are
 

00:09:47.750 --> 00:09:50.260 align:start position:0%
machine corresponding to a graph are
being<00:09:48.110><c> followed</c><00:09:48.550><c> yeah</c><00:09:49.550><c> I</c><00:09:49.580><c> think</c><00:09:49.760><c> that's</c><00:09:50.120><c> it</c>

00:09:50.260 --> 00:09:50.270 align:start position:0%
being followed yeah I think that's it
 

00:09:50.270 --> 00:09:51.100 align:start position:0%
being followed yeah I think that's it
basically

00:09:51.100 --> 00:09:51.110 align:start position:0%
basically
 

00:09:51.110 --> 00:09:52.970 align:start position:0%
basically
thank<00:09:51.680><c> you</c>

00:09:52.970 --> 00:09:52.980 align:start position:0%
thank you
 

00:09:52.980 --> 00:10:04.870 align:start position:0%
thank you
[Applause]

00:10:04.870 --> 00:10:04.880 align:start position:0%
 
 

00:10:04.880 --> 00:10:06.940 align:start position:0%
 
you